Solovay’s Completeness Without Fixed Points

Abstract

In this paper we present a new proof of Solovay’s theorem on arithmetical completeness of Gödel-Löb provability logic $\mathsf {GL}$. Originally, completeness of $\mathsf {GL}$ with respect to interpretation of $\Box$ as provability in $\mathsf {PA}$ was proved by Solovay in 1976. The key part of Solovay’s proof was his construction of an arithmetical evaluation for a given modal formula that made the formula unprovable in $\mathsf {PA}$ if it were unprovable in $\mathsf {GL}$. The arithmetical sentences for the evaluations were constructed using certain arithmetical fixed points. The method developed by Solovay have been used for establishing similar semantics for many other logics. In our proof we develop new more explicit construction of required evaluations that doesn’t use any fixed points in their definitions. To our knowledge, it is the first alternative proof of the theorem that is essentially different from Solovay’s proof in this key part.

F. Pakhomov—This work is supported by the Russian Science Foundation under grant 14-50-00005.

Appendices

A Formalization of the Omitting Types Theorem

In order to formalize Theorem 2 in $\mathsf {ACA_0}$ we will first show that the Omitting Types Theorem is formalizable in $\mathsf {ACA_0}$. We will adopt the proof from [CK90]. We remind a reader that we use the approach to formalization of model theory from Simpson book [Sim09].

Definition 2

( $\mathsf {ACA}_0$ ). Let $\mathsf {T}$ be a first-order theory and $\varSigma =\varSigma (x_1,\ldots ,x_n)$ be a set of formulas of the language of $\mathsf {T}$ that have no free variables other than $x_1,\ldots ,x_n$. We say that $\mathsf {T}$ locally omits $\varSigma$ if for every formula $\varphi (x_1,\ldots ,x_n)$ at least one of the following fails:

• 1. the theory $\mathsf {T}+\varphi$ is consistent;

• 2. for all $\psi \in \varSigma$ we have $\mathsf {T}\vdash \forall x_1,\ldots ,x_n(\varphi \rightarrow \psi )$.

We say that a model $\mathfrak {M}$ of $\mathsf {T}$ omits $\varSigma$ if for any $a_1,\ldots ,a_n\in \mathfrak {M}$ there is a formula $\psi (x_1,\ldots ,x_n)\in \varSigma$ such that .

Theorem 3

( $\mathsf {ACA}_0$ ). Suppose $\mathsf {T}$ is a consistent theory that locally omits the set of formulas $\varSigma (x_1,\ldots ,x_n)$. Then there is a model $\mathfrak {M}$ of $\mathsf {T}$ that omits the set $\varSigma$.

Proof

We will follow the proof of [CK90, Theorem 2.2.9] but make sure that our arguments could be carried out in $\mathsf {ACA}_0$.

We will prove the theorem for $n=1$, i.e. $\varSigma =\varSigma (x)$. The case $n>1$ could be proved essentially the same way, but the notations would be more complicated.

We extend the language of $\mathsf {T}$ by fresh constants $c_0,c_1,\ldots$. We arrange all sentences of the extended language in a sequence $\varphi _0,\varphi _1,\ldots$ (since we work in $\mathsf {ACA}_0$ the formulas are encoded by Gödel numbers and we could arrange them by their Gödel numbers). We will construct a sequence of finite sets of sentences

$$\begin{aligned} \emptyset =\mathsf {U}_0\subset \mathsf {U}_1\subset \ldots \subset \mathsf {U}_m\subset \ldots \end{aligned}$$

such that for every m we have the following:

• 1. $\mathsf {U}_m$ is consistent with $\mathsf {T}$;

• 2. either $\varphi _m\in \mathsf {U}_{m+1}$ or $\lnot \varphi _m\in \mathsf {U}_{m+1}$;

• 3. if $\varphi _m$ is of the form $\exists x \psi (x)$ and $\varphi _m\in \mathsf {U}_{m+1}$ then $\psi (c_p)\in \mathsf {U}_{m+1}$, where $c_p$ is the first $c_i$ that doesn’t occur in $\mathsf {U}_m$ or $\varphi _m$;

• 4. there is a formula $\chi (x)\in \varSigma$ such that $\lnot \chi (c_m)\in \mathsf {U}_{m+1}$.

