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.

1 Introduction

The study of provability as a modality could be traced back to at least as early as Gödel work [Gö33]. Löb [Lö55] have proved a generalization of Gödel’s Second Incompleteness Theorem that is now known as Löb’s Theorem. In order to formulate his theorem Löb have stated conditions on provability predicates that are now known as Hilbert-Bernays-Löb derivability conditions. Despite Löb haven’t mentioned the interpretation of a modality as a provability predicate there, his conditions essentially corresponded to the standard axiomatization of modal logic $\mathsf {K4}$. Also note that arithmetical soundness of Gödel-Löb provability logic $\mathsf {GL}$ immediately follows from Löb’s Theorem.

The axioms of modal system $\mathsf {GL}$ have first appeared in [Smi63]. Segerberg have shown that $\mathsf {GL}$ is Kripke-complete and moreover that it is complete with respect to the class of all finite transitive irreflexive trees [Seg71]. The arithmetical completeness of the system $\mathsf {GL}$ were established by Solovay [Sol76]. Solovay have proved that a modal formula $\varphi$ is a theorem of $\mathsf {GL}$ iff for every arithmetical evaluation f(x) the arithmetical sentence $f(\varphi )$ is provable in $\mathsf {PA}$.

Latter modifications of Solovay’s method were used in order to prove a lot of other similar results, we will mention just few of them. Japaridze have proved arithmetical completeness of polymodal provability logic $\mathsf {GLP}$ [Jap86]. Shavrukov [Sha88] and Berarducci [Ber90] have determined the interpretability logic of $\mathsf {PA}$.

The key part of Solovay’s proof was to show that in certain sense every finite $\mathsf {GL}$-model is “embeddable” in arithmetic. Using the construction of “embeddings”, it is easy to construct evaluations $f_{\varphi }(x)$ such that $\mathsf {PA}\nvdash f_{\varphi }(\varphi )$, for all $\mathsf {GL}$-unprovable modal formulas $\varphi$. In order to construct the “embeddings”, Solovay have used Diagonal Lemma to define certain primitive-recursive function (Solovay function), for every finite $\mathsf {GL}$ Kripke model. Then, using the functions, Solovay have defined the sentences that constituted the “embeddings”.

de Jongh, Jumelet, and Montagna have shown that $\mathsf {GL}$ is complete with respect to $\varSigma _1$-provability predicates for theories $\mathsf {T}\supseteq \mathsf {I\Delta _0}+\mathsf {Exp}$ [dJJM91]. Their proof have avoided the use of Solovay functions, however, their construction still “emulated” Solovay’s approach using individual sentences constructed by Diagonal Lemma.

In a discussion on FOM (Foundation of Mathematics mailing list) Shipman have asked a question about important theorems that have “essentially” only one proof [Shi09]. The example of Solovay’s theorem were provided by Sambin. To the author knowledge, up to the date there were no proofs of Solovay’s theorem that have avoided the central idea of Solovay’s proof—the Solovay’s method of constructing required sentences in terms of certain fixed points.

We note that completeness of some extensions of $\mathsf {GL}$ with respect to interpretations of $\Box$ that are similar to formalized provability were proved by the completely different methods. Solovay in his paper [Sol76] have briefly mentioned a method of determining modal logics of several natural interpretations of $\Box$ in set theory, namely for the interpretations of $\Box$ as “to be true in all transitive models” and as “to be true in all models $\mathbf {V}_{\kappa }$, where $\kappa$ is an inaccessible cardinal” (there are more detailed proofs in Boolos book [Boo95, Chap. 13]). A modification of the method also have been used to show completeness of wide variety of extensions of $\mathsf {GL}$ with respect to artificially defined (not $\varSigma _1$) provability-like predicates [Pak16].

In the paper we present a new approach to the proof of arithmetical completeness theorem for $\mathsf {GL}$. We introduce a different method of “embedding” of finite $\mathsf {GL}$ Kripke models. As the result, the completeness of $\mathsf {GL}$ is achieved with the use of evaluations given by more explicitly constructed and more “natural” sentences (in particular, we do not rely on Diagonal Lemma in the construction). In order to avoid potential misunderstanding, we note that despite the sentences from evaluations are given explicitly, our proof rely on Gödel’s Second Incompleteness Theorem and the results by Pudlák [Pud86] that were proved with the use of Diagonal Lemma.

