## 1. The history of provability logic



Two strands of research have led to the birth of provability logic.
The first one stems from a paper by
 K. Godel
 (1933), where he introduces translations from intuitionistic
propositional logic into modal logic (more precisely, into the system
nowadays called S4), and briefly mentions that provability can be
viewed as a modal operator. Even earlier, C.I. Lewis started the
modern study of modal logic by introducing strict implication as a
kind of deducibility, where he may have meant deducibility in a formal
system like
 Principia Mathematica,
 but this is not clear from his writings.



The other strand starts from research in meta-mathematics: what can
mathematical theories say about themselves by encoding interesting
properties? In 1952, L. Henkin posed a deceptively simple question
inspired by
 Godel's incompleteness theorems.
 In order to formulate Henkin's question, some more background is
needed. As a reminder, Godel's first incompleteness theorem
states that, for a sufficiently strong formal theory like Peano
Arithmetic, any sentence asserting its own unprovability is in fact
unprovable. On the other hand, from "outside" the formal
theory, one can see that such a sentence is true in the standard
model, pointing to an important distinction between truth and
provability.



More formally, let \(\ulcorner A \urcorner\) denote the Godel
number of arithmetical formula \(A\), which is the result of assigning
a numerical code to \(A\). Let \(\Prov\) be the formalized provability
predicate for Peano Arithmetic, which is of the form \(\exists p \,
\Proof(p,x)\). Here, \(\Proof\) is the formalized proof predicate of
Peano Arithmetic, and \(\Proof(p,x)\) stands for "Godel
number \(p\) codes a correct proof from the axioms of Peano Arithmetic
of the formula with Godel number \(x\)". (For a more
precise formulation, see Smorynski (1985), Davis (1958).) Now,
suppose that Peano Arithmetic proves \(A \leftrightarrow \neg\)
\(\Prov (\ulcorner A \urcorner)\), then by Godel's result,
\(A\) is not provable in Peano Arithmetic, and thus it is true, for in
fact the self-referential sentence \(A\) states "I am not
provable".



Henkin on the other hand wanted to know whether anything could be said
about sentences asserting their own provability: supposing that Peano
Arithmetic proves \(B \leftrightarrow \Prov(\ulcorner B \urcorner)\),
what does this imply about \(B\)? Three years later, M. Lob took
up the challenge and answered Henkin's question in a surprising way.
Even though all sentences provable in Peano Arithmetic are indeed true
about the natural numbers, Lob showed that the formalized version
of this fact, \(\Prov(\ulcorner B \urcorner) \rightarrow B\), can be
proved in Peano Arithmetic only in the trivial case that Peano
Arithmetic already proves \(B\) itself. This result, now called
Lob's theorem, immediately answers Henkin's question. (For a
proof of Lob's theorem, see
 Section 4.)
 Lob also showed a formalized version of his theorem, namely that
Peano Arithmetic proves

 

\[
\Prov(\ulcorner \Prov(\ulcorner B\urcorner ) \rightarrow B\urcorner ) 
 \rightarrow \Prov(\ulcorner B \urcorner ).
\]


In the same paper, Lob formulated three conditions on the
provability predicate of Peano Arithmetic, that form a useful
modification of the complicated conditions that Hilbert and Bernays
introduced in 1939 for their proof of Godel's second
incompleteness theorem. In the following, derivability of \(A\) from
Peano Arithmetic is denoted by \(\PA \vdash A\):


1. If \(\PA \vdash A\), then \(\PA \vdash \Prov(\ulcorner A \urcorner
)\);
2. \(\PA \vdash \Prov(\ulcorner A\rightarrow B\urcorner) \rightarrow (
\Prov(\ulcorner A \urcorner ) \rightarrow \Prov(\ulcorner B \urcorner
));\)
3. \(\PA \vdash \Prov(\ulcorner A \urcorner ) \rightarrow
\Prov(\ulcorner \Prov(\ulcorner A \urcorner ) \urcorner ).\)



These Lob conditions, as they are called nowadays, seem to cry
out for a modal logical investigation, where the modality \(\Box\)
stands for provability in PA. Ironically, the first time that the
formalized version of Lob's theorem was stated as the modal
principle

 

\[
\Box(\Box A \rightarrow A) \rightarrow \Box A
\]


was in a paper by Smiley in 1963 about the logical basis of ethics,
which did not consider arithmetic at all. More relevant
investigations, however, seriously started only almost twenty years
after publication of Lob's paper. The early 1970s saw the rapid
development of propositional provability logic, where several
researchers in different countries independently proved the most
important results, discussed in Sections
 2,
 3, and
 4.
 Propositional provability logic turned out to capture exactly what
many formal theories of arithmetic can say by propositional means
about their own provability predicate. More recently, researchers have
investigated the boundaries of this approach and have proposed several
interesting more expressive extensions of provability logic (see
 Section 5).


## 2. The axiom system of propositional provability logic



The logical language of propositional provability logic contains, in
addition to propositional atoms and the usual truth-functional
operators as well as the contradiction symbol \(\bot\), a modal
operator \(\Box\) with intended meaning "is provable in
\(T\)," where \(T\) is a sufficiently strong formal theory, let
us say Peano Arithmetic (see
 Section 4).
 \(\Diamond A\) is an abbreviation for \(\neg\,\Box\neg\, A\). Thus, the
language is the same as that of modal systems such as K and S4
presented in the entry
 modal logic.


### 2.1 Axioms and rules



