# Provability Logic

*First published Wed Apr 2, 2003; substantive revision Tue Nov 9, 2010*

Provability logic is a modal logic that is used to investigate what arithmetical theories can express in a restricted language about their provability predicates. The logic has been inspired by developments in meta-mathematics such as Gödel's incompleteness theorems of 1931 and Löb's theorem of 1953. As a modal logic, provability logic has been studied since the early seventies, and has had important applications in the foundations of mathematics.

From a philosophical point of view, provability logic is interesting because the concept of provability in a fixed theory of arithmetic has a unique and non-problematic meaning, other than concepts like necessity and knowledge studied in modal and epistemic logic. Furthermore, provability logic provides tools to study the notion of self-reference.

- 1. The history of provability logic
- 2. The axiom system of propositional provability logic
- 3. Possible worlds semantics and topological semantics
- 4. Provability logic and Peano Arithmetic
- 5. The scope of provability logic
- 6. Philosophical significance
- Bibliography
- Academic Tools
- Other Internet Resources
- Related Entries

## 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. Gödel (1933), where he introduces a translation 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 Gödel's incompleteness theorems. In order to formulate Henkin's question, some more background is needed. As a reminder, Gödel'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
^{⌈}*A*^{⌉}
denote the Gödel 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
∃*p**Proof*(*p*,*x*). Here, *Proof* is the
formalized proof predicate of Peano Arithmetic, and
*Proof*(*p*,*x*) stands for Gödel number
*p* codes a correct proof from the axioms of Peano Arithmetic of
the formula with Gödel number *x*. (For a more precise
formulation, see Smoryński (1985), Davis (1958).) Now, suppose that
Peano Arithmetic proves *A*
↔¬*Prov*^{⌈}*A*^{⌉}, then by Gödel'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* ↔*Prov*(^{⌈}*B*^{⌉}), what does this imply
about *B*? Three years later, M. Löb 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, Löb showed that the formalized version of this
fact, *Prov*(^{⌈}*B*^{⌉}) → *B*, can be proved in Peano
Arithmetic only in the trivial case that Peano Arithmetic already proves
*B* itself. This result, now called Löb's theorem,
immediately answers Henkin's question. (For a proof of Löb's
theorem, see
Section 4.)
Löb also showed a
formalized version of his theorem, namely that Peano Arithmetic
proves

Prov(^{⌈}Prov(^{⌈}B^{⌉}) →B^{⌉})→Prov(^{⌈}B^{⌉}).

In the same paper, Löb 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 Gödel's second
incompleteness theorem. In the following, derivability of *A*
from Peano Arithmetic is denoted by
PA ⊢ *A*:

- If
PA ⊢
*A*, then PA ⊢*Prov*(^{⌈}*A*^{⌉}); - PA ⊢
*Prov*(^{⌈}*A*→*B*^{⌉}) →(*Prov*(^{⌈}*A*^{⌉}) →*Prov*(^{⌈}*B*^{⌉})); - PA ⊢
*Prov*(^{⌈}*A*^{⌉}) →*Prov*(^{⌈}*Prov*(^{⌈}*A*^{⌉})^{⌉}).

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

□(□A→A) → □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 Löb's paper. The early seventies 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. 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 ⊥, a modal operator
□ with intended meaning “is provable in *T*,”
where *T* is a sufficiently strong formal theory, let us say
Peano Arithmetic (see
Section 4).
◊*A* is
an abbreviation for ¬□¬*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 Gödel and Löb. (Alternative names found in the literature for equivalent systems are L, KW, K4W, and PrL). The logic GL results from adding the following axiom to the basic modal logic K:

(GL) □(□A→A) → □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

Distribution Axiom: □(A→B) → (□A→ □B).

Furthermore, it is closed under the Modus Ponens Rule, allowing to
derive *B* from *A* → *B* and *A*, and
the Generalization Rule, which says that if *A* is a theorem of
GL, then so is □*A*.

The notion GL
⊢
*A*
denotes provability of a modal formula *A* in propositional
provability logic. It is not difficult to see that the modal axiom
□*A* → □□*A* (known as Axiom 4 of
modal logic) is indeed provable in GL. To prove this, one uses the
substitution *A*∧□*A* for *A* in the axiom (GL). Then, seeing that the antecedent of the resulting implication follows from □*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.

