Titelaufnahme

Titel
Provability interpretations of a many-sorted polymodal logic / von Gerald Berger
VerfasserBerger, Gerald
Begutachter / BegutachterinTompits, Hans
Erschienen2015
UmfangIX, 87 S. : graph. Darst.
HochschulschriftWien, Techn. Univ., Dipl.-Arb., 2015
Anmerkung
Zsfassung in dt. Sprache
SpracheEnglisch
DokumenttypDiplomarbeit
Schlagwörter (DE)Beweisbarkeitslogiken / Mathematische Logik / Modallogik / Formale Arithmetik
Schlagwörter (EN)Provability Logics / Mathematical Logic / Modal Logic / Formal Arithmetic
URNurn:nbn:at:at-ubtuw:1-83834 Persistent Identifier (URN)
Zugriffsbeschränkung
 Das Werk ist frei verfügbar
Dateien
Provability interpretations of a many-sorted polymodal logic [0.95 mb]
Links
Nachweis
Klassifikation
Zusammenfassung (Deutsch)

Beweisbarkeitslogiken stellen einen wohlstudierten Zweig nichtklassischer Logiken dar und finden Interpretationen in Systemen, welche die elementare Zahlentheorie formalisieren. Die polymodale Beweisbarkeitslogik GLP von G.K. Japaridze erfuhr reges Interesse in der Literatur. GLP ist vollständig bezüglich einer arithmetischen Interpretation, welche eng mit den partiellen uniformen Reflexionsprinzipien der formalen Arithmetik zusammenhängt. Weiters erlaubt das geschlossene Fragment von GLP die Entwicklung eines Systems zur Notation von Ordinalzahlen bis $\varepsilon_0$. Basierend auf diesen Beobachtungen lieferte L.D. Beklemishev einen zum Gentzen'schen alternativen Beweis zur Konsistenz der Peano Arithmetik (PA) per transfiniter Induktion bis $\varepsilon_0$. Diese beweistheoretische Analyse wird im Rahmen von sortierten Beweisbarkeitsalgebren durchgeführt, welche einem erlauben beweistheoretische Informationen der betrachteten Theorie zu erfassen. Die sortierte Beweisbarkeitsalgebra einer Theorie kann-von einem logischen Standpunkt betrachtet-als mehrsortige Variante von GLP aufgefasst werden. In dieser Arbeit untersuchen wir diese mehrsortige Variante von GLP, welche aussagenlogischen Variablen Sorten $\alpha \leq \omega$ zuweist. Dabei wird jede aussagenlogische Variable der Sorte $n < \omega$ nur durch $\Pi_ GLP. In Anlehnung an eine Arbeit von Beklemishev definieren wir einen mehrsortigen positiven Reflexionskalkül, wobei wir die modalen Diamanten als verschiedene Formen der Reflexion in der formalen Arithmetik auffassen. Dabei erlaubt uns die Beschränkung auf das positive Fragment eine reichhaltigere Interpretation der aussagenlogischen Variablen: Diese werden nicht als arithmetische Sätze, sondern als primitiv rekursive Aufzählungen von möglicherweise unendlichen arithmetischen Theorien interpretiert. Hierbei werden Variablen der Sorte $n < \omega$ durch $\Pi_

Zusammenfassung (Englisch)

Provability logics constitute a well-studied branch of nonclassical logics and find interpretations in systems formalizing elementary number theory. The polymodal provability logic GLP, due to G.K. Japaridze, received considerable interest in the literature. GLP is arithmetically complete for an arithmetical interpretation which is closely related to the partial uniform reflection principles in formal arithmetic. Furthermore, the closed fragment of GLP allows to develop an ordinal notation system up to $\varepsilon_0$. Based on these observations, L.D. Beklemishev provided an alternative proof of G. Gentzen's consistency proof for Peano Arithmetic (PA) by transfinite induction up to $\varepsilon_0$. This ordinal analysis is carried out in the framework of graded provability algebras, which enable one to capture proof-theoretic information of the theory under consideration. The graded provability algebra of a theory can-from a logical point of view-be considered as a many-sorted variant of GLP. In this thesis, we investigate this many-sorted variant of GLP which assigns sorts $\alpha \leq \omega$ to propositional variables. Thereby, propositional variables of sort $n < \omega$ are arithmetically interpreted as $\Pi_ from the point of view of arithmetic, interpret the modal diamonds as different forms of reflection in formal arithmetic. Thereby, the restriction to the positive fragment allows for a richer arithmetical interpretation of propositional variables: these are not interpreted as single arithmetical sentences but as primitive recursive numerations of possibly infinite arithmetical theories. There, variables of sort $n < \omega$ are interpreted as $\Pi_