Now we will give an example of unprovable $\mathsf {GL}$-formula $\varphi$ and an evaluation f(x) provided by our proof such that $\mathsf {PA}\nvdash f(\varphi )$. We consider the formula

$$\begin{aligned} \varphi \mathrel {\leftrightharpoons } \Diamond v \rightarrow (\Diamond u \rightarrow \Diamond (v\wedge u)). \end{aligned}$$

We use the following definitions for numerical functions in order to define the evaluation f(x):

$$\begin{aligned} \mathrm {exp}(x)=2^x,\;\; \log (x)=\max (\{y\mid \mathrm {exp}(y)\le x\}\cup 0), \end{aligned}$$

(note that the functions $\mathrm {exp}^{\star }(x)$ and $\log ^{\star }(x)$ are called super exponentiation and super logarithmic functions, respectively). The evaluation f(x) is given as following:

We note that somewhat similar approach based on the parity of $\log ^{\star }$ were used by Solovay in his letter to Nelson [Sol86]. Solovay proved that there are sentences $\mathsf {F}$ and $\mathsf {G}$ such that $\mathsf {I\Delta _0+\Omega _1}+\mathsf {F}$ and $\mathsf {I\Delta _0+\Omega _1}+\mathsf {G}$ are cut-interpretable in $\mathsf {I\Delta _0+\Omega _1}$, but $\mathsf {I\Delta _0+\Omega _1}+ \mathsf {F}\wedge \mathsf {G}$ isn’t cut-interpretable in $\mathsf {I\Delta _0+\Omega _1}$. Also, Kotlarski in [Kot96] have used an explicit parity-based construction of a pair of sentences in order to give an alternative proof for Rosser’s Theorem.

2 Preliminaries

Let us first define Gödel-Löb provability logic $\mathsf {GL}$. The language of $\mathsf {GL}$ extends the language of propositional calculus with propositional constants $\top$ (truth) and $\bot$ (false) by the unary modal connective $\Box$. $\mathsf {GL}$ have the following Hilbert-style deductive system:

• 1. axiom schemes of classical propositional calculus $\mathsf {PC}$;

• 2. $\Box (\varphi \rightarrow \psi )\rightarrow (\Box \varphi \rightarrow \Box \psi )$;

• 3. $\Box (\Box \varphi \rightarrow \varphi )\rightarrow \Box \varphi$;

• 4. $\frac{\varphi \;\;\varphi \rightarrow \psi }{\psi }$;

• 5. $\frac{\varphi }{\Box \varphi }$.

The expression $\Diamond \varphi$ is an abbreviation for $\lnot \Box \lnot \varphi$.

A set with a binary relation $(W,\prec )$ is called irreflexive transitive tree if

• 1. $\prec$ is a transitive irreflexive relation;

• 2. there is an element $r\in W$ that is called the root of $(W,\prec )$ such that the upward cone $\{a\mid r\prec a\}$ coincides with W;

• 3. for any element $w\in W$ the restriction of $\prec$ on the downward cone $\{a\mid a\prec w\}$ is a strict well-ordering order.

Segerberg [Seg71] have shown that the logic $\mathsf {GL}$ is complete with respect to the class of all finite irreflexive transitive trees.

Our proof relies on the results by Verbrugge and Visser [VV94] and indirectly on the results by Pudlák [Pud86]. This results are sensitive to details of formalization of some metamathematical notions. Thus unlike some other papers, where this kind of details could be safely be left unspecified, we will need to be more careful here.

We identify syntactical expressions with binary strings. We encode binary strings by positive integers numbers. A positive integer n of the form $1a_{k-1}\ldots a_0$ in binary notation encodes the binary string $a_{k-1}\ldots a_0$. We note that the binary logarithm $\log (n)$ of a number n coincides with the length of the binary string that the number n encodes. For a formula $\mathsf {F}$ the number n that encodes $\mathsf {F}$ is known as the Gödel number of $\mathsf {F}$.