In recent years there has been renewed interest in the *proof theory* of GL, inspired by Valentini (1983). In particular, it turns out 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 Negri (2005), Goré and Ramanayake (2008); see also the entry the development of proof theory for a precise explanation of cut elimination). This leads to the desirable *subformula property* for GL, because all formulas that appear in a cut-free proof are subformulas of the endsequent formulas.

### 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.
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*) = ¬□*p*, or
*A*(*p*) = □(*p* → *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 ⊢B↔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
⊢
*C* ↔
*A*(*C*), then we must have GL
⊢
*B*↔*C*. Most proofs in the
literature give an algorithm by which one can compute the fixed point
(see Smoryński 1985, Boolos 1993).

For example, suppose that *A*(*p*) = ¬
□*p*. Then the fixed point produced by such an algorithm
is ¬ □⊥, and indeed one can prove that

GL ⊢ ¬□⊥ ↔ ¬□(¬□⊥).

If this is read arithmetically, the direction from left to right is
just the formalized version of Gödel'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* =
⟨*W*,*R*,*V*⟩, where *W* is a 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* = ⟨*W*,*R*⟩ 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* ⊨
*A*, is defined inductively. Let us repeat only the most
interesting clause, the one for the provability operator □:

M,w⊨ □Aiff for everyw′, ifwRw′, thenM,w′ ⊨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* ⊨ *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 framesF= <W,R>,F⊨ □(□p→p) → □piffRis 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*…. Note that conversely well-founded frames are also
irreflexive, for if wRw, this gives rise to an infinite ascending
sequence *wRwRwR*….

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 □*A*
→ □□*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 Goré 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 Γ in a modal logic *S*, written as Γ
⊢ *A*, if *A* is in Γ or *A* follows from formulas in Γ 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
Γ and all formulas *A*:

If, on appropriateS-frames,Ais true in all worlds in which all formulas of Γ are true, then Γ ⊢Ain the logicS.

This condition holds for systems like K, M, K4, S4, and S5. If restricted to finite sets Γ, 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 Γ of formulas,

If every finite subset Δ of Γ has a model on an appropriateS-frame, then Γ also has a model on an appropriateS-frame.

As a counterexample, take the infinite set of formulas

Γ = {◊p_{0}, □(p_{0}→ ◊p_{1}), □(p_{1}→ ◊p_{2}), □(p_{2}→ ◊p_{3}),…, □(p_{n}→ ◊p_{n+1}),…}

Then for every finite subset Δ of Γ, one can construct a
model on a transitive, conversely well-founded frame and a world in the
model where all formulas of Δ are true. So by modal soundness, GL
does not prove ⊥ from Δ for any finite Δ ⊆
Γ, and *a fortiori* GL does not prove ⊥ from Γ,
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 Γ hold. Thus ⊥ follows
semantically from Γ, 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 ∧ corresponds to the set-theoretic operation ∩, while ∨ corresponds to ∪, ¬ corresponds to the set-theoretic complement, and → corresponds to ⊆. Modal logics that contain the reflection axiom □*A* →*A* enjoy a particularly natural interpretation of the modal operators as well. For these logics, ◊ corresponds to the closure operator in a topological space, while □ 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 □⊥ →⊥ 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 ◊ 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 ◊, 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* ⊆ *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
≥ω^{ω}.

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 2010, 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).

## 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*(⊥)=⊥;*f*respects the logical connectives, for example,*f*(*B*→*C*) = (*f*(*B*)→*f*(*C*)); and- □ is translated as the provability predicate
*Prov*, so*f*(□*B*) =*Prov*(^{⌈}*f*(*B*)^{⌉}).

### 4.1 Arithmetical soundness

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

If GL ⊢A, then for all realizationsf, PA ⊢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 ⊢Prov(^{⌈}A→B^{⌉}) →(Prov(^{⌈}A^{⌉}) →Prov(^{⌈}B^{⌉}))

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

If PA ⊢A, then PA ⊢Prov(^{⌈}A^{⌉}),

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

