TWO NEW SERIES OF PRINCIPLES IN THE INTERPRETABILITY LOGIC OF ALL REASONABLE ARITHMETICAL THEORIES

The provability logic of a theory T captures the structural behavior of formalized provability in T as provable in T itself. Like provability, one can formalize the notion of relative interpretability giving rise to interpretability logics. Where provability logics are the same for all moderately sound theories of some minimal strength, interpretability logics do show variations.The logic IL (All) is defined as the collection of modal principles that are provable in any moderately sound theory of some minimal strength. In this article we raise the previously known lower bound of IL (All) by exhibiting two series of principles which are shown to be provable in any such theory. Moreover, we compute the collection of frame conditions for both series.

NON–WELL-FOUNDED DERIVATIONS IN THE GÖDEL-LÖB PROVABILITY LOGIC

We consider Hilbert-style non–well-founded derivations in the Gödel-Löb provability logic GL and establish that GL with the obtained derivability relation is globally complete for algebraic and neighbourhood semantics.

THE -PROVABILITY LOGIC OF

For the Heyting Arithmetic HA, $HA^{\text{*}} $ is defined [14, 15] as the theory $\left\{ {A|HA \vdash A^\square } \right\}$, where $A^\square $ is called the box translation of A (Definition 2.4). We characterize the ${\text{\Sigma }}_1 $-provability logic of $HA^{\text{*}} $ as a modal theory $iH_\sigma ^{\text{*}} $ (Definition 3.17).

COMPLETE ADDITIVITY AND MODAL INCOMPLETENESS

In this article, we tell a story about incompleteness in modal logic. The story weaves together an article of van Benthem (1979), “Syntactic aspects of modal incompleteness theorems,” and a longstanding open question: whether every normal modal logic can be characterized by a class ofcompletely additivemodal algebras, or as we call them,${\cal V}$-baos. Using a first-order reformulation of the property of complete additivity, we prove that the modal logic that starred in van Benthem’s article resolves the open question in the negative. In addition, for the case of bimodal logic, we show that there is a naturally occurring logic that is incomplete with respect to${\cal V}$-baos, namely the provability logic$GLB$(Japaridze, 1988; Boolos, 1993). We also show that even logics that are unsound with respect to such algebras do not have to be more complex than the classical propositional calculus. On the other hand, we observe that it is undecidable whether a syntactically defined logic is${\cal V}$-complete. After these results, we generalize the Blok Dichotomy (Blok, 1978) to degrees of${\cal V}$-incompleteness. In the end, we return to van Benthem’s theme of syntactic aspects of modal incompleteness.

Provability logic

Central to Gödel’s second incompleteness theorem is his discovery that, in a sense, a formal system can talk about itself. Provability logic is a branch of modal logic specifically directed at exploring this phenomenon. Consider a sufficiently rich formal theory T. By Gödel’s methods we can construct a predicate in the language of T representing the predicate ‘is formally provable in T’. It turns out that T is able to prove statements of the form - (1) If A is provable in T, then it is provable in T that A is provable in T. In modal logic, predicates such as ‘it is unavoidable that’ or ‘I know that’ are considered as modal operators, that is, as non-truth-functional propositional connectives. In provability logic, ‘is provable in T’ is similarly treated. We write □A for ‘A is provable in T’. This enables us to rephrase (1) as follows: - (1′) □A →□□A. This is a well-known modal principle amenable to study by the methods of modal logic. Provability logic produces manageable systems of modal logic precisely describing all modal principles for □A that T itself can prove. The language of the modal system will be different from the language of the system T under study. Thus the provability logic of T (that is, the insights T has about its own provability predicate as far as visible in the modal language) is decidable and can be studied by finitistic methods. T, in contrast, is highly undecidable. The advantages of provability logic are: (1) it yields a very perspicuous representation of certain arguments in a formal theory T about provability in T; (2) it gives us a great deal of control of the principles for provability in so far as these can be formulated in the modal language at all; (3) it gives us a direct way to compare notions such as knowledge with the notion of formal provability; and (4) it is a fully worked-out syntactic approach to necessity in the sense of Quine.

PROVABILITY LOGICS RELATIVE TO A FIXED EXTENSION OF PEANO ARITHMETIC

Let T and U be any consistent theories of arithmetic. If T is computably enumerable, then the provability predicate $P{r_\tau }\left( x \right)$ of T is naturally obtained from each ${{\rm{\Sigma }}_1}$ definition $\tau \left( v \right)$ of T. The provability logic $P{L_\tau }\left( U \right)$ of τ relative to U is the set of all modal formulas which are provable in U under all arithmetical interpretations where □ is interpreted by $P{r_\tau }\left( x \right)$. It was proved by Beklemishev based on the previous studies by Artemov, Visser, and Japaridze that every $P{L_\tau }\left( U \right)$ coincides with one of the logics $G{L_\alpha }$, ${D_\beta }$, ${S_\beta }$, and $GL_\beta ^ -$, where α and β are subsets of ω and β is cofinite.We prove that if U is a computably enumerable consistent extension of Peano Arithmetic and L is one of $G{L_\alpha }$, ${D_\beta }$, ${S_\beta }$, and $GL_\beta ^ -$, where α is computably enumerable and β is cofinite, then there exists a ${{\rm{\Sigma }}_1}$ definition $\tau \left( v \right)$ of some extension of $I{{\rm{\Sigma }}_1}$ such that $P{L_\tau }\left( U \right)$ is exactly L.