A proof of an arithmetical formula $\varphi$ in an arithmetical theory $\mathsf {T}$ is a list of arithmetical formulas such that it ends with $\varphi$ and every formula in the list is either an axiom of $\mathsf {T}$, or is an axiom of predicate calculus, or is obtained by inference rules from previous formulas.

We will be interested in formalization of provability in the theory $\mathsf {PA}$ and its extensions by finitely many axioms. We take the standard axiomatization of $\mathsf {PA}$ (by axioms of Robinson arithmetic $\mathsf {Q}$ and the induction schema). We consider the natural axiomatization in arithmetic of the property of a number to be the Gödel number of some axiom of $\mathsf {PA}$. For all extensions $\mathsf {T}$ of $\mathsf {PA}$ by finitely many axioms this gives us $\varDelta _0$-predicates $\mathsf {Prf}_{\mathsf {T}}(x,y)$ that are natural formalizations of “x is a proof of the formula with Gödel number y in the theory $\mathsf {T}$” that is based on the definition of the notion of proof given above. And we obtain $\varSigma _1$-provability predicates

$$\begin{aligned} \mathsf {Prv}_{\mathsf {T}}(y)\leftrightharpoons \exists x\mathsf {Prf}_{\mathsf {T}}(x,y). \end{aligned}$$

We will use effective binary numerals. The n-th numeral is defined as follows:

• 1. $\underline{0}$ is the term 0;

• 2. $\underline{1}$ is the term 1;

• 3. $\underline{2n}$ is the term $(1+1)\mathop {\cdot }\underline{n}$;

• 4. $\underline{2n+1}$ is the term $(1+1)\mathop {\cdot }\underline{n}+1$.

Clearly, the length of $\underline{n}$ is $\mathcal {O}(\log (n))$.

For an arithmetical formula $\mathsf {F}$ we denote by the n-th numeral, where n is the Gödel number of the formula $\mathsf {F}$.

We denote by $\mathsf {Prv}(x)$ and $\mathsf {Prf}(x,y)$ the predicates $\mathsf {Prv}_{\mathsf {PA}}(x)$ and $\mathsf {Prf}_{\mathsf {PA}}(x,y)$.

An arithmetical evaluation is a function f(x) from $\mathsf {GL}$ formulas to the sentences of the language of first-order arithmetic such that

• 1. $f(\varphi \wedge \psi )\mathrel {\leftrightharpoons }f(\varphi )\wedge f(\psi )$;

• 2. $f(\varphi \vee \psi )\mathrel {\leftrightharpoons }f(\varphi )\vee f(\psi )$;

• 3. $f(\lnot \varphi )\mathrel {\leftrightharpoons }\lnot f(\varphi )$;

• 4. $f(\varphi \rightarrow \psi )\mathrel {\leftrightharpoons } f(\varphi \rightarrow \psi )$;

• 5. $f(\top )\mathrel {\leftrightharpoons } 0=0$;

• 6. $f(\bot )\mathrel {\leftrightharpoons } 0=1$;

• 7. .

Note that an arithmetical evaluation is uniquely determined by its values on propositional variables $u,v,\ldots$.

We will use $\top$, $\bot$, $\Box$, and $\Diamond$ within arithmetical formulas: the expression $\top$ is an abbreviation for $0=0$, the expression $\bot$ is an abbreviation for $0=1$, the expression $\Box \mathsf {F}$ is an abbreviation for , and the expression $\Diamond \mathsf {F}$ is an abbreviation for . The expressions of the form $\Box ^n \mathsf {F}$ and $\Diamond ^n \mathsf {F}$ are abbreviations for $\mathop {\underbrace{\Box \Box \ldots \Box }}\limits _{n \text{ times }}\mathsf {F}$ and $\mathop {\underbrace{\Diamond \Diamond \ldots \Diamond }}\limits _{n \text{ times }}\mathsf {F}$, respectively.

3 Proof of Solovay’s Theorem

In the section we will just give a proof of “completeness part” of Solovay’s theorem. Soundness of the logic $\mathsf {GL}$ essentially is due to Löb [Lö55] and we refer a reader to Boolos book [Boo95, Chap. 3] for a detailed proof.

Theorem 1