PA ⊢Prov(^{⌈}Prov(^{⌈}A^{⌉}) →A^{⌉}) →Prov(^{⌈}A^{⌉}).

This is exactly the formalized version of Löb's theorem mentioned in Section 1 .

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

PA ⊢B↔C(^{⌈}B^{⌉}).

In words, the formula *B* says “I have property
C.”

**Proof of Löb's theorem:**. Suppose that
PA ⊢ *Prov*(^{⌈}*A*^{⌉})→*A*; we
need to show that
PA ⊢ *A*. By
the diagonalization lemma, there is a formula *B* such that

PA ⊢B↔(Prov(^{⌈}B^{⌉})→A).

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

PA ⊢Prov(^{⌈}B^{⌉}) ↔Prov(^{⌈}Prov(^{⌈}B^{⌉}) →A^{⌉}).

Thus, again by Löb's second condition,

PA ⊢Prov(^{⌈}B^{⌉}) →(Prov(^{⌈}Prov(^{⌈}B^{⌉})^{⌉})→Prov(^{⌈}A^{⌉})).

On the other hand Löb's third condition gives

PA ⊢Prov(^{⌈}B^{⌉})→Prov(^{⌈}Prov(^{⌈}B^{⌉})^{⌉}),

thus

PA ⊢Prov(^{⌈}B^{⌉})→Prov(^{⌈}A^{⌉}).

Together with the assumption that
PA ⊢ *Prov*(^{⌈}*A*^{⌉}) →*A*, this gives

PA ⊢Prov(^{⌈}B^{⌉})→A.

Finally, the equation produced by the diagonalization lemma implies
that
PA ⊢ *B*, so
PA ⊢ *Prov*(^{⌈}*B*^{⌉}), thus

PA ⊢A,

as desired.

Note that substituting ⊥ for *A* in Löb's theorem,
we derive that
PA ⊢
¬*Prov*
(^{⌈}⊥^{⌉}) implies
PA ⊢ ⊥, which is just the contraposition of Gödel'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 ⊢Aif and only if for all realizationsf, PA ⊢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 □*p* ∨
□¬*p*, so by Solovay's theorem, there is an
arithmetical sentence *f*(*p*) such that Peano
Arithmetic does not
prove *Prov*(^{⌈}*f*(*p*)^{⌉})
∨ *Prov*(^{⌈}¬*f*(*p*)^{⌉}). In
particular, this implies that neither *f*(*p*) nor
¬*f*(*p*) is provable in Peano Arithmetic; for
suppose on the contrary that PA ⊢
*f*(*p*), then by Löb's first condition and
propositional logic, PA ⊢
*Prov*(^{⌈}*f*(*p*)^{⌉})
∨ *Prov*(^{⌈}¬*f*(*p*)^{⌉}),
leading to a contradiction, and similarly if one supposes that PA
⊢ ¬*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. Δ_{0}-formulas are
arithmetical formulas in which all quantifiers are bounded by a term,
for example

∀y≤ss0 ∀z≤y∀x≤y+z(x+y≤ (y+(y+z))),

where **s** is the successor operator
(“+1”). The arithmetical theory *I*Δ_{0}
(where I stands for “induction”), is similar to Peano Arithmetic,
except that it allows less induction: the induction scheme

A(0) ∧ ∀x(A(x)→A(sx)) → ∀xA(x)

is restricted to Δ_{0}-formulas *A*.

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