We will give the definition that will determine unique sequence $\mathsf {U}_0,\mathsf {U}_1,\ldots$. We want to make sure that for our definition of the sequence $\mathsf {U}_0,\mathsf {U}_1,\ldots$, the property of a number x to be the code of the sequence $\langle \mathsf {U}_0,\mathsf {U}_1,\ldots ,\mathsf {U}_y\rangle$ is expressible by a formula without second-order quantifiers. If we will ensure this, then we will be able to construct a set that encodes the sequence $\mathsf {U}_0,\mathsf {U}_1, \ldots , \mathsf {U}_m,\ldots$ using the arithmetic comprehension.

Let us define $\mathsf {U}_{m+1}$ in terms of $\mathsf {U}_m$. If $\varphi _m$ is consistent with $\mathsf {T}\cup \mathsf {U}_m$ then we put $\sigma _m$ to be $\varphi _m$. Otherwise we put $\sigma _m$ to be $\lnot \varphi _m$. If $\sigma _m$ is $\varphi _m$ and is of the form $\exists x \psi (x)$ then we put $\xi _m$ to be $\psi (c_p)$, where $c_p$ is the first $c_i$ that doesn’t occur in $\mathsf {U}_m$ or $\varphi _m$. Otherwise, we put $\xi _m$ to be equal to $\sigma _m$. We choose the formula $\chi (x)$ with the smallest Gödel number such that $\chi (x)\in \varSigma$ and $\mathsf {T}\nvdash \bigwedge \mathsf {U}_m \rightarrow \chi (c_m)$. We put $\mathsf {U}_{m+1}=\mathsf {U}_m\cup \{\xi _m,\sigma _m,\chi (c_m)\}$.

It is easy to see that for this definition, indeed, we could express by a formula without second-order quantifiers the property of a number x to be the code of the sequence $\langle \mathsf {U}_0,\mathsf {U}_1,\ldots ,\mathsf {U}_y\rangle$. By a trivial induction on y we could prove that for every y the said sequence exists and unique. Thus, we have obtained the sequence $\mathsf {U}_0, \mathsf {U}_1,\ldots ,\mathsf {U}_m,\ldots$ encoded by a set.

Now, using the definition of the sequence, we could easily prove that the sequence satisfy the conditions 1, 2, 3, and 4.

We consider the union $\mathsf {T}\cup \bigcup \limits _{i\in \mathbb {N}}\mathsf {U}_i=\mathsf {T}'$. By condition 1. the theory $\mathsf {T}'$ is consistent. By condition 2. the theory $\mathsf {T}'$ is complete. By condition 3. the theory $\mathsf {T}'$ gives the truth definition with Tarski conditions for a model with the domain $\{c_0,c_1,\ldots \}$; this gives us a model $\mathfrak {M}$ of $\mathsf {T}'$ with the domain $\{c_0,c_1,\ldots \}$. By condition 4. The model $\mathfrak {M}$ omits the set $\varSigma$.

B Formalization of the Injecting Inconsistencies Theorem

Now we are going to check that Theorem 2 is provable in $\mathsf {ACA}_0$. Below we assume that a reader is familiar with the paper [VV94] and we will use some notions from the paper without giving the definitions here.

Theorem 4

Let $\mathsf {R}\subset \mathsf {I\Delta _0+\Omega _1}$ be a finitely axiomatizable theory. Then $\mathsf {ACA_0}$ proves the following:

Let $\mathsf {T}\supseteq \mathsf {I\Delta _0+\Omega _1}$ be a $\varSigma _1^b$-axiomatized theory for which the small reflection principle is provable in $\mathsf {R}$. Let $\mathsf {Con}_{\mathsf {T}}(x)$ denote the formula . Let $\mathfrak {M}$ be a non-standard model of $\mathsf {T}$ and let c, a be nonstandard elements of $\mathfrak {M}$ such that $\mathfrak {M}\models c\le a$, $\mathrm {exp}(a^c)\in \mathfrak {M}$, and $\mathfrak {M}\models \mathsf {Con}_{\mathsf {T}}(a^k)$, for all standard k. Then there exists a model $\mathfrak {K}$ of $\mathsf {T}$ such that $a\in \mathfrak {K}$ and

• 1. $\mathfrak {M}\upharpoonright a =\mathfrak {K} \upharpoonright a$;