If a modal formula $\varphi$ is not provable in $\mathsf {GL}$ then there exists an arithmetical evaluation f(x) such that $\mathsf {PA}\nvdash f(\varphi )$.

Let us fix some modal formula $\varphi$ that is not provable in $\mathsf {GL}$. By Segerberg’s result [Seg71], we can find a finite transitive irreflexive tree $\mathfrak {F}=(W,\prec )$ such that r is the root of $\mathfrak {F}$ and there is a model $\mathbf {M}$ on $\mathfrak {F}$ with $\mathbf {M},r\nVdash \varphi$. For all the worlds a of $\mathfrak {F}$ we denote by h(a) their “height”:

$$\begin{aligned} h(a)=\sup (\{0\}\cup \{h(b)+1\mid a \prec b\}). \end{aligned}$$

Let us assign arithmetical sentences $\mathsf {C}_a$ to all the worlds a of $\mathfrak {F}$. We put $\mathsf {C}_r$ to be $0=0$. We consider a non-leaf world a and assign sentences $\mathsf {C}_b$ to all its immediate successors b. Suppose $b_0,\ldots ,b_n$ are all the immediate successors of a. We fix some enumeration $b_0,\ldots ,b_n$ such that $h(b_n)=h(a)-1$. For $i<n$ we put $\mathsf {C}_{b_{i}}$ to be the sentence

The sentence $\mathsf {C}_{b_n}$ is

$$\begin{aligned} \Box ^{h(a)}\bot \wedge \bigwedge \limits _{i<n} \lnot \mathsf {C}_{b_i}. \end{aligned}$$

Note that $\mathsf {PA}\vdash \lnot (\mathsf {C}_{b_i}\wedge \mathsf {C}_{b_j})$, for $i\ne j$ and

$$\begin{aligned} \mathsf {PA}\vdash \Box ^{h(a)}\bot \mathrel {\leftrightarrow }\bigvee \limits _{i\le n} \mathsf {C}_{b_i}. \end{aligned}$$

We note that all $\mathsf {C}_{b_i}$ are $\mathsf {PA}$-equivalent to $\varSigma _1$-sentences: it is obvious for $i\ne n$ and $\mathsf {C}_{b_n}$ is equivalent to $\varSigma _1$-sentence since it states that there is a $\mathsf {PA}+\Diamond ^{h(a)-1}\top$-proof of $0=1$ and in addition it states that the least $\mathsf {PA}+\Diamond ^{h(a)-1}\top$-proof of $0=1$ satisfy certain $\varDelta _0(\mathrm {exp})$-property.

We assign sentences $\mathsf {F}_a$ to all the worlds a of $\mathfrak {F}$. The sentence $\mathsf {F}_a$ is

$$\begin{aligned} \bigwedge \limits _{b \preceq a} \mathsf {C}_b \wedge \Diamond ^{h(a)}\top . \end{aligned}$$

It is easy to see that the disjunction of all $\mathsf {F}_a$’s is provable in $\mathsf {PA}$ and any conjunction $\mathsf {F}_a\wedge \mathsf {F}_b$, for $a\ne b$, is disprovable in $\mathsf {PA}$.

Lemma 1

For any set of worlds A we have

$$\begin{aligned} \mathsf {PA}+\Box ^{h(r)+1}\bot \vdash \Diamond \Big (\bigvee \limits _{a\in A}\mathsf {F}_a\Big ) \mathrel {\leftrightarrow } \bigvee \limits _{b,\exists a\in A(b\prec a)}\mathsf {F}_b. \end{aligned}$$

Let us first prove Theorem 1 using Lemma 1 and only then prove the lemma.

Proof

For a variable v we assign the evaluation f(v):

$$\begin{aligned} \bigvee \limits _{\mathbf {M},a\Vdash v}\mathsf {F}_a. \end{aligned}$$

By induction on the length of modal formulas $\psi$ we prove that

$$\begin{aligned} \mathsf {PA}+\Box ^{h(r)+1}\bot \vdash f(\psi ) \mathrel {\leftrightarrow } \bigvee \limits _{\mathbf {M},a\Vdash \psi }\mathsf {F}_a. \end{aligned}$$