*T*proves induction for Δ_{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*Δ_{0}+EXP;*T*does not prove any false sentences of the form ∃*x**A*(*x*), with*A*(*x*) a Δ_{0}-formula.

For such theories, arithmetical soundness and completeness of GL
hold, provided that □ translates to
*Prov*_{T}, a natural provability predicate
with respect to a sufficiently simple axiomatization of *T*.
Thus for modal sentences *A*:

GL ⊢Aif and only if for all realizationsf,T⊢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*Δ_{0}+Ω_{1}, a theory which is
somewhat weaker than *I*Δ_{0}+EXP in that
Ω_{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*Δ_{0}+Ω_{1}, but except for some
partial results by Berarducci et al. (1993), providing arithmetic
realizations consistent with *I*Δ_{0} +
Ω_{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
⊳,
where for a
given arithmetical theory *T*, the modal sentence *A*
⊳ *B* is meant to stand for
“*T*+*B* is interpretable in
*T*+*A*”. De Jongh and Veltman (1990) investigated
modal semantics for several interpretability logics. 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 Visser 1990,1997; Berarducci 1990, Shavrukov
1988).

### 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:

∀p∀q∃r□((□p ∨ □q) ↔ □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. The set of sentences of GL with propositional quantifiers that is arithmetically valid turns out to be undecidable (Shavrukov 1997).

### 5.4 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 □. Here, the situation becomes much more complex than in the case of propositional provability logic. Is there a 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 (1985) that the set of sentences of predicate provability logic all of whose realizations are provable in PA is not even recursively enumerable, so it has no reasonable axiomatization.

### 5.5 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 1994, 1999; Iemhoff 2000, 2001; Visser 2008);
- Rosser orderings and proof speed-up (see Guaspari and Solovay 1979, Švejdar 1983, Montagna 1992);
- classification of provability logics (see Visser 1980, Artemov 1985b, Beklemishev 1989, Beklemishev et al. 1999);
- bimodal provability logics with provability operators for different theories (see Beklemishev 1994, 1996);
- the polymodal logic of strong provability predicates (Japaridze 1986, Ignatiev 1993, Beklemishev 2004, Beklemishev, Joosten and Vervoort 2005);
- 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); and
- provability algebras, also called diagonalizable algebras or Magari algebras (see Magari 1975a, 1975b; Shavrukov 1993a, 1993b, 1997; Zambella 1994).

## 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 □◊
*p* →□⊥ 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

∀x□∃y(y=x)

are not at all problematic. If the number *n* is assigned to
*x*, then □∃*y*(*y* = *x*) is
true with respect to this assignment iff the sentence
∃*y*(*y* = *I*_{n}) is provable in Peano
Arithmetic; here, *I*_{n} is the numeral of
*n*, i.e., the term
**ss**…**s**0 with *n*
occurrences of the successor
operator ** s**. This sentence is true for
all

*n*in the standard model of the natural numbers, and ∀

*x*□∃

*y*(

*y*=

*x*) is even provable in Peano Arithmetic.

By the way, the Barcan Formula

∀x□A(x) → □∀xA(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 ⊥”). Its converse

□∀xA(x) → ∀x□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):

S5 ⊢ □A→A, (if one knowsA, thenAis true).

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

if GL ⊢ □A→A, then GL ⊢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 Gödel'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 Gödel's incompleteness theorems.

## Bibliography

### General references on provability logic

- Artemov, S.N. and L.D. Beklemishev, 2004, “Provability
Logic,” in
*Handbook of Philosophical Logic*, Second Edition, D. Gabbay and F. Guenthner, eds., Volume 13, Dordrecht: Kluwer, pp. 229–403. - Artemov, S.N., 2006, “Modal Logic in Mathematics,” in
P. Blackburn, et al. (eds.),
*Handbook of Modal Logic*, Amsterdam: Elsevier, pp. 927–970. - Boolos, G., 1979,
*The Unprovability of Consistency: An Essay in Modal Logic*, Cambridge: Cambridge University Press. - Boolos, G., 1993,
*The Logic of Provability*, New York and Cambridge: Cambridge University Press. - de Jongh, D.H.J. and G. Japaridze, 1998, “The Logic of
Provability,” in
*Handbook of Proof Theory*, Buss, S.R. (ed.), Amsterdam: North-Holland, pp. 475-546. - Lindström, P., 1996, “Provability Logic—A Short
Introduction,”
*Theoria*, 52(1–2): 19–61. - Segerberg, K., 1971,
*An Essay in Classical Modal Logic*, Uppsala: Filosofiska Föreningen och Filosofiska Institutionen vid Uppsala Universitet. - Švejdar, V., 2000, “On Provability
Logic,”
*Nordic Journal of Philosophy*, 4: 95–116. - Smoryński, C., 1995,
*Self-Reference and Modal Logic*, New York: Springer-Verlag. - Verbrugge, R. 1996, “Provability” in
*The Encyclopedia of Philosophy*(Supplement), D.M. Borchert (ed.), New York: Simon and Schuster MacMillan, pp. 476–478. - Visser, A., 1998, “Provability Logic,” in
*Routledge Encyclopedia of Philosophy*, W. Craig (ed.), London: Routledge, pp. 793–797.

### History

- van Benthem, J.F.A.K., 1978, “Four
Paradoxes,”
*Journal of Philosophical Logic*, 7(1): 49–72. - Boolos, G. and G. Sambin, 1991, “Provability: The Emergence
of a Mathematical Modality,”
*Studia Logica*, 50(1): 1–23. - Gödel, K., 1933, “Eine Interpretation des
Intuitionistischen Aussagenkalküls,”
*Ergebnisse eines Mathematischen Kolloquiums*, 4: 39–40; translation “An Interpretation of the Intuitionistic Propositional Calculus,” in K. Gödel,*Collected Works*, S. Feferman et al. (eds.), Oxford and New York: Oxford University Press, Volume 3, 1995, pp. 296–302. - Gödel, K., 1931, “Über Formal Unentscheidbare
Sätze der Principia Mathematica und Verwandter Systeme I,”
*Monatshefte für Mathematik und Physik*, 38: 173–198. - Henkin, L., 1952, “A Problem Concerning Provability,”
*Journal of Symbolic Logic*, 17: 160. - Hilbert, D. and P. Bernays, 1939,
*Grundlagen der Mathematik*, volume 2, Berlin/Heidelberg/New York: Springer-Verlag. - Lewis, C.I., 1912, “Implication and the Algebra of
Logic,”
*Mind*, 21: 522–531. - Löb, M.H., 1955, “Solution of a Problem of Leon
Henkin,”
*Journal of Symbolic Logic*, 20: 115–118. - Macintyre, A.J. and H. Simmons, 1973, “Gödel's
Diagonalization Technique and Related Properties of
Theories,”
*Colloquium Mathematicum*, 28: 165–180. - Magari, R., 1975a, “The Diagonalizable
Algebras,”
*Bollettino della Unione Mathematica Italiana*, 12: 117–125. - Magari, R., 1975b, “Representation and Duality Theory for
Diagonalizable Algebras,”
*Studia Logica*, 34(4): 305–313. - Smiley, T.J., 1963, “The Logical Basis of
Ethics,”
*Acta Philosophica Fennica*, 16: 237–246.

### Cut-elimination for provability logic

- Goré, R. and R. Ramanayake, 2008, “Valentini's
Cut-Elimination for Provability Logic Resolved,” in
*Advances in Modal Logic Volume 7*, C. Areces and R. Goldblatt (eds.), London: College Publications, pp. 67-86. - Negri, S., 2005, “Proof Analysis in Modal
Logic,”
*Journal of Philosophical Logic*, 50: 507–544. - Valentini, S., 1983, “The Modal Logic of Provability:
Cut-Elimination,”
*Journal of Philosophical Logic*, 12: 471–476.

### Possible worlds semantics and topological semantics

- Abashidze, M., 1985, “Ordinal Completeness of the
Gödel-Löb Modal System,” (in Russian) in
*Intensional Logics and the Logical Structure of Theories*, Tbilisi: Metsniereba, pp. 49–73. - Aiello, M., I. Pratt-Hartmann and J. van Benthem (eds.), 2007,
*Handbook of Spatial Logics*, Berlin: Springer-Verlag. - Beklemishev, L.D., G. Bezhanishvili and T. Icard, 2009, “On Topological Models of GLP,” Logic Group Preprint Series 278, Utrecht: University of Utrecht. Available at http://preprints.phil.uu.nl/lgps/.
- Beklemishev, L.D. 2010, “Ordinal completeness of bimodal provability logic GLB,” Logic Group Preprint Series 282, Utrecht: University of Utrecht. Available at http://preprints.phil.uu.nl/lgps/.
- Blass, A., 1990, “Infinitary Combinatorics and Modal
Logic,”
*Journal of Symbolic Logic*, 55(2): 761–778. - Esakia, L., 1981, “Diagonal Constructions, Löb's
Formula and Cantor's Scattered Spaces,” (in Russian), in
*Studies in Logic and Semantics*, Z. Mikeladze (ed.), Tbilisi: Metsniereba, pp. 128–143. - Esakia, L., 2003, “Intuitionistic Logic and Modality via
Topology,”
*Annals of Pure and Applied Logic*, 127: 155–170. - Goré, R. and J. Kelly, 2007, “Automated Proof Search in Gödel-Löb Provability Logic,”, British Logic Colloquium 2007, available at http://www.dcs.bbk.ac.uk/~roman/blc/.
- Goré, R., 2009, “Machine Checking Proof Theory: An
Application of Logic to Logic,” In
*ICLA '09: Proceedings of the 3rd Indian Conference on Logic and Its Applications*, Berlin: Springer-Verlag, pp. 23-35. - Hakli, R. and S. Negri, 2010 (to appear), “Does the
Deduction Theorem Fail for Modal
Logic?,”
*Synthese*. - Icard, T.F. III, 2011, “A Topological Study of the Closed
Fragment of GLP,”
*Journal of Logic and Computation*, 21(4): 683–696; first published online 2009, doi:10.1093/logcom/exp043 - Japaridze, G.K., 1986,
*The Modal Logical Means of Investigation of Provability*, Thesis in Philosophy (in Russian), Moscow. - McKinsey, J.C.C. and A. Tarski, 1944, “The Algebra of
Topology,”
*Annals of Mathematics*, 45: 141–191.

### Provability and Peano Arithmetic

- Davis, M., 1958,
*Computability and Unsolvability*, New York, McGraw-Hill; reprinted with an additional appendix, New York, Dover Publications 1983. - Hájek, P. and P. Pudlák, 1993,
*Metamathematics of First-Order Arithmetic*, Berlin: Springer-Verlag. - Solovay, R.M., 1976, “Provability Interpretations of Modal
Logic,”
*Israel Journal of Mathematics*, 25: 287–304.

### The scope of provability logic

- Artemov, S.N., 1985a, “Nonarithmeticity of Truth Predicate
Logics of Provability,”
*Doklady Akademii Nauk SSSR*, 284: 270–271 (in Russian); English translation in*Soviet Mathematics Dokl*, 32: 403–405. - Artemov, S.N., 1985b,“On Modal Logics Axiomatizing
Provability,”
*Izvestiya Akad. Nauk SSSR, ser. mat.*, 49(6): 1123–1154 (in Russian); English translation in*Math. USSR Izvestiya*, 27(3). - Artemov, S.N. and L.D. Beklemishev, 1993, “On Propositional
Quantifiers in Provability Logic,”
*Notre Dame Journal of Formal Logic*, 34: 401–419. - Artemov, S.N., 1994, “Logic of Proofs,”
*Annals of Pure and Applied Logic*, 67(2): 29–59. - Artemov, S.N. and F. Montagna, 1994, “On First-order
Theories with Provability Operator,”
*Journal of Symbolic Logic*, 59(4): 1139–1153. - Artemov, S.N., 2001, “Explicit Provability and Constructive
Semantics,”
*Bulletin of Symbolic Logic*, 7: 1–36. - Artemov, S.N. and R. Iemhoff, 2007, “The Basic
Intuitionistic Logic of Proofs,”
*Journal of Symbolic Logic*, 72(2): 439–451. - Beklemishev, L.D., 1989, “On the Classification of
Propositional Provability Logics,”
*Izvestiya Akademii Nauk SSSR, ser. mat.*, 53(5): 915–943 (in Russian); English translation in*Math. USSR Izvestiya*, 35 (1990) 247–275. - Beklemishev, L.D., 1994, “On Bimodal Logics of
Provability,”
*Annals of Pure and Applied Logic*, 68: 115–160. - Beklemishev, L.D., 1996, “Bimodal Logics for Extensions of
Arithmetical Theories,”
*Journal of Symbolic Logic*, 61: 91–124. - Beklemishev, L.D., 1999, “Parameter-Free Induction and
Provably Total Computable Functions,”
*Theoretical Computer Science*, 224: 13–33. - Beklemishev, L.D., M. Pentus and N. Vereshchagin, 1999,
*Provability, Complexity, Grammars*, American Mathematical Society Translations (Series 2, Volume 192). - Beklemishev, L.D., 2004, “Provability Algebras and
Proof-Theoretic Ordinals, I,”
*Annals of Pure and Applied Logic*, 128: 103–123. - Beklemishev, L.D., 2005, “Reflection Principles and
Provability Algebras in Formal Arithmetic,”
*Uspekhi Matematicheskikh Nauk*, 60(2): 3–78. (in Russian); English translation in:*Russian Mathematical Surveys*, 60(2) (2005): 197–268. - Beklemishev, L.D., 2006, “The Worm Principle,”
in
*Lecture Notes in Logic 27. Logic Colloquium '02*, Z. Chatzidakis, P. Koepke, and W. Pohlers (eds.), Natick (MA): AK Peters, pp. 75–95. - Beklemishev, L.D., J. Joosten and M. Vervoort, 2005, “A
Finitary Treatment of the Closed Fragment of Japaridze's Provability
Logic,”
*Journal of Logic and Computation*, 15(4): 447–463. - Beklemishev, L.D. and A. Visser, 2006, “Problems in the
Logic of Provability,” in
*Mathematical Problems from Applied Logic I: Logics for the XXIst Century*, D.M. Gabbay, S.S. Goncharov and M. Zakharyashev (eds.), (International Mathematical Series, Volume 4), New York: Springer, pp. 77–136. - Berarducci, A., 1990, “The Interpretability Logic of Peano
Arithmetic,”
*Journal of Symbolic Logic*, 55: 1059–1089. - Berarducci, A. and R. Verbrugge, 1993, “On the Provability
Logic of Bounded Arithmetic,”
*Annals of Pure and Applied Logic*, 61: 75–93. - de Jongh, D.H.J. and F. Veltman, 1990, “Provability Logics
for Relative Interpretability,” in P.P. Petkov
(ed.),
*Mathematical Logic: Proceedings of the Heyting 1988 Summer School in Varna, Bulgaria*, Boston: Plenum Press, pp. 31–42. - Guaspari, D. and R.M. Solovay, 1979, “Rosser
Sentences,”
*Annals of Mathematical Logic*, 16: 81–99. - Iemhoff, R., 2000, “A Modal Analysis of some Principles of
the Provability Logic of Heyting Arithmetic,” in
*Advances in Modal Logic*(Volume 2), M. Zakharyashev et al. (eds.), Stanford: CSLI Publications, pp. 319–354. - Iemhoff, R., 2001, “On the Admissible Rules of
Intuitionistic Propositional Logic,”
*Journal of Symbolic Logic*, 66: 281–294. - Iemhoff, R., 2003, “Preservativity Logic: An Analogue of
Interpretability Logic for Constructive
Theories,”
*Mathematical Logic Quarterly*, 49(3): 1–21. - Ignatiev, K.N., 1993, “On Strong Provability Predicates and
the Associated Modal Logics,”
*Journal of Symbolic Logic*, 58: 249–290. - Jongh, D.H.J. de, M. Jumelet and F. Montagna, 1991, “On the
Proof of Solovay's Theorem,”
*Studia Logica*, 50: 51–70. - McGee, V. and G. Boolos, 1987, “The Degree of the Set of
Sentences of Predicate Provability Logic that are True under Every
Interpretation,”
*Journal of Symbolic Logic*, 52: 165–171. - Montagna, F., 1992, “Polynomially and Superexponentially
Shorter Proofs in Fragments of Arithmetic,”
*Journal of Symbolic Logic*, 57: 844–863. - Shavrukov, V.Yu., 1988, “The Logic of Relative Interpretability over Peano Arithmetic,” Technical Report No. 5, Moscow: Steklov Mathematical Institute (in Russian).
- Shavrukov, V.Yu., 1993a, “A Note on the Diagonalizable
Algebras of PA and ZF,”
*Annals of Pure and Applied Logic*, 61: 161–173. - Shavrukov, V.Yu., 1993b, “Subalgebras of Diagonalizable
Algebras of Theories Containing Arithmetic,”
*Dissertationes Mathematicae*, 323. - Shavrukov, V.Yu., 1997, “Undecidability in Diagonalizable
Algebras,”
*Journal of Symbolic Logic*, 62: 79–116. - Švejdar, V., 1983, “Modal Analysis of Generalized
Rosser Sentences,”
*Journal of Symbolic Logic*, 48: 986–999. - Troelstra, A.S., 1973,
*Metamathematical Investigation of Intuitionistic Arithmetic and Analysis*, Berlin: Springer-Verlag. - Vardanyan, V.A., 1986, “Arithmetic Complexiy of Predicate
Logics of Provability and their Fragments,”
*Doklady Akademii Nauk SSSR*, 288: 11–14 (in Russian); English translation in*Soviet Math. Dokl.*, 33: 569–572. - Visser, A., 1980,
*Aspects of Diagonalization and Provability*, Ph.D. Thesis, Utrecht: University of Utrecht. - Visser, A., 1990, “Interpretability Logic,”
in
*Mathematical Logic: Proceedings of the Heyting 1988 Summer School in Varna, Bulgaria*, P.P. Petkov (ed.), Boston: Plenum Press, pp. 175–209. - Visser, A., 1998, “An Overview of Interpretability
Logic,” in
*Advances in Modal Logic*(Volume 1), M. Kracht et al. (eds.), Stanford: CSLI Publications, pp. 307–359. - Visser, A., 1999, “Rules and Arithmetics,”
*Notre Dame Journal of Formal Logic*, 40(1): 116–140. - Visser, A., 2002, “Substitutions of Σ
_{1}Sentences: Explorations between Intuitionistic Propositional Logic and Intuitionistic Arithmetic,”*Annals of Pure and Applied Logic*, 114: 227–271. - Visser, A. and M. de Jonge, 2006, “No Escape from
Vardanyan's Theorem”,
*Archive of Mathematical Logic*, 45(5): 539–554. - Visser, A., 2008, “Closed Fragments of Provability Logics of
Constructive Theories,”
*Journal of Symbolic Logic*, 73: 1081–1096. - Zambella, D., 1994, “Shavrukov's Theorem on the Subalgebras
of Diagonalizable Algebras for Theories Containing
IΔ
_{0}+exp,”*Notre Dame Journal of Formal Logic*, 35: 147–157.

### Philosophical significance

- Davis, M., 1990, “Is Mathematical Insight
Algorithmic?,” Commentary on Roger Penrose, The Emperor's New
Mind,
*Behavioral and Brain Sciences*, 13: 659–660. - Davis, M., 1993, “How Subtle is Gödel's Theorem?”
(Commentary on Roger Penrose, The Emperor's New Mind),
*Behavioral and Brain Sciences*, 16: 611–612. - Egré, P., 2005, “The Knower Paradox in the Light of
Provability Interpretations of Modal Logics,”
*Journal of Logic, Language, and Information*, 14(1): 13–48. - Kaplan, D. and R. Montague, 1960, “A Paradox
Regained,”
*Notre Dame Journal of Formal Logic*, 1(3): 79–90. - Montague, R., 1963, “Syntactical Treatments of Modality,
With Corollaries on Reflection Principles and Finite
Axiomatizability,”
*Acta Philosophica Fennica*, 16: 153–67. - Quine, W.V., 1966, “Necessary Truth,” in Quine,
W.V.,
*The Ways of Paradox and Other Essays*, New York: Random House, pp. 48–56. - Quine, W.V., 1953, “Three Grades of Modal
Involvement,” in
*Proceedings of the 11th International Congress of Philosophy*, Amsterdam: North-Holland, pp. 65-81; reprinted in Quine, W.V., 1966,*The Ways of Paradox and Other Essays*, New York: Random House, pp. 156–174.

## Academic Tools

How to cite this entry. Preview the PDF version of this entry at the Friends of the SEP Society. Look up this entry topic at the Indiana Philosophy Ontology Project (InPhO). Enhanced bibliography for this entry at PhilPapers, with links to its database.

## Other Internet Resources

- Open problems in Provability Logic, maintained by Lev Beklemishev, University of Utrecht
- Mailing list Foundations of Mathematics, New York University
- Paper by Albert Visser on formal provability versus human provability (in Dutch), University of Utrecht
- Presentation slides on provability logic by Rineke Verbrugge, University of Groningen