• 2. $\mathfrak {M}\upharpoonright \mathrm {exp}(a^k) \subseteq \mathfrak {K}$, for all standard k;

• 3. $\mathfrak {K}\models \lnot \mathsf {Con}_{\mathsf {T}}(a^c)$;

• 4. for all standard k we have $\mathfrak {K}\models \mathsf {Con}_{\mathsf {T}}(a^k)$;

• 5. $\mathfrak {K}\models \mathrm {exp}(a^c)\downarrow$.

Proof

Essentially, we just need to formalize the proof of [VV94, Theorem 5.1] in $\mathsf {ACA_0}$. The only difference between our formulation and the formulation by Visser and Verbrugge is that we have replaced the requirement that the small reflection principle is provable in $\mathsf {I\Delta _0+\Omega _1}$ with a stronger requirement that states that the small reflection principle is provable in $\mathsf {R}$. First, we show how to formalize the proof itself and then explain why the results used in the proof are formalizable in $\mathsf {ACA_0}$.

The only non-trivial part of the formalization of the proof itself is the issue with the lack of truth definition for the cut

$$\begin{aligned} \mathfrak {N}=\{u\in \mathfrak {M}\mid u<\mathrm {exp}(a^k)\text {, for some standard } {k}\} \end{aligned}$$

of $\mathfrak {M}$. However, for the purposes of the proof, it would be enough for $\mathfrak {N}$ to be a weak model (i.e. poses truth definition only for axioms, [Sim09, Definition II.8.9]). Moreover, unlike the original proof of Visser and Verbrugge, we just need $\mathfrak {N}$ to be a weak model of $\mathsf {R}+\mathsf {B\varSigma _1}$ rather than a model of $\mathsf {B\varSigma _1+\Omega _1}$. And since $\mathsf {R}$ is externally fixed finitely axiomatizable theory, we could create the required truth definition straightforward using arithmetical comprehension. Other parts of the proof could be formalized without any complications.

The proof of [VV94, Theorem 5.1] used Wilkie and Paris result [WP89, Theorem 1], Pudlák results from [Pud86], and the Omitting Types Theorem. We have already formalized the Omitting Types Theorem in Appendix A. The proof of [WP89, Theorem 1] is trivial and could be easily formalized in $\mathsf {ACA_0}$. The technique of [Pud86] is purely finitistic and thus could be easily formalized in $\mathsf {ACA_0}$.

Now we want to derive the formalization of Theorem 2 from Theorem 4. In order to do it, we first need to fix some finite fragment $\mathsf {R}\subset \mathsf {I\Delta _0+\Omega _1}$. And next we need to show in $\mathsf {ACA}_0$ that all the extensions of $\mathsf {PA}$ by finitely many axioms are $\varSigma _1^b$-axiomatizable extensions of $\mathsf {I\Delta _0+\Omega _1}$ for which $\mathsf {R}$ proves the small reflection principle. Obviously, extensions of $\mathsf {PA}$ by finitely many axioms are $\varSigma _1^b$-axiomatizable (and it could be checked in $\mathsf {ACA_0}$).

In [VV94, Theorem 4.20] it were established that $\mathsf {I\Delta _0+\Omega _1}$ proves small reflection principle for $\mathsf {I\Delta _0+\Omega _1}$. By inspecting the proof, it is easy to see that it is possible to use only finitely many axioms of $\mathsf {I\Delta _0+\Omega _1}$ in order to prove all the instances of the small reflection principle. Now we will indicate how to modify the proof of [VV94, Theorem 4.20] in order to prove in a finite fragment of $\mathsf {I\Delta _0+\Omega _1}$ all the instances of the small reflection principle for all the extensions of $\mathsf {PA}$ by finitely many axioms. Actually, the only part of the proof that should be changed is [VV94, Lemma 4.16] that were needed to deal with the schema of $\varDelta _0$-induction schema in the case of $\mathsf {I\Delta _0+\Omega _1}$-provability. For our adaptation we need to replace it with the analogous lemma that will deal with schema of full induction in the case of provability in $\mathsf {PA}$. This analogous lemma could be proved essentially in the same way as [VV94, Lemma 4.16] itself with the only difference that the last part of the proof that were reducing an instance of induction schema to an instance of $\varDelta _0$-induction schema will not be needed any longer. This concludes the proof of Theorem 2 in $\mathsf {ACA_0}$.