The only non-trivial case for the induction step is when the topmost connective of $\psi$ is modality. Assume $\psi$ is of the form $\Box \chi$. From inductive assumption we know that

$$\begin{aligned} \mathsf {PA}\vdash \Box ^{h(r)+1}\bot \rightarrow (f(\chi ) \mathrel {\leftrightarrow } \bigvee \limits _{\mathbf {M},a\Vdash \chi }\mathsf {F}_a). \end{aligned}$$

We use Lemma 1:

$$\begin{aligned} \begin{aligned} \mathsf {PA}+\Box ^{h(r)+1}\bot \vdash f(\Box \chi )&\mathrel {\leftrightarrow } \Box (f(\chi ))\\&\mathrel {\leftrightarrow } \Box (\Box ^{h(r)+1}\bot \wedge f(\chi ))\\&\mathrel {\leftrightarrow } \Box (\Box ^{h(r)+1}\bot \wedge \bigvee \limits _{\mathbf {M},a\Vdash \chi }\mathsf {F}_a)\\&\mathrel {\leftrightarrow } \Box (\bigvee \limits _{\mathbf {M},a\Vdash \chi }\mathsf {F}_a)\\&\mathrel {\leftrightarrow } \Box (\lnot \bigvee \limits _{\mathbf {M},a\Vdash \lnot \chi }\mathsf {F}_a)\\&\mathrel {\leftrightarrow } \lnot \Diamond (\bigvee \limits _{\mathbf {M},a\Vdash \lnot \chi }\mathsf {F}_a)\\&\mathrel {\leftrightarrow } \lnot \bigvee \limits _{\mathbf {M},a\Vdash \Diamond \lnot \chi }\mathsf {F}_a.\\&\mathrel {\leftrightarrow } \bigvee \limits _{\mathbf {M},a\Vdash \Box \chi }\mathsf {F}_a.\\ \end{aligned} \end{aligned}$$

Therefore,

$$\begin{aligned} \mathsf {PA}+\Box ^{h(r)+1}\bot \vdash f(\varphi ) \mathrel {\leftrightarrow } \bigvee \limits _{\mathbf {M},a\Vdash \varphi }\mathsf {F}_a. \end{aligned}$$

Since $\mathbf {M},r\nVdash \varphi$, we have $\mathsf {PA}+\Box ^{h(r)+1}\bot +\mathsf {F}_r\vdash \lnot f(\varphi )$. The sentence $\mathsf {F}_r$ is just equivalent to $\Diamond ^{h(r)}\top$. Hence, by Gödel’s Second Incompleteness Theorem for $\mathsf {PA}+ \Diamond ^{h(r)}\top$, the theory $\mathsf {PA}+\Box ^{h(r)+1}\bot +\mathsf {F}_r$ is consistent. Therefore, $\lnot f(\varphi )$ is consistent with $\mathsf {PA}$ and thus $\mathsf {PA}\nvdash f(\varphi )$.

In order to prove Lemma 1, clearly, it will be enough to prove the following two lemmas:

Lemma 2

For any world a from $\mathfrak {F}$, we have

$$\begin{aligned} \mathsf {PA}+\Box ^{h(r)+1}\bot \vdash \Diamond \mathsf {F}_a \rightarrow \bigvee \limits _{b\prec a}\mathsf {F}_b. \end{aligned}$$

Proof

Let us reason in $\mathsf {PA}+\Box ^{h(r)+1}\bot$. Assume $\Diamond \mathsf {F}_a$. We need to prove $\bigvee \limits _{b\prec a}\mathsf {F}_b$. Let us denote by $r=c_0 \prec c_1 \prec \ldots \prec c_n=a$ the maximal chain from r to a. Let us find the greatest k such that $\mathsf {C}_{c_k}$ holds.

Note that for any $1\le i \le n$ the sentence $\Box ^{h(c_{i-1})}\bot$ implies $\mathsf {C}_{c_i}$. Indeed, $\Box ^{h(c_{i-1})}\bot$ implies that $\mathsf {C}_{c}$ for some immediate successor c of $c_{i-1}$. But since $\mathsf {C}_c$ is $\varSigma _1$ and we assumed $\Diamond \mathsf {F}_a$, we would have $\Diamond (\mathsf {F}_a \wedge \mathsf {C}_c)$, which is possible only for $c=c_i$.