Propositional provability logic is often called GL, after Godel
and Lob. (Alternative names found in the literature for
equivalent systems are L, G, KW, K4W, and PrL). The logic GL results from
adding the following axiom to the basic modal logic K:

 

\[\tag{GL}
\Box(\Box A \rightarrow A) \rightarrow \Box A.
\]


As a reminder, because GL extends K, it contains all formulas having
the form of a propositional tautology. For the same reason, GL
contains the

 

\[\tag{Distribution Axiom}
\Box(A \rightarrow B) \rightarrow (\Box A \rightarrow \Box B).
\]


Furthermore, it is closed under the Modus Ponens Rule, which allows to
derive \(B\) from \(A \rightarrow B\) and \(A\), and the
Generalization Rule, which says that if \(A\) is a theorem of GL, then
so is \(\Box A\).



The notion \(\GL \vdash A\) denotes provability of a modal formula
\(A\) in propositional provability logic. It is not difficult to see
that the modal axiom \(\Box A \rightarrow \Box\Box A\) (known as Axiom
4 of modal logic) is indeed provable in GL. To prove this, one uses
the substitution \(A \wedge \Box A\) for \(A\) in the axiom (GL).
Then, seeing that the antecedent of the resulting implication follows
from \(\Box A\), one applies the Distribution Axiom and the
Generalization Rule as well as some propositional logic. Unless
explicitly stated otherwise, in the sequel "provability
logic" stands for the system GL of propositional provability
logic.



As to the *proof theory* of provability logic, Valentini (1983)
proved that a standard sequent calculus formulation of GL obeys
*cut elimination*, which means, roughly formulated, that each
formula provable from GL in the sequent calculus also has a GL sequent
proof "without detours" (see the entry
 the development of proof theory
for a precise explanation of cut elimination). In recent years, there
has been renewed interest in the proof theory of GL, see for example
Gore and Ramanayake (2008). Cut-elimination leads to the
desirable *subformula property* for GL, because all formulas
that appear in a cut-free proof are subformulas of the endsequent
formulas. 




For recent proof-theoretic investigations of provability logic based
on different cut-free sequent calculi see (Negri 2005, 2014; Poggiolesi 2009). Negri
presents two equivalent labelled sequent calculi for GL and a
syntactic proof of cut elimination. Even if a full subformula property
does not hold for these calculi because of the labelling, the usual
consequences of the subformula property can be established: The
labelled formalism allows a direct completeness proof, which can be
used to establish decidability as well as the finite model property,
which means that any formula that is not provable has
a *finite* counter-model. 



An intriguing new proof-theoretical development is Shamkanov's
expansion of sequent-style proof systems by allowing *circular
proofs* (Shamkanov 2014). Consider a sequent system for K4, the
modal system resulting from GL by replacing the axiom GL by the weaker
axiom \(\Box A \rightarrow \Box\Box A\) (axiom 4). However, suppose
that open hypotheses are allowed, provided that the same sequent
occurs strictly below that hypothesis in the proof tree. Formulated
more technically, one can find a circular derivation from an ordinary
derivation tree by linking each of its non-axiomatic leaves with an
identical interior node. Shamkanov (2014) proved that the resulting
system is consistent and that moreover, in general, each sequent has a
GL-derivation if and only if it has a circular K4-derivation. Circular
proofs also provide a method to show proof-theoretically that Lyndon's
interpolation theorem holds for GL. Standard interpolation for GL 
had already been proved before by different methods (Boolos 1979; 
Smorynski 1978; Rautenberg 1983). (For more information
about Lyndon's interpolation theorem for first-order logic, see also the entry
 first-order model theory ).


### 2.2 The fixed point theorem



The main "modal" result about provability logic is the
fixed point theorem, which D. de Jongh and G. Sambin independently
proved in 1975 (Sambin 1976). Even though it is formulated and proved by strictly
modal methods, the fixed point theorem still has great arithmetical
significance. It says essentially that self-reference is not really
necessary, in the following sense. Suppose that all occurrences of the
propositional variable \(p\) in a given formula \(A(p)\) are under the
scope of the provability operator, for example \(A(p) = \neg\Box p\),
or \(A(p) = \Box(p \rightarrow q)\). Then there is a formula \(B\) in
which \(p\) does not appear, such that all propositional variables
that occur in \(B\) already appear in \(A(p)\), and such that



\[ 
\GL \vdash B \leftrightarrow A(B).
\]


This formula \(B\) is called a *fixed point* of \(A(p)\).
Moreover, the fixed point is unique, or more accurately, if there is
another formula \(C\) such that \( \GL \vdash C \leftrightarrow
A(C)\), then we must have \( \GL \vdash B \leftrightarrow C\). Most
proofs in the literature give an algorithm by which one can compute
the fixed point (see Smorynski 1985, Boolos 1993, Sambin and
Valentini 1982, Lindstrom 2006). A particularly short and clear proof, as well as a
very efficient algorithm to compute fixed points, can be found in
Reidhaar-Olson (1990). 



For example, suppose that \(A(p) = \neg \, \Box p\). Then the fixed point
produced by such an algorithm is \(\neg \, \Box\bot\), and indeed one can
prove that

 

\[
\GL \vdash \neg\,\Box\bot \leftrightarrow \neg\,\Box(\neg\,\Box\bot).
\]


If this is read arithmetically, the direction from left to right is
just the formalized version of Godel's second incompleteness
theorem: if a sufficiently strong formal theory \(T\) like Peano
Arithmetic does not prove a contradiction, then it is not provable in
\(T\) that \(T\) does not prove a contradiction. Thus, sufficiently
strong consistent arithmetical theories cannot prove their own
consistency. We will turn to study the relation between provability
logic and arithmetic more precisely in
 Section 4,
 but to that end another "modal" aspect of GL needs to be
