Provability interpretations of a many-sorted polymodal logic

Abstract

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_{n+1}$-Sätze interpretiert. In Beantwortung einer von Beklemishev gestellten Frage zeigen wir im ersten Teil dieser Arbeit, dass diese mehrsortige Logik arithmetisch vollständig bezüglich einer geeigneten arithmetischen Interpretation ist, welche der zuvor Einschränkung bezüglich der Sorten genügt. Da die beweistheoretischen Anwendungen von GLP bereits in dem positiven Fragment derselben erfolgen können, folgen wir im zweiten Teil dieser Arbeit jüngsten Untersuchungen positiver Fragmente von 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_{n+1}$-axiomatisierbare Erweiterungen von PA instanziert, während jene der Sorte $\omega$ durch beliebige Erweiterungen derselben interpretiert werden. Diese Interpretation gestattet die Einführung eines modalen Operators $\langle\omega\rangle$, welcher als das Schema der vollen uniformen Reflexion der Arithmetik interpretiert wird, für welches es keine endliche, jedoch eine rekursive Axiomatisierung gibt. Wir zeigen, dass unser Reflexionskalkül arithmetisch vollständig bezüglich dieser Interpretation ist.

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_{n+1}$-sentences. In response to a question posed by Beklemishev, we show in the first part of this thesis that the resulting many-sorted modal logic is arithmetically complete with respect to a class of arithmetical interpretations which satisfies the aforementioned restriction. Since these proof-theoretic applications can already be carried out in a positive fragment of GLP, we follow in the second part of this thesis recent trends concerning the investigation of such positive fragments of GLP. In the style of a work due to Beklemishev, we define a many-sorted positive reflection calculus where we, 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_{n+1}$-axiomatized extensions of PA, while variables of sort $\omega$ are interpreted as arbitrary extensions thereof. This interpretation enables us to introduce an additional modal operator $\langle\omega\rangle$ which is interpreted as the full uniform reflection schema in arithmetic that knows no finite, yet a recursive axiomatization. We prove that our reflection calculus is arithmetically complete with respect to this interpretation.