By a simple check of cases $k=0$ and $k\ne 0$ we obtain $\Box ^{h(c_k)+1}\bot$. Therefore, for all $i<k$, we have $\Box ^{h(c_i)}\bot$ and hence, for all $i\le k$, the sentence $\mathsf {C}_{c_i}$ holds. From $\Box ( \mathsf {F}_a\rightarrow \Diamond ^{h(a)}\top )$ and $\Diamond \mathsf {F}_a$ we derive $\Diamond ^{h(a)+1}\top$. Thus, $\lnot \mathsf {C}_a$ and hence $k<n$. Since $\Box ^{h(c_k)}\bot$ implies $C_{c_{k+1}}$, we have $\Diamond ^{h(c_k)}\top$. Therefore the sentence $\mathsf {F}_{c_k}$ holds and finally we derive $\bigvee \limits _{b\prec a}\mathsf {F}_b$.

Lemma 3

For any worlds $a\prec b$, we have $\mathsf {PA}+\Box ^{h(r)+1}\bot \vdash \mathsf {F}_a \rightarrow \Diamond \mathsf {F}_b$.

We will use model-theoretic methods in our proof of Lemma 3. More precisely, we will need to use within $\mathsf {PA}$ some facts that we will establish using model-theoretic methods. There is an approach to formalization in arithmetic of results obtained by model-theoretic methods that is based on the use of the systems of the second-order arithmetic. In particular there is a well-known system $\mathsf {ACA_0}$ that is a conservative extension of $\mathsf {PA}$. We will use the formalization of model-theoretic notions in systems of second-order arithmetic that could be found in Simpson book [Sim09, Sects. II.8 and IV.3].

The key model-theoretic result that we use is the Injecting Inconsistencies Theorem. We will use the version of the theorem that is a corollary of the version of the theorem that were proved by Visser and Verbrugge [VV94, Theorem 5.1]. Earlier similar results are due to Hájek, Solovay, Krajíček, and Pudlák [Há84, Sol89, KP89].

Definition 1

Suppose $\mathfrak {M}$ is a model of $\mathsf {PA}$. We denote by $\mathfrak {M}\upharpoonright a$ the structure with the domain $\{e\in \mathfrak {M}\mid \mathfrak {M}\models e\le a\}$ the constant 0 and partial functions S, $+$, and $\cdot$ induced by $\mathfrak {M}$ on the domain. For two structures $\mathfrak {A}$ and $\mathfrak {B}$ with the constant 0 and (maybe) partial functions S, $+$, and $\cdot$ we write

• 1. $\mathfrak {A}\subseteq \mathfrak {B}$ if the domain of $\mathfrak {A}$ is a subset of the domain of $\mathfrak {B}$ and for any arithmetical term $t(x_1,\ldots ,x_n)$ and elements $q_1,\ldots ,q_n\in \mathfrak {A}$:

  • (a) if p is the value of $t(q_1,\ldots ,q_n)$ in $\mathfrak {B}$ and $p\in \mathfrak {A}$ then the value of $t(q_1,\ldots ,q_n)$ is defined in $\mathfrak {A}$ and is equal to p,

  • (b) if p is the value of $t(q_1,\ldots ,q_n)$ in $\mathfrak {A}$ then the value of $t(q_1,\ldots ,q_n)$ is defined in $\mathfrak {B}$ and is equal to p;

• 2. $\mathfrak {A}= \mathfrak {B}$ if $\mathfrak {A}\subseteq \mathfrak {B}$ and $\mathfrak {B}\subseteq \mathfrak {A}$.

We note that the definition actually could also be applied to models of $\mathsf {I\Delta _0}$.

We will show in Appendix B that the following theorem is formalizable in $\mathsf {ACA}_0$:

Theorem 2