provided first: semantics.


## 3. Possible worlds semantics and topological semantics



Provability logic has suitable possible worlds semantics, just like
many other modal logics. As a reminder, a possible worlds model (or
Kripke model) is a triple \(M = \langle W,R,V \rangle\), where \(W\)
is a non-empty set of possible worlds, \(R\) is a binary accessibility
relation on \(W\), and \(V\) is a valuation that assigns a truth value
to each propositional variable for each world in \(W\). The pair \(F =
\langle W,R \rangle\) is called the frame of this model. The notion of
truth of a formula \(A\) in a model \(M\) at a world \(W\), notation
\(M,w \models A\), is defined inductively. Let us repeat only the most
interesting clause, the one for the provability operator \(\Box\):



\[
M,w \models \Box A \text{ iff for every } w', 
 \text{ if } wRw', \text{ then } M,w' \models A.
\]


See the entry
 modal logic
 for more information about possible worlds semantics in general.


### 3.1 Characterization and modal soundness



The modal logic K is valid in all Kripke models. Its extension GL
however, is not: we need to restrict the class of possible worlds
models to a more suitable one. Let us say that a formula \(A\) is
valid in frame \(F\), notation \(F \models A\), iff \(A\) is true in
all worlds in Kripke models \(M\) based on \(F\). It turns out that
the new axiom (GL) of provability logic corresponds to a condition on
frames, as follows:



For all frames \(F = \langle W,R \rangle, F \models \Box(\Box p
\rightarrow p) \rightarrow \Box p\) iff \(R\) is transitive and
conversely well-founded. 



Here, *transitivity* is the well-known property that for all
worlds \(w\_1\), \(w\_2\), \(w\_3\) in \(W\), if \(w\_1 Rw\_2\) and \(w\_2
Rw\_3\), then \(w\_1 Rw\_3\). A relation is *conversely
well-founded* iff there are no infinite ascending sequences, that
is sequences of the form \(w\_1 Rw\_2 Rw\_3 R \ldots\). Note that
conversely well-founded frames are also irreflexive, for if \(wRw\),
this gives rise to an infinite ascending sequence
\(wRwRwR\ldots\).



The above correspondence result immediately shows that GL is modally
sound with respect to the class of possible worlds models on
transitive conversely well-founded frames, because all axioms and
rules of GL are valid on such models. The question is whether
completeness also holds: for example, the formula \(\Box A \rightarrow
\Box\Box A\), which is valid on all transitive frames, is indeed
provable in GL, as was mentioned in
 Section 1.
 But is *every* formula that is valid on all transitive
conversely well-founded frames also provable in GL?


### 3.2 Modal completeness



Unaware of the arithmetical significance of GL, K. Segerberg proved in
1971 that GL is indeed complete with respect to transitive conversely
well-founded frames; D. de Jongh and S. Kripke independently proved
this result as well. Segerberg showed that GL is complete even with
respect to the more restricted class of finite transitive irreflexive
trees, a fact which later turned out to be very useful for Solovay's
proof of the arithmetical completeness theorem (see
 Section 4).



The modal soundness and completeness theorems immediately give rise to
a decision procedure to check for any modal formula \(A\) whether
\(A\) follows from GL or not, by depth-first search through
irreflexive transitive trees of bounded depth. Looking at the
procedure a bit more precisely, it can be shown that GL is decidable
in the computational complexity class PSPACE, like the well-known
modal logics K, T and S4. This means that there is a Turing machine
that, given a formula \(A\) as input, answers whether \(A\) follows
from GL or not; the size of the memory that the Turing machine needs
for its computation is only polynomial in the length of \(A\). One can
show that the decision problem for GL (again, like the decision
problems for K, T and S4) is PSPACE-*complete*, in the sense
that all other problems in PSPACE are no harder than deciding whether
a given formula is a theorem of GL. (See Gore and Kelly (2007)
for the description of an automated theorem prover for GL.)



To give some more perspective on complexity, the class P of functions
computable in an amount of time polynomial in the length of the input,
is included in PSPACE, which in turn is included in the class EXPTIME
of functions computable in exponential time (see the entry
 computability and complexity).
 It remains a famous open problem whether these two inclusions are
strict, although many complexity theorists believe that they are. Some
other well-known modal logics, like epistemic logic with common
knowledge, are decidable in EXPTIME, thus they may be more complex
than GL, depending on the open problems.


### 3.3 Failure of strong completeness



Many well-known modal logics \(S\) are not only complete with respect
to an appropriate class of frames, but even *strongly
complete*. In order to explain strong completeness, we need the
notion of *derivability from a set of assumptions*. A formula
\(A\) is derivable from the set of assumptions \(\Gamma\) in a modal
logic \(S\), written as \(\Gamma \vdash A\), if \(A\) is in \(\Gamma\)
or \(A\) follows from formulas in \(\Gamma\) and axioms of \(S\) by
applications of Modus Ponens and the Generalization Rule. Here, the
Generalization Rule can only be applied to derivations without
assumptions (see Hakli and Negri 2010).



Now a modal logic \(S\) is *strongly complete* if for all
(finite or infinite) sets \(\Gamma\) and all formulas \(A\):



If, on appropriate \(S\)-frames, \(A\) is true in all worlds in which
all formulas of \(\Gamma\) are true, then \(\Gamma \vdash A\) in the
logic \(S\). 



