Modal and arithmetical completeness results

Definition 3.7   By the class of ${\mathit ILX}$-frames we mean the class of $\mathit{IL}$-frames where X hold as a scheme. This class is often also referred to as the class of characteristical ${\mathit ILX}$-frames.

The Veltman semantics yields a uniform soundness theorem, that is, all ${\mathit ILX}$ are sound w.r.t. their corresponding class of characteristical frames. So every derivable formula holds on every characteristical frame of that logic. One can ask if the reverse also holds. So if a formula holds on all ${\mathit ILX}$-frames, is it then automatically provable in ${\mathit ILX}$? No uniform method is known to settle this modal completeness problem and with every new logic a new proof has to be found. The logics $\mathit{ILM}$, $\mathit{ILP}$ and $\mathit{ILW}$ are known to be modally complete. The completeness proof of $\mathit{ILW}$ of Dick de Jongh and Frank Veltman is to be published soon ([dJV]). For a long time the modal completeness of $\mathit{ILM_0}$ has been an open problem. In this thesis the question is answered positively. All modal completeness results in provability logic look alike a little. One works with maximal consistent subsets of a certain adequate set. With these maximal consistent sets as construction material, one makes up a countermodel for some statement ${\mathcal A}$ which is not provable in the logic. With any new logic, one has to re-consider the notion of adequateness. Adequate means large enough to do the required mathematics and small enough to have the countermodel finite. So in one stroke one proves modal completeness and decidability. (That is, if the logic is r.e. axiomatizable.) Miraculously this method work for most logics in this area. In this paper a method is developed by which only completeness is established without necessarily decidability.

Definition 3.8   Given ${\mathit ILX}$. An arithmetical translation is a function *, assigning arithmetical formulas to formulas in the language $\Box$, $\rhd$ in such a way that * commutes with all the connectives and moreover:

-

$(\bot )^*=\bot$,

-

$(\Box A)^*=$ an intensional formalization of ``A^* is provable in ${\mathit ILX}$'', for example the standard $\exists x{\mathit Proof}(x,\ulcorner A^*\urcorner)$,

-

$(A\rhd B)^*=$ an intensional formalization of `` $\mathit{IL}X +A^*$interprets $\mathit{IL}X+ B^*$''. One can use (+) for this purpose.

Once this translation is introduced, one can ask for the logic of all principles proved by $\mathit{PA}$ under this translation. In 2.2 and 2.3 we have already seen all the principles of $\mathit{ILM}$ to be provable under the translation *. But something stronger holds. Solovay's first completeness theorem can be generalized to interpretability logic to obtain the arithmetical completeness of $\mathit{ILM}$ w.r.t. $\mathit{PA}$.

Theorem 3.9 (Berarducci [Ber90], Shavrukov [Sha88])   $\mathit{ILM} \vdash A \Leftrightarrow \forall \ ^* \ {\mathit PA}\vdash A^*$.

Actually $\mathit{ILM}$ is the interpretability logic of any essentially reflexive theory. It turns out that also in this situation adding the reflexion principle is sufficient to obtain a generalization of Solovay's second completeness result. See [Ber90]. All principles of $\mathit{ILP}$ have been seen to be arithmetically valid in every reasonable finitely axiomatizable arithmetical theory. We also have $\mathit{ILP}$ arithmetically complete w.r.t. any such theory. So $\mathit{ILP}$is the interpretability logic of $I\Sigma_n$ for all $n\in \omega$ as every $I\Sigma_n$ is finitely axiomatizable.

We have a notion of reasonable arithmetical theory. For the time being this notion can be thought of as $I\Delta_0 + \mathrm{SUPEXP}$. Up until today it is unknown what the interpretability logic of all reasonable arithmetical theories is. For a long time it was conjectured to be $\mathit{ILW}$. See [Vis91]. Until M₀ was seen to be arithmetically valid. Also in [Vis91]. Since then $\mathit{ILW}^*(={\mathit ILWM_0})$ has been conjectured to be the interpretability logic of all reasonable arithmetical theories. From now on we will abbreviate this target logic by $\mathit{GIL}$, for general interpretability logic. We will not write ${\mathit ILG}$ as we do not want to insinuate that we would know the relevant principle. A priori it is not even known if $\mathit{GIL}$ is axiomatizable at all! In this paper the conjecture that $\mathit{ILW}^*$ is $\mathit{GIL}$ is falsified.

Definition 3.10   T' is $\Pi^0_1$-conservative over T means that $T'\vdash \pi$implies $T\vdash \pi$ for every $\pi \in \Pi^0_1$.

The definition could be generalized by fixing different sets $\Gamma$of sentences instead of just $\Pi^0_1$. One can also translate $A\rhd B$ to an intensional formalization of ``T+B is $\Pi^0_1$-conservative over T+A''. The logic corresponding to this translation is the logic of $\Pi^0_1$-conservativity. It is known that $\mathit{ILM}$ is the logic of $\Pi^0_1$-conservativity for any arithmetical theory containing $I\Sigma_1$. If an arithmetical theory is essentially reflexive the notion of $\Pi^0_1$-conservativity coincides with the notion of interpretability.