Let T be an extension of $\mathsf {PA}$ by finitely many axioms. Let $\mathsf {Con}_{\mathsf {T}}(x)$ denote the formula . Let $\mathfrak {M}$ be a non-standard countable model of $\mathsf {T}$. And let q, p be nonstandard elements of $\mathfrak {M}$ such that $\mathfrak {M}\models q\le p$ and $\mathfrak {M}\models \mathsf {Con}_{\mathsf {T}}(p^k)$, for all standard k. Then there exists a countable model $\mathfrak {N}$ of $\mathsf {T}$ such that $p\in \mathfrak {N}$ and

• 1. $\mathfrak {M}\upharpoonright p =\mathfrak {N} \upharpoonright p$;

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

• 3. $\mathfrak {N}\models \lnot \mathsf {Con}_{\mathsf {T}}(p^q)$;

• 4. $\mathfrak {N}\models \mathsf {Con}_{\mathsf {T}}(p^k)$, for all standard k.

Let us now prove Lemma 3 using the formalization of Theorem 2.

Proof

It would be enough to prove the lemma for the case when b is an immediate successor of a. Indeed, after that we will be able to derive $\Diamond ^n\mathsf {F}_b$ for any b, $a\prec b$, where n is the length of the maximal chain from a to b; next we could conclude that we have the required $\Diamond \mathsf {F}_b$.

Now let us consider the case when b is an immediate successor of a and is $b_k$ in our fixed order $b_0,\ldots ,b_n$ of the immediate successors of a.

For the rest of the proof we reason in $\mathsf {ACA_0}+\mathsf {F}_a+\Box ^{h(r)+1}\bot$ in order to show that we have $\Diamond \mathsf {F}_b$; since $\mathsf {ACA_0}$ is a conservative extension of $\mathsf {PA}$, this will conclude the proof.

Since we have $\Diamond ^{h(a)}\top$, we could construct a model $\mathfrak {M}$ of $\mathsf {PA}+\Diamond ^{h(a)-1}\top$. Suppose $v\in \mathfrak {M}$ is the least $\mathsf {PA}+\Diamond ^{h(a)-1}\top$-proof of $0=1$ in $\mathfrak {M}$, if there exists one and an arbitrary nonstandard number, otherwise. Note that since we have $\Diamond ^{h(a)}\top$, the element v couldn’t be standard. Next we find some nonstandard $u\in \mathfrak {M}$ such that

• 1. $\mathfrak {M}\models \mathrm {exp}(\mathrm {exp}(u))<v$,

• 2. $\mathfrak {M} \models \log ^{\star } (u+1)\equiv k-1 \;\; (\mathrm {mod} \;\;n+1)$,

• 3. $\mathfrak {M} \models \log ^{\star } (u)\equiv k-2 \;\; (\mathrm {mod} \;\;n+1)$.

We can find u with this properties since we know that the functions $\mathrm {exp}(x)$ and $\mathrm {exp}^{\star }(x)$ are total on standard natural numbers and hence we know that the functions $\log (x)$ and $\log ^{\star }(x)$ map nonstandard elements to nonstandard elements in $\mathfrak {M}$.

Now we apply Theorem 2 to the model $\mathfrak {M}$ with $p=u$ and $q=\log (u)+1$. We obtain a model $\mathfrak {M}'$ of $\mathsf {PA}+\Diamond ^{h(a)-1}\top$ such that $\mathfrak {M}\upharpoonright u=\mathfrak {M}'\upharpoonright u$ and there is the least $\mathsf {PA}+\Diamond ^{h(a)-1}\top$-proof $d\in \mathfrak {M}'$ of $0=1$ such that

$$\begin{aligned} \mathfrak {M}'\models u+1<u^2<\log (d)\le u^{\log (u)+1}\le \mathrm {exp}((\log (u)+1)^2)< \mathrm {exp}(u). \end{aligned}$$

Thus,

$$\begin{aligned} \mathfrak {M}'\models \log ^{\star } (d)\equiv k \;\; (\mathrm {mod} \;\;n+1). \end{aligned}$$

If $h(b)=h(a)-1$, then we have constructed a model of $\mathsf {PA}+\mathsf {C}_b+\Diamond ^{h(b)}\top$.

Assume $h(b)<h(a)-1$. Clearly, there are no $\mathsf {PA}+\Diamond ^{h(b)}\top$-proofs of $0=1$ in $\mathfrak {M}'$. We apply Theorem 2 to $\mathfrak {M}'$ with $p=d^{\log (d)+1}$ and $q=\log (d)+1$. We obtain a model $\mathfrak {M}''$ of $\mathsf {PA}+\Diamond ^{h(b)}\top$ such that