This condition holds for systems like K, M, K4, S4, and S5. If
restricted to finite sets \(\Gamma\), the above condition corresponds
to completeness.



Strong completeness does not hold for provability logic, however,
because *semantic compactness* fails. Semantic compactness is
the property that for each infinite set \(\Gamma\) of formulas,



If every finite subset \(\Delta\) of \(\Gamma\) has a model on an
appropriate \(S\)-frame, then \(\Gamma\) also has a model on an
appropriate \(S\)-frame. 



As a counterexample, take the infinite set of formulas

 

\[
\Gamma = \{\Diamond p\_0,
 \Box(p\_0 \rightarrow \Diamond p\_1),
 \Box(p\_1 \rightarrow \Diamond p\_2),
 \Box(p\_2 \rightarrow \Diamond p\_3), \ldots,
 \Box(p\_n \rightarrow \Diamond p\_{n+1}), \ldots\}
\]


Then for every finite subset \(\Delta\) of \(\Gamma\), one can
construct a model on a transitive, conversely well-founded frame and a
world in the model where all formulas of \(\Delta\) are true. So by
modal soundness, GL does not prove \(\bot\) from \(\Delta\) for any
finite \(\Delta \subseteq \Gamma\), and *a fortiori* GL does
not prove \(\bot\) from \(\Gamma\), as any GL-proof is finite. On the
other hand, it is easy to see that there is no model on a transitive,
conversely well-founded frame where in any world, all formulas of
\(\Gamma\) hold. Thus \(\bot\) follows semantically from \(\Gamma\),
but is not provable from it in GL, contradicting the condition of
strong completeness.


### 3.4 Topological semantics for provability logic



As an alternative to possible worlds semantics, many modal logics may
be given topological semantics. Clearly, propositions can be
interpreted as subsets of a topological space. It is also easy to see
that the propositional connective \(\wedge\) corresponds to the
set-theoretic operation \(\cap\), while \(\vee\) corresponds to
\(\cup\), \(\neg\) corresponds to the set-theoretic complement, and
\(\rightarrow\) corresponds to \(\subseteq\). Modal logics that
contain the reflection axiom \(\Box A \rightarrow A\) enjoy a
particularly natural interpretation of the modal operators as well.
For these logics, \(\Diamond\) corresponds to the closure operator in
a topological space, while \(\Box\) corresponds to the interior. To
see why these interpretations are appropriate, notice that the
reflection axiom corresponds to the fact that each set is included in
its closure and each set includes its interior.



However, provability logic does *not* prove reflection, as the
instantiation \(\Box\bot \rightarrow \bot\) of reflection would lead
to a contradiction with the axiom (GL).



Provability logic therefore needs a different approach. Based on a
suggestion by J. McKinsey and A. Tarski (1944), L. Esakia (1981, 2003)
investigated the interpretation of \(\Diamond\) as the derived set
operator \(d\), which maps a set \(B\) to the set of its limit points
\(d(B)\). To explain the consequences of this interpretation of
\(\Diamond\), we need two more definitions, namely of the concepts
*dense-in-itself* and *scattered*. A subset \(B\) of a
topological space is called *dense-in-itself* if \(B \subseteq
d(B)\). A topological space is called *scattered* if it has no
non-empty subset that is dense-in-itself. The ordinals in their
interval topology form examples of scattered spaces. Esakia (1981)
proved an important correspondence: he showed that a topological space
*satisfies the axiom GL* if and only if the space is
*scattered*. This correspondence soon led to the result,
independently found by Abashidze (1985) and Blass (1990), that
provability logic is complete with respect to any ordinal \(\ge
\omega^\omega\).



In recent years, topological semantics for provability logic has seen
a veritable revival, especially in the study of Japaridze's bimodal
provability logic GLB, an extension of GL (Japaridze 1986). The logic
GLB turns out to be *modally incomplete* with respect to its
possible worlds semantics, in the sense that it does not correspond to
any class of frames. This feature places bimodal GLB in sharp contrast
with unimodal GL, which corresponds to the class of finite transitive
irreflexive trees, as mentioned above. Beklemishev et al. (2009)
showed that GLB is, however, complete with respect to its
*topological* semantics (see also Beklemishev 2009, Icard
2011). Intriguing reverberations of Esakia's correspondence between GL
and scattered topological spaces can even be found in recent
topological studies of spatial and epistemic logics (see Aiello et al.
2007). (See
 Section 5.4
 for further discussion about GLB).


## 4. Provability logic and Peano Arithmetic



From the time GL was formulated, researchers wondered whether it was
adequate for formal theories like Peano Arithmetic (PA): does GL prove
*everything* about the notion of provability that can be
expressed in a propositional modal language and can be proved in Peano
Arithmetic, or should more principles be added to GL? To make this
notion of adequacy more precise, we define a *realization*
(sometimes called translation or interpretation) to be a function
*f* that assigns to each propositional atom of modal logic a
sentence of arithmetic, where


* \(f(\bot)=\bot;\)
* \(f\) respects the logical connectives, for example, \(f(B
\rightarrow C) = (f(B) \rightarrow f(C));\) and
* \(\Box\) is translated as the provability predicate \(\Prov\), so
\(f(\Box B) = \Prov(\ulcorner f(B)\urcorner ).\)


### 4.1 Arithmetical soundness



It was already clear in the early 1970s that GL is *arithmetically
sound* with respect to PA, formally: 

 

\[
\text{If } \GL \vdash A,
\text{then for all realizations } f, 
\PA \vdash f(A).\]


To give some taste of meta-mathematics, let us sketch the soundness
proof.