$$\begin{aligned} \mathfrak {M}'\upharpoonright d^{\log (d)+1}=\mathfrak {M}''\upharpoonright d^{\log (d)+1}, \end{aligned}$$

there is a $\mathsf {PA}+\Diamond ^{h(b)}\top$-proof of $0=1$ in $\mathfrak {M}''$ and for the least $\mathsf {PA}+\Diamond ^{h(b)}\top$-proof $e\in \mathfrak {M}''$ of $0=1$ we have

$$\begin{aligned} \mathfrak {M}''\models \log (e)\le d^{(\log (d)+1)^2}\le \mathrm {exp}((\log (d)+1)^3)<\mathrm {exp}(d). \end{aligned}$$

Since $\mathfrak {M}'\upharpoonright d^{\log (d)+1}=\mathfrak {M}''\upharpoonright d^{\log (d)+1}$ and $\mathsf {Prf}(x,y)$ is a $\varDelta _0$ predicate, we see that d is the least $\mathsf {PA}+\Diamond ^{h(a)-1}\top$-proof of $0=1$ in $\mathfrak {M}''$. Hence $\mathfrak {M}''$ is a model of $\mathsf {PA}+\mathsf {C}_b+\Diamond ^{h(b)}\top$.

Thus, under no additional assumptions, we have a model of $\mathsf {PA}+\mathsf {C}_b+\Diamond ^{h(b)}\top$. Since all $\mathsf {C}_c$, for $c\preceq a$, are $\varSigma _1$-sentences, actually we have a model of $\mathsf {PA}+\mathsf {F}_b$. Therefore, $\Diamond \mathsf {F}_b$.

4 Conclusions

In the present paper we have gave a new method of constructing arithmetical evaluations of modal formulas from a given Kripke model and proved arithmetical completeness of $\mathsf {GL}$ with respect to provability in $\mathsf {PA}$ using the method. We consider the evaluations that have been constructed in the paper to be more “natural” than the evaluations provided by Solovay’s proof.

We proved the theorem specifically for the standard provability predicate for $\mathsf {PA}$. It is unclear to author, for what exact class of provability predicates our methods are applicable. The most essential limitation for our technique seems to be the fact that it relies on the formalized version of Theorem 2. It seems very likely that for theories that are stronger than $\mathsf {PA}$ one could apply our method with only minor adjustments. In particular, it seems that for a general result one would need to modify $\mathsf {Prf}$-predicates while preserving $\mathsf {Prv}$-predicate (up to provable equivalence) in order to ensure that [VV94, Theorem 5.1] is applicable. For theories that are weaker than $\mathsf {PA}$, there are more significant problems with adopting our technique. Namely, our technique essentially relies on formalized version of the Injecting Inconsistencies Theorem. And the proofs of stronger versions of this theorem [KP89, VV94] essentially rely on the Omitting Types Theorem. We have provided a proof of the Omitting Types Theorem in $\mathsf {ACA_0}$ in Appendix A, but it is not clear whether it could be done in weaker systems. The author is not familiar with results that calibrate reverse mathematics strength of the required version of the Omitting Types Theorem. We note that reverse mathematics analysis of other version of Omitting Types Theorem have been done by Hirschfeldt et al. [HSS09], in particular from their results it follows that their version of the Omitting Types Theorem is not provable in $\mathsf {WKL_0}$ but follows from $\mathsf {RT_2^2}$ (and thus couldn’t be equivalent to $\mathsf {ACA_0}$ over $\mathsf {RCA_0}$). But nevertheless, we conjecture that the same kind of evaluations as we have gave in Sect. 3 will provide completeness of $\mathsf {GL}$ for all finitely axiomatizable extensions of $\mathsf {I\Delta _0+Exp}$.

Also, since the technique that were introduced in the paper is significantly different from Solovay’s technique, it seems plausible that it may give some advantage for some open problems, for which Solovay’s method have been the “default approach” before (see [BV06] for open problems in provability logic).

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}$.