**Proof sketch of arithmetical soundness**. PA indeed
proves realizations of propositional tautologies, and provability of
the Distribution Axiom of GL translates to

 

\[
\PA \vdash \Prov(\ulcorner A \rightarrow B\urcorner )
 \rightarrow (\Prov(\ulcorner A\urcorner ) \rightarrow \Prov(\ulcorner B\urcorner ))
\]


for all formulas *A* and *B*, which is just Lob's
second derivability condition (see
 Section 1).
 Moreover, PA obeys Modus Ponens, as well as the translation of the
Generalization Rule:

 

\[
\text{If }
 \PA \vdash A,
\text{then }
 \PA \vdash \Prov(\ulcorner A\urcorner ),
\]


which is just Lob's first derivability condition. Finally, the
translation of the main axiom (GL) is indeed provable in PA:



\[
\PA \vdash \Prov(\ulcorner \Prov(\ulcorner A\urcorner )
 \rightarrow A\urcorner ) \rightarrow 
\Prov(\ulcorner A\urcorner ).
\]


This is exactly the formalized version of Lob's theorem mentioned
in
 Section 1.



Let us give a sketch of the proof of Lob's theorem itself from
his derivability conditions (the proof of the formalized version is
similar). The proof is based on Godel's diagonalization lemma,
which says that for any arithmetical formula \(C(x)\) there is an
arithmetical formula \(B\) such that

 

\[
\PA \vdash B \leftrightarrow C(\ulcorner B\urcorner ).
\]


In words, the formula \(B\) says "I have property
\(C\)."



**Proof of Lob's theorem:**. Suppose that \(\PA
\vdash \Prov(\ulcorner A\urcorner ) \rightarrow A\); we need to show
that \(\PA \vdash A\). By the diagonalization lemma, there is a
formula \(B\) such that

 

\[
\PA \vdash B \leftrightarrow (\Prov(\ulcorner B\urcorner ) 
 \rightarrow A).
\]


From this it follows by Lob's first and second derivability
conditions plus some propositional reasoning that

 

\[
\PA \vdash \Prov(\ulcorner B\urcorner ) \leftrightarrow 
 \Prov(\ulcorner \Prov(\ulcorner B\urcorner ) 
 \rightarrow A\urcorner ).
\]


Thus, again by Lob's second condition,

 

\[
\PA \vdash \Prov(\ulcorner B\urcorner )
 \rightarrow (\Prov(\ulcorner \Prov(\ulcorner B\urcorner )
 \urcorner ) \rightarrow 
 \Prov(\ulcorner A\urcorner )).
\]


On the other hand Lob's third condition gives

 

\[
\PA \vdash \Prov(\ulcorner B\urcorner ) \rightarrow 
 \Prov(\ulcorner \Prov(\ulcorner B\urcorner )\urcorner ),
\]


thus

 

\[
\PA \vdash \Prov(\ulcorner B\urcorner ) \rightarrow 
 \Prov(\ulcorner A\urcorner ).
\]


Together with the assumption that \(PA \vdash \Prov(\ulcorner
A\urcorner ) \rightarrow A\), this gives

 

\[
\PA \vdash \Prov(\ulcorner B\urcorner ) \rightarrow A.
\]


Finally, the equation produced by the diagonalization lemma implies
that \(\PA \vdash B\), so \(\PA \vdash \Prov(\ulcorner B\urcorner )\),
thus

 

\[
\PA \vdash A,
\]


as desired.



Note that substituting \(\bot\) for \(A\) in Lob's theorem, we
derive that \(\PA \vdash \neg\, \Prov(\ulcorner \bot\urcorner )\) implies
\(\PA \vdash \bot\), which is just the contraposition of Godel's
second incompleteness theorem.


### 4.2 Arithmetical completeness



The landmark result in provability logic is R. Solovay's arithmetical
completeness theorem of 1976, showing that GL is indeed adequate for
Peano Arithmetic:

 

\[
\GL \vdash A
\text{ if and only if for all realizations }
f, \PA \vdash f(A).
\]


This theorem says essentially that the modal logic GL captures
everything that Peano Arithmetic can truthfully say in modal terms
about its own provability predicate. The direction from left to right,
arithmetical soundness of GL, is discussed above. Solovay set out to
prove the other, much more difficult, direction by contraposition. His
proof is based on intricate self-referential techniques, and only a
small glimpse can be given here.



The modal completeness theorem by Segerberg was an important first
step in Solovay's proof of arithmetical completeness of GL with
respect to Peano Arithmetic. Suppose that GL does not prove the modal
formula \(A\). Then, by modal completeness, there is a finite
transitive irreflexive tree such that \(A\) is false at the root of
that tree. Now Solovay devised an ingenious way to simulate such a
finite tree in the language of Peano Arithmetic. Thus he found a
realization \(f\) from modal formulas to sentences of arithmetic, such
that Peano Arithmetic does not prove \(f(A)\).



Solovay's completeness theorem provides an alternative way to
construct many arithmetical sentences that are not provable in Peano
Arithmetic. For example, it is easy to make a possible worlds model to
show that GL does not prove \(\Box p \vee \Box\neg\, p\), so by
Solovay's theorem, there is an arithmetical sentence \(f(p)\) such
that Peano Arithmetic does not prove \(\Prov(\ulcorner f(p)\urcorner )
\vee \Prov(\ulcorner \neg\, f(p)\urcorner )\). In particular, this
implies that neither \(f(p)\) nor \(\neg\, f(p)\) is provable in Peano
Arithmetic; for suppose on the contrary that \(\PA \vdash f(p)\), then
by Lob's first condition and propositional logic, \(\PA \vdash
\Prov(\ulcorner f(p)\urcorner ) \vee \Prov(\ulcorner \neg\, f(p)\urcorner
)\), leading to a contradiction, and similarly if one supposes that
\(\PA \vdash \neg\, f(p)\).



Solovay's theorem is so significant because it shows that an
interesting fragment of an undecidable formal theory like Peano
Arithmetic--namely that which arithmetic can express in
propositional terms about its own provability predicate--can be
studied by means of a decidable modal logic, GL, with a perspicuous
possible worlds semantics.


## 5. The scope of provability logic



In this section, some recent trends in research on provability logic
are discussed. One important strand concerns the limits on the scope
of GL, where the main question is, for which formal theories, other
than Peano Arithmetic, is GL the appropriate propositional provability
logic? Next, we discuss some generalizations of propositional
provability logic in more expressive modal languages.


### 5.1 Boundaries



In recent years, logicians have investigated many other systems of
arithmetic that are weaker than Peano Arithmetic. Often these
logicians took their inspiration from computability issues, for
example the study of functions computable in polynomial time. They
have given a partial answer to the question: "For which theories
of arithmetic does Solovay's arithmetical completeness theorem (with
respect to the appropriate provability predicate) still hold?"
To discuss this question, two concepts are needed.
\(\Delta\_0\)-formulas are arithmetical formulas in which all
quantifiers are bounded by a term, for example

 

\[
\forall y \le \bs\bs 0 
 \: \forall z \le y 
 \: \forall x \le y + z 
 \: (x + y \le (y+(y+z))),
\]


where \(\bs\) is the successor operator ("\(+1\)"). The
arithmetical theory \(I \Delta\_0\) (where I stands for
"induction"), is similar to Peano Arithmetic, except that
it allows less induction: the induction scheme

 

\[
A(0) \wedge \forall x\, (A(x) \rightarrow A(\bs x)) \rightarrow
 \forall x \, A(x)
\]


is restricted to \(\Delta\_0\)-formulas \(A\).



As De Jongh and others (1991) pointed out, arithmetical completeness
certainly holds for theories \(T\) that satisfy the following two
conditions:


1. \(T\) proves induction for \(\Delta\_0\)-formulas, and \(T\) proves
EXP, the formula expressing that for all \(x\), its power \(2^x\)
exists. In more standard notation: \(T\) extends \(I
\Delta\_0\)+EXP;
2. \(T\) does not prove any false sentences of the form \(\exists x\,
A(x)\), with \(A(x)\) a \(\Delta\_0\)-formula.



For such theories, arithmetical soundness and completeness of GL hold,
provided that \(\Box\) translates to \(\Prov\_T\), a natural provability
predicate with respect to a sufficiently simple axiomatization of
\(T\). Thus for modal sentences \(A\):

 

\[
\GL \vdash A
\text{ if and only if for all realizations }
 f,T \vdash f(A).
\]


It is not clear yet whether Condition 1 gives a lower bound on the
scope of provability logic. For example, it is still an open question
whether GL is the provability logic of \(I \Delta\_0+\Omega\_1\), a
theory which is somewhat weaker than \(I \Delta\_0\)+EXP in that
\(\Omega\_1\) is the axiom asserting that for all \(x\), its power
\(x^{\log(x)}\) exists. Provability logic GL is arithmetically sound
with respect to \(I \Delta\_0+\Omega\_1\), but except for some partial
results by Berarducci and Verbrugge (1993), providing arithmetic
realizations consistent with \(I \Delta\_0+\Omega\_1\) for a restricted
class of sentences consistent with GL, the question remains open. Its
answer may hinge on open problems in computational complexity
theory.



The above result by De Jongh et al. shows a strong feature of
provability logic: for many different arithmetical theories, GL
captures exactly what those theories say about their own provability
predicates. At the same time this is a weakness. For example,
propositional provability logic does not point to any differences
between those theories that are finitely axiomatizable and those that
are not.


### 5.2 Interpretability logic



In order to be able to speak in a modal language about important
distinctions between theories, researchers have extended provability
logic in many different ways. Let us mention a few. One extension is
to add a binary modality \(\interprets\), where for a given
arithmetical theory \(T\), the modal sentence \(A \interprets B\) is
meant to stand for "\(T+B\) is interpretable in \(T+A\)"
(Svejdar, 1983).
De Jongh and Veltman (1990) investigated modal semantics for several
interpretability logics, while De Jongh and Visser (1991) proved the
explicit fixed-point property for the most important ones. Visser
characterized the interpretability logic of the most common finitely
axiomatized theories, and Berarducci and Shavrukov independently
characterized the one for PA, which is not finitely axiomatizable. It
appears that indeed, the interpretability logic of finitely
axiomatizable theories is different from the interpretability logic of
Peano Arithmetic (see Montagna 1987; Visser 1990, 1998; Berarducci
1990, Shavrukov 1988; Joosten and Visser 2000).


### 5.3 Propositional quantifiers



Another way to extend the framework of propositional provability logic
is to add propositional quantifiers, so that one can express
principles like Goldfarb's:

 

\[
\forall p \,\forall q \,\exists r \: \Box((\Box p \vee \Box q) 
 \leftrightarrow \Box r),
\]


saying that for any two sentences there is a third sentence which is
provable if and only if either of the first two sentences is provable.
This principle is provable in Peano Arithmetic (see e.g. Artemov and
Beklemishev 1993). The set of sentences of GL with propositional
quantifiers that is arithmetically valid turns out to be undecidable
(Shavrukov 1997).


### 5.4 Japaridze's bimodal and polymodal provability logics



Japaridze's (1988) bimodal logic GLB has two \(\Box\)-like
provability operators, denoted by \([0]\) and \([1]\), with their dual
\(\Diamond\)-like operators \(\langle 0\rangle\) and \(\langle
1\rangle\), respectively. In Japaridze's interpretation, one can
think of \([0]\) as standing for the standard provability predicate in
Peano Arithmetic. On the other hand, \([1]\) corresponds to a stronger
provability predicate, namely \(\omega\)-*provabilty*. 



Let us define the concepts that are needed to understand this intended
interpretation of GLB. An arithmetical theory \(T\) is defined to be
\(\omega\)-*consistent* if and only if for all formulas A with
free variable \(x\), \(T\vdash \neg\, A(I\_n)\) for all \(n\) implies
that \(T \not\vdash \exists x \, A(x)\); here, \(I\_n\) is the numeral of
\(n\), i.e., the term \(\bs\bs\ldots\bs 0\) with \(n\) occurrences of
the successor operator \(\bs\). Peano Arithmetic (PA) is the most
well-known example of an \(\omega\)-consistent theory (see also
 Godel's incompleteness theorems).
 Now let PA\(^+\) be the arithmetical theory whose axioms are those of
PA together with all sentences \(\forall x \, \neg \, A(x)\) such that for
every \(n\), PA\(\vdash \neg \, A(I\_n)\). Now \(\omega\)-provability is
simply provability in PA\(^+\), so it is the dual of
\(\omega\)-consistency.



Japaridze's bimodal provability logic GLB can be axiomatized by the
axioms and rules of GL (see
 Section 2),
 formulated separately for [0] and [1]. In addition, GLB has two mixed
axioms, namely: 

\[\tag{Monotonicity}
[0] A \rightarrow [1] A
\]

 

\[\tag{\(\Pi^0\_1\)-completeness}
\langle 0\rangle A \rightarrow [1]\langle 0\rangle A
\]

 Japaridze's logic is
decidable and has a reasonable Kripke semantics, and it is
arithmetically sound and complete with respect to Peano Arithmetic
(Japaridze 1988, Boolos 1993).



A polymodal analogue of Japaridze's GLB, named GLP, has received a lot
of attention in recent years. GLP has infinitely many \(\Box\)-like
provability operators, denoted by boxes \([n]\) for every natural
number \(n\), with their dual \(\Diamond\)-like operators
\(\langle n\rangle\). Again, one can think of \([0]\) as standing for the
standard provability predicate in Peano Arithmetic, \(\langle 1\rangle\)
for \(\omega\)-provability, etcetera. GLP has been axiomatized by
starting from the axioms and rules of GL (see
 Section 2),
 formulated separately for each \([n]\). In addition, GLP has three
mixed axiom schemes, namely, as formulated by Beklemishev (2010):

\[
[m] A \rightarrow [n] A, \mbox{ for } m \leq n
\]

 

\[
\langle k\rangle A \rightarrow [n]\langle k\rangle A, \mbox{ for } k \lt n
\]

 

\[
[m] A \rightarrow [n][m] A, \mbox{ for } m \leq n
\]

 



GLP has recently been endowed with a Kripke semantics with respect to
which it is complete, and has also been shown to be arithmetically
complete with respect to Peano Arithmetic (see Beklemishev 2010a,
2011a). Just like for GL, the decision problem for GLP is
PSPACE-complete (Shapirovsky 2008), while its closed fragment is
polynomial time decidable (Pakhomov 2014).



In recent years a number of results have been proved about the
polymodal logic GLP of strong provability predicates. Here follow some
particularly fruitful topics:


* the closed fragment of GLP (see Ignatiev 1993; Beklemishev,
Joosten and Vervoort 2005);
* GLP and proof-theoretic ordinals (Beklemishev 2004);
* Interpolation theorems for GLP (see Beklemishev 2010b, Shamkanov
2011);
* The relationship between topological semantics and set theory,
among others particular large cardinal axioms and stationary
reflection (see Beklemishev 2011b; Beklemishev and Gabelaia 2013,
2014; Fernandez-Duque 2014).


### 5.5 Predicate provability logic



Finally, one can of course study predicate provability logic. The
language is that of predicate logic without function symbols, together
with the operator \(\Box\). Here, the situation becomes much more
complex than in the case of propositional provability logic. To begin
with, the straightforward quantified version of GL does not have the
fixed-point property, is not complete with respect to any class of
Kripke frames, and is not arithmetically complete with respect to
Peano Arithmetic (Montagna, 1984). The question then arises: Is there
any nicely axiomatized predicate provability logic that is adequate,
proving exactly the valid principles of provability? The answer is
unfortunately a resounding no: Vardanyan (1986) has proved on the
basis of ideas by Artemov (1985a) that the set of sentences of
predicate provability logic all of whose realizations are provable in
PA is not even recursively enumerable but \(\Pi^0\_2\)-complete, so it
has no reasonable axiomatization. Visser and De Jonge (2006) showed
that there is no escape from Vardanyan's theorem by proving a
generalization: For a wide range of arithmetical theories \(T\), the
set of sentences of predicate provability logic all of whose
realizations are provable in \(T\) turns out to be
\(\Pi^0\_2\)-complete as well. 


### 5.6 Other generalizations



Left out in the above discussion are many other important strands of
research in provability logic and its extensions. The interested
reader is pointed to the following areas: 


* the provability logic of intuitionistic arithmetic (see Troelstra
1973; Visser 1982, 1999; Iemhoff 2000, 2001, 2003; Visser 2002,
2008);
* classification of provability logics (see Visser 1980, Artemov
1985b, Beklemishev 1989, Beklemishev et al. 1999);
* Rosser orderings and proof speed-up (see Guaspari and Solovay
1979, Svejdar 1983, Montagna 1992);
* several kinds of bimodal provability logics with provability
operators for different theories (see Carlson 1986; Smorynski
1985; Beklemishev 1994, 1996);
* provability logics for standard provability combined with unusual
provability predicates externally enumerating PA, such as Feferman's
and Parikh's provability predicates and slow provability predicates
(see Montagna 1978; Visser 1989; Shavrukov 1994; Lindstrom 1994,
2006; Henk and Pakhomov 2016 (Other Internet Resources));
* the logic of explicit proofs (see Artemov 1994, 2001; Artemov and
Montagna 1994; Artemov and Iemhoff 2007);
* applications of provability logic in proof theory (see Beklemishev
1999, 2004, 2005, 2006);
* positive provability logics and reflection calculus (see
Beklemishev 2012, 2014; Dashkov 2012);
* generalizations of the polymodal provability logic GLP, namely
provability logics with transfinitely many modalities (see Beklemishev
et al. 2014; Fernandez-Duque and Joosten 2013a, 2013b, 2013
(Other Internet Resources), 2014);
* relations between provability logic and the \(\mu\)-calculus (see van
Benthem 2006, Visser 2005, Alberucci and Facchini 2009); and
* provability algebras, also called diagonalizable algebras or
Magari algebras (see Magari 1975a, 1975b; Montagna 1979, 1980a, 1980b;
Shavrukov 1993a, 1993b, 1997; Zambella 1994; for recent results on
their elementary theories, see Pakhomov 2012, 2014 (Other Internet
Resources), 2015 (Other Internet Resources)).

 For the reader who would like to contribute to the area of
provability logic and its generalizations, Beklemishev and Visser
(2006) have proposed an annotated list of intriguing open problems.

## 6. Philosophical significance



Even though propositional provability logic is a modal logic with a
kind of "necessity" operator, it withstands Quine's (1976)
controversial critique of modal notions as unintelligible, already
because of its clear and unambiguous arithmetic interpretation. For
example, unlike for many other modal logics, formulas with nested
modalities like \(\Box\Diamond p \rightarrow \Box\bot\) are not
problematic, nor are there any disputes about which ones should be
tautologies. In fact, provability logic embodies all the desiderata
that Quine (1953) set out for syntactic treatments of modality.



Quine's main arrows were pointed towards modal predicate logics,
especially the construction of sentences that contain modal operators
under the scope of quantifiers ("quantifying in"). In
predicate provability logic, however, where quantifiers range over
natural numbers, both *de dicto* and *de re* modalities
have straightforward interpretations, contrary to the case of other
modal logics (see the note on the
 *de dicto* / *de re* distinction).
 For example, formulas like

 

\[
\forall x\, \Box\, \exists y \,(y=x)
\]


are not at all problematic. If the number \(n\) is assigned to \(x\),
then \(\Box \,\exists y\,(y = x)\) is true with respect to this assignment
iff the sentence \(\exists y\,(y=I\_n)\) is provable in Peano Arithmetic;
here, \(I\_n\) is the numeral of \(n\), i.e., the term
\(\bs\bs\ldots\bs 0\) with \(n\) occurrences of the successor operator
\(\bs\). This sentence is true for all \(n\) in the standard model of
the natural numbers, and \(\forall x \,\Box\, \exists y \,(y = x)\) is even
provable in Peano Arithmetic.



By the way, the Barcan Formula

 

\[
\forall x \,\Box\, A(x) \rightarrow \Box\, \forall x\, A(x)
\]


is not true for the integers, let alone provable (for example, take
for \(A(x)\) the formula "\(x\) does not code a proof of
\(\bot\)"). Its converse 

 

\[
\Box\, \forall x \, A(x) \rightarrow \forall x \, \Box\, A(x)
\]


on the other hand, is provable in Peano Arithmetic for any formula
\(A\). 



Provability logic has very different principles from other modal
logics, even those with a seemingly similar purpose. For example,
while provability logic captures provability in formal theories of
arithmetic,
 epistemic logic
 endeavors to describe knowledge, which could be viewed as a kind of
informal provability. In many versions of epistemic logic, one of the
most important principles is the truth axiom (5):

 

\[
\mbox{S5} \vdash \Box A \rightarrow A,
 (\text{if one knows } A, 
 \text{ then } A
 \text{ is true}).
\]


The analogous principle clearly does not hold for GL: after all, 



\[
\text{if } \GL \vdash \Box A \rightarrow A,
\text{ then } \GL \vdash A.
\]


Thus, it seems misguided to compare the strength of both notions or to
combine them in one modal system. Perhaps formal provability is indeed
in some sense a stronger notion than informal provability, but
definitely this is not an arithmetic truth or validity, nor is the
other direction. Discussions of the consequences of Godel's
incompleteness theorems sometimes involve confusion around the notion
of provability, giving rise to claims that humans could beat formal
systems in "knowing" theorems (see Davis (1990, 1993) for
good discussions of such claims).



All in all, formal provability is a precisely defined concept, much
more so than truth and knowledge. Thus,
 self-reference
 within the scope of provability does not lead to semantic paradoxes
like the Liar. Instead, it has led to some of the most important
results about mathematics, such as Godel's incompleteness
theorems.