Provability logic is a modal logic that is used to investigate whatarithmetical theories can express in a restricted language about theirprovability predicates. The logic has been inspired by developments inmeta-mathematics such as Gödel’s incompleteness theorems of1931 and Löb’s theorem of 1953. As a modal logic,provability logic has been studied since the early seventies, and hashad important applications in the foundations of mathematics.

From a philosophical point of view, provability logic is interestingbecause the concept of provability in a fixed theory of arithmetic hasa unique and non-problematic meaning, other than concepts likenecessity and knowledge studied in modal and epistemic logic.Furthermore, provability logic provides tools to study the notion ofself-reference.

• 1. The history of provability logic
• 2. The axiom system of propositional provability logic
  • 2.1 Axioms and rules
  • 2.2 The fixed point theorem
• 3. Possible worlds semantics and topological semantics
  • 3.1 Characterization and modal soundness
  • 3.2 Modal completeness
  • 3.3 Failure of strong completeness
  • 3.4 Topological semantics for provability logic
• 4. Provability logic and Peano Arithmetic
  • 4.1 Arithmetical soundness
  • 4.2 Arithmetical completeness
• 5. The scope of provability logic
  • 5.1 Boundaries
  • 5.2 Interpretability logic
  • 5.3 Propositional quantifiers
  • 5.4 Japaridze’s bimodal and polymodal provability logics
  • 5.5 Predicate provability logic
  • 5.6 Other generalizations
• 6. Philosophical significance
• Bibliography
• Academic Tools
• Other Internet Resources
  • Papers and Presentations
  • Other Sites
• 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 byK. Gödel (1933), where he introduces translations from intuitionisticpropositional logic into modal logic (more precisely, into the systemnowadays called S4), and briefly mentions that provability can beviewed as a modal operator. Even earlier, C.I. Lewis started themodern study of modal logic by introducing strict implication as akind of deducibility, where he may have meant deducibility in a formalsystem likePrincipia Mathematica, but this is not clear from his writings.

The other strand starts from research in meta-mathematics: what canmathematical theories say about themselves by encoding interestingproperties? In 1952, L. Henkin posed a deceptively simple questioninspired byGödel’s incompleteness theorems. In order to formulate Henkin’s question, some more backgroundis needed. As a reminder, Gödel’s first incompletenesstheorem states that, for a sufficiently strong formal theory likePeano Arithmetic, any sentence asserting its own unprovability is infact unprovable. On the other hand, from “outside” theformal theory, one can see that such a sentence is true in thestandard model, pointing to an important distinction between truth andprovability.

More formally, let \(\ulcorner A \urcorner\) denote the Gödelnumber of arithmetical formula \(A\), which is the result of assigninga numerical code to \(A\). Let \(\Prov\) be the formalized provabilitypredicate for Peano Arithmetic, which is of the form \(\exists p \,\Proof(p,x)\). Here, \(\Proof\) is the formalized proof predicate ofPeano Arithmetic, and \(\Proof(p,x)\) stands for “Gödelnumber \(p\) codes a correct proof from the axioms of Peano Arithmeticof the formula with Gödel number \(x\)”. (For a moreprecise formulation, see Smoryński (1985), Davis (1958).) Now,suppose that Peano Arithmetic proves \(A \leftrightarrow \neg\)\(\Prov (\ulcorner A \urcorner)\), then by Gödel’s result,\(A\) is not provable in Peano Arithmetic, and thus it is true, for infact the self-referential sentence \(A\) states “I am notprovable”.

Henkin on the other hand wanted to know whether anything could be saidabout sentences asserting their own provability: supposing that PeanoArithmetic proves \(B \leftrightarrow \Prov(\ulcorner B \urcorner)\),what does this imply about \(B\)? Three years later, M. Löb tookup the challenge and answered Henkin’s question in a surprisingway. Even though all sentences provable in Peano Arithmetic are indeedtrue about the natural numbers, Löb showed that the formalizedversion of this fact, \(\Prov(\ulcorner B \urcorner) \rightarrow B\),can be proved in Peano Arithmetic only in the trivial case that PeanoArithmetic already proves \(B\) itself. This result, now calledLöb’s theorem, immediately answers Henkin’s question.(For a proof of Löb’s theorem, seeSection 4.) Löb also showed a formalized version of his theorem, namely thatPeano Arithmetic proves

In the same paper, Löb formulated three conditions on theprovability predicate of Peano Arithmetic, that form a usefulmodification of the complicated conditions that Hilbert and Bernaysintroduced in 1939 for their proof of Gödel’s secondincompleteness theorem. In the following, derivability of \(A\) fromPeano 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 Löb conditions, as they are called nowadays, seem to cryout for a modal logical investigation, where the modality \(\Box\)stands for provability in PA. Ironically, the first time that theformalized version of Löb’s theorem was stated as the modalprinciple

was in a paper by Smiley in 1963 about the logical basis of ethics,which did not consider arithmetic at all. More relevantinvestigations, however, seriously started only almost twenty yearsafter publication of Löb’s paper. The early 1970s saw therapid development of propositional provability logic, where severalresearchers in different countries independently proved the mostimportant results, discussed in Sections2,3, and4. Propositional provability logic turned out to capture exactly whatmany formal theories of arithmetic can say by propositional meansabout their own provability predicate. More recently, researchers haveinvestigated the boundaries of this approach and have proposed severalinteresting more expressive extensions of provability logic (seeSection 5).

2. The axiom system of propositional provability logic

The logical language of propositional provability logic contains, inaddition to propositional atoms and the usual truth-functionaloperators as well as the contradiction symbol \(\bot\), a modaloperator \(\Box\) with intended meaning “is provable in\(T\),” where \(T\) is a sufficiently strong formal theory, letus say Peano Arithmetic (seeSection 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 S4presented in the entrymodal logic.

2.1 Axioms and rules

Propositional provability logic is often called GL, after Gödeland Löb. (Alternative names found in the literature forequivalent systems are L, G, KW, K4W, and PrL). The logic GL resultsfrom adding the following axiom to the basic modal logic K:

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

Furthermore, it is closed under the Modus Ponens Rule, which allows toderive \(B\) from \(A \rightarrow B\) and \(A\), and theGeneralization Rule, which says that if \(A\) is a theorem of GL, thenso is \(\Box A\).

The notion \(\GL \vdash A\) denotes provability of a modal formula\(A\) in propositional provability logic. It is not difficult to seethat the modal axiom \(\Box A \rightarrow \Box\Box A\) (known as Axiom4 of modal logic) is indeed provable in GL. To prove this, one usesthe substitution \(A \wedge \Box A\) for \(A\) in the axiom (GL).Then, seeing that the antecedent of the resulting implication followsfrom \(\Box A\), one applies the Distribution Axiom and theGeneralization Rule as well as some propositional logic.

Note that GL proves many unexpected theorems that are not shared withother well-known modal logics such as K and S4. For example, oneinstantiation of the axiom GL is \(\Box(\Box\bot \rightarrow \bot)\rightarrow \Box\bot\), from which it follows by the other axioms andrules that \(\Box\Diamond A \rightarrow \Box B\) for any formulas\(A\) and \(B\).^[1] Unless explicitly stated otherwise, in the sequel “provabilitylogic” stands for the system GL of propositional provabilitylogic.

As to theproof theory of provability logic, Valentini (1983)proved that a standard sequent calculus formulation of GL obeyscut elimination, which means, roughly formulated, that eachformula provable from GL in the sequent calculus also has a GL sequentproof “without detours” (see the entrythe development of proof theory for a precise explanation of cut elimination). In recent years, therehas been renewed interest in the proof theory of GL, see for exampleGoré and Ramanayake (2008, 2012) and Goré, Ramanayakeand Shillito (2021). Cut-elimination leads to the desirablesubformula property for GL, because all formulas that appearin a cut-free proof are subformulas of the endsequent formulas.

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

An intriguing new proof-theoretical development is Shamkanov’sexpansion of sequent-style proof systems by allowingcircularproofs (Shamkanov 2014). Consider a sequent system for K4, themodal system resulting from GL by replacing the axiom GL by the weakeraxiom \(\Box A \rightarrow \Box\Box A\) (axiom 4). However, supposethat open hypotheses are allowed, provided that the same sequentoccurs strictly below that hypothesis in the proof tree. Formulatedmore technically, one can find a circular derivation from an ordinaryderivation tree by linking each of its non-axiomatic leaves with anidentical interior node. Shamkanov (2014) proved that the resultingsystem is consistent and that moreover, in general, each sequent has aGL-derivation if and only if it has a circular K4-derivation. Circularproofs also provide a method to show proof-theoretically thatLyndon’s interpolation theorem holds for GL (Shamkanov 2011).Standard interpolation for GL had already been proved before bydifferent methods (Boolos 1979; Smoryński 1978; Rautenberg 1983)and so had uniform interpolation (Shavrukov 1993b,Bílková 2016, Férée et al. [Other InternetResources]). (For more information about Lyndon’s interpolationtheorem for first-order logic, see also the entryfirst-order model theory).

2.2 The fixed point theorem

The main “modal” result about provability logic is thefixed point theorem, which D. de Jongh and G. Sambin independentlyproved in 1975 (Sambin 1976, Smoryński 1985, de Jonghforthcoming). Even though it is formulated and proved by strictlymodal methods, the fixed point theorem still has great arithmeticalsignificance. It says essentially that self-reference is not reallynecessary, in the following sense. Suppose that all occurrences of thepropositional variable \(p\) in a given formula \(A(p)\) are under thescope of the provability operator, for example \(A(p) = \neg\Box p\),or \(A(p) = \Box(p \rightarrow q)\). Then there is a formula \(B\) inwhich \(p\) does not appear, such that all propositional variablesthat occur in \(B\) already appear in \(A(p),\) and such that

This formula \(B\) is called afixed point of \(A(p)\).Moreover, the fixed point is unique, or more accurately, if there isanother formula \(C\) such that \( \GL \vdash C \leftrightarrowA(C)\), then we must have \( \GL \vdash B \leftrightarrow C\). Mostproofs in the literature give an algorithm by which one can computethe fixed point (see Smoryński 1985, Boolos 1993, Sambin andValentini 1982, Lindström 2006). A particularly short and clearproof, 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 fixedpoint produced by such an algorithm is \(\neg \, \Box\bot\), andindeed one can prove that

If this is read arithmetically, the direction from left to right isjust the formalized version of Gödel’s secondincompleteness theorem: if a sufficiently strong formal theory \(T\)like Peano Arithmetic does not prove a contradiction, then it is notprovable in \(T\) that \(T\) does not prove a contradiction. Thus,sufficiently strong consistent arithmetical theories cannot provetheir own consistency. We will turn to study the relation betweenprovability logic and arithmetic more precisely inSection 4, but to that end another “modal” aspect of GL needs to beprovided first: semantics.

3. Possible worlds semantics and topological semantics

Provability logic has suitable possible worlds semantics, just likemany other modal logics. As a reminder, a possible worlds model (orKripke model) is a triple \(M = \langle W,R,V \rangle\), where \(W\)is a non-empty set of possible worlds, \(R\) is a binary accessibilityrelation on \(W\), and \(V\) is a valuation that assigns a truth valueto each propositional variable for each world in \(W\). The pair \(F =\langle W,R \rangle\) is called the frame of this model. The notion oftruth 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 mostinteresting clause, the one for the provability operator \(\Box\):

See the entrymodal 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 GLhowever, is not: we need to restrict the class of possible worldsmodels to a more suitable one. Let us say that a formula \(A\) isvalid in frame \(F\), notation \(F \models A\), iff \(A\) is true inall worlds in Kripke models \(M\) based on \(F\). It turns out thatthe new axiom (GL) of provability logic corresponds to a condition onframes, as follows:

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

Here,transitivity is the well-known property that for allworlds \(w_1\), \(w_2\), \(w_3\) in \(W\), if \(w_1 Rw_2\) and \(w_2Rw_3\), then \(w_1 Rw_3\). A relation isconverselywell-founded iff there are no infinite ascending sequences, thatis sequences of the form \(w_1 Rw_2 Rw_3 R \ldots\). Note thatconversely 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 modallysound with respect to the class of possible worlds models ontransitive conversely well-founded frames, because all axioms andrules of GL are valid on such models. The question is whethercompleteness also holds: for example, the formula \(\Box A \rightarrow\Box\Box A\), which is valid on all transitive frames, is indeedprovable in GL, as was mentioned inSection 1. But isevery formula that is valid on all transitiveconversely well-founded frames also provable in GL?

3.2 Modal completeness

Unaware of the arithmetical significance of GL, K. Segerberg proved in1971 that GL is indeed complete with respect to transitive converselywell-founded frames; D. de Jongh and S. Kripke independently provedthis result as well. Segerberg showed that GL is complete even withrespect to the more restricted class of finite transitive irreflexivetrees, a fact which later turned out to be very useful forSolovay’s proof of the arithmetical completeness theorem (seeSection 4).

The modal soundness and completeness theorems immediately give rise toa decision procedure to check for any modal formula \(A\) whether\(A\) follows from GL or not, by depth-first search throughirreflexive transitive trees of bounded depth. Looking at theprocedure a bit more precisely, it can be shown that GL is decidablein the computational complexity class PSPACE, like the well-knownmodal logics K, T and S4. This means that there is a Turing machinethat, given a formula \(A\) as input, answers whether \(A\) followsfrom GL or not; the size of the memory that the Turing machine needsfor its computation is only polynomial in the length of \(A\). One canshow that the decision problem for GL (again, like the decisionproblems for K, T and S4) is PSPACE-complete, in the sensethat all other problems in PSPACE are no harder than deciding whethera given formula is a theorem of GL. (See Goré and Kelly 2007[Other Internet Resources] for the description of an automated theoremprover for GL.)

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

3.3 Failure of strong completeness

Many well-known modal logics \(S\) are not only complete with respectto an appropriate class of frames, but evenstronglycomplete. In order to explain strong completeness, we need thenotion ofderivability from a set of assumptions. A formula\(A\) is derivable from the set of assumptions \(\Gamma\) in a modallogic \(S\), written as \(\Gamma \vdash A\), if \(A\) is in \(\Gamma\)or \(A\) follows from formulas in \(\Gamma\) and axioms of \(S\) byapplications of Modus Ponens and the Generalization Rule. Here, theGeneralization Rule can only be applied to derivations withoutassumptions (see Hakli and Negri 2010).

Now a modal logic \(S\) isstrongly 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 whichall formulas of \(\Gamma\) are true, then \(\Gamma \vdash A\) in thelogic \(S\).

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

Strong completeness does not hold for provability logic, however,becausesemantic compactness fails. Semantic compactness isthe property that for each infinite set \(\Gamma\) of formulas,

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

As a counterexample, take the infinite set of formulas

Then for every finite subset \(\Delta\) of \(\Gamma\), one canconstruct a model on a transitive, conversely well-founded frame and aworld in the model where all formulas of \(\Delta\) are true. So bymodal soundness, GL does not prove \(\bot\) from \(\Delta\) for anyfinite \(\Delta \subseteq \Gamma\), anda fortiori GL doesnot prove \(\bot\) from \(\Gamma\), as any GL-proof is finite. On theother 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 ofstrong completeness.^[2]

3.4 Topological semantics for provability logic

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

However, provability logic doesnot prove reflection, as theinstantiation \(\Box\bot \rightarrow \bot\) of reflection would leadto a contradiction with the axiom (GL).

Provability logic therefore needs a different approach. Based on asuggestion by J. McKinsey and A. Tarski (1944), L. Esakia (1981, 2003)investigated the interpretation of \(\Diamond\) as the derived setoperator \(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 conceptsdense-in-itself andscattered. A subset \(B\) of atopological space is calleddense-in-itself if \(B \subseteqd(B)\). A topological space is calledscattered if it has nonon-empty subset that is dense-in-itself. The ordinals in theirinterval topology form examples of scattered spaces. Esakia (1981)proved an important correspondence: he showed that a topological spacesatisfies the axiom GL if and only if the space isscattered. This correspondence soon led to the result,independently found by Abashidze (1985) and Blass (1990), thatprovability logic is complete with respect to any ordinal \(\ge\omega^\omega\).

In the previous decades, topological semantics for provability logichas seen a veritable revival, especially in the study ofJaparidze’s bimodal provability logic GLB, an extension of GL(Japaridze 1986). The logic GLB turns out to bemodallyincomplete with respect to its possible worlds semantics, in thesense that it does not correspond to any class offrames.^[3] 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 itstopological semantics(see also Beklemishev 2009, Icard 2011). Intriguing reverberations ofEsakia’s correspondence between GL and scattered topologicalspaces can even be found in topological studies of spatial andepistemic logics (see Aiello et al. 2007). (SeeSection 5.4 for further discussion about GLB).

4. Provability logic and Peano Arithmetic

From the time GL was formulated, researchers wondered whether it wasadequate for formal theories like Peano Arithmetic (PA): does GL proveeverything about the notion of provability that can beexpressed in a propositional modal language and can be proved in PeanoArithmetic, or should more principles be added to GL? To make thisnotion of adequacy more precise, we define arealization(sometimes called translation or interpretation) to be a functionf that assigns to each propositional atom of modal logic asentence 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 isarithmeticallysound with respect to PA, formally:

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

Proof sketch of arithmetical soundness. PA indeedproves realizations of propositional tautologies, and provability ofthe Distribution Axiom of GL translates to

for all formulasA andB, which is justLöb’s second derivability condition (seeSection 1). Moreover, PA obeys Modus Ponens, as well as the translation of theGeneralization Rule:

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

This is exactly the formalized version of Löb’s theoremmentioned inSection 1.

Let us give a sketch of the proof of Löb’s theorem itselffrom his derivability conditions (the proof of the formalized versionis similar). The proof is based on Gödel’s diagonalizationlemma, which says that for any arithmetical formula \(C(x)\) there isan arithmetical formula \(B\) such that

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

Proof of Löb’s theorem:. Suppose that\(\PA \vdash \Prov(\ulcorner A\urcorner ) \rightarrow A\); we need toshow that \(\PA \vdash A\). By the diagonalization lemma, there is aformula \(B\) such that

From this it follows by Löb’s first and second derivabilityconditions plus some propositional reasoning that

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

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

thus

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

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

as desired.

Note that substituting \(\bot\) for \(A\) in Löb’s theorem,we derive that \(\PA \vdash \neg\, \Prov(\ulcorner \bot\urcorner )\)implies \(\PA \vdash \bot\), which is just the contraposition ofGödel’s second incompleteness theorem.

4.2 Arithmetical completeness

The landmark result in provability logic is R. Solovay’sarithmetical completeness theorem of 1976, showing that GL is indeedadequate for Peano Arithmetic:

This theorem says essentially that the modal logic GL captureseverything that Peano Arithmetic can truthfully say in modal termsabout its own provability predicate. The direction from left to right,arithmetical soundness of GL, is discussed above. Solovay set out toprove the other, much more difficult, direction by contraposition. Hisproof is based on intricate self-referential techniques, and only asmall glimpse can be given here.

The modal completeness theorem by Segerberg was an important firststep in Solovay’s proof of arithmetical completeness of GL withrespect to Peano Arithmetic. Suppose that GL does not prove the modalformula \(A\). Then, by modal completeness, there is a finitetransitive irreflexive tree such that \(A\) is false at the root ofthat tree. Now Solovay devised an ingenious way to simulate such afinite tree in the language of Peano Arithmetic. Thus he found arealization \(f\) from modal formulas to sentences of arithmetic, suchthat Peano Arithmetic does not prove \(f(A)\).

Solovay’s completeness theorem provides an alternative way toconstruct many arithmetical sentences that are not provable in PeanoArithmetic. For example, it is easy to make a possible worlds model toshow that GL does not prove \(\Box p \vee \Box\neg\, p\), so bySolovay’s theorem, there is an arithmetical sentence \(f(p)\)such that Peano Arithmetic does not prove \(\Prov(\ulcornerf(p)\urcorner ) \vee \Prov(\ulcorner \neg\, f(p)\urcorner )\). Inparticular, this implies that neither \(f(p)\) nor \(\neg\, f(p)\) isprovable in Peano Arithmetic; for suppose on the contrary that \(\PA\vdash f(p)\), then by Löb’s first condition andpropositional 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 aninteresting fragment of an undecidable formal theory like PeanoArithmetic—namely that which arithmetic can express inpropositional terms about its own provability predicate—can bestudied by means of a decidable modal logic, GL, with a perspicuouspossible worlds semantics.

5. The scope of provability logic

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

5.1 Boundaries

Since the late 1980s, logicians have investigated many other systemsof arithmetic that are weaker than Peano Arithmetic. Often theselogicians took their inspiration from computability issues, forexample the study of functions computable in polynomial time. Theyhave given a partial answer to the question: “For which theoriesof arithmetic does Solovay’s arithmetical completeness theorem(with respect to the appropriate provability predicate) stillhold?” To discuss this question, two concepts are needed.\(\Delta_0\)-formulas are arithmetical formulas in which allquantifiers are bounded by a term, for example

where \(\bs\) is the successor operator (“\(+1\)”). Thearithmetical theory \(I \Delta_0\) (where I stands for“induction”), is similar to Peano Arithmetic, except thatit allows less induction: the induction scheme

is restricted to \(\Delta_0\)-formulas \(A\).

As De Jongh and others (1991) pointed out, arithmetical completenesscertainly holds for theories \(T\) that satisfy the following twoconditions:

1. \(T\) proves induction for \(\Delta_0\)-formulas, and \(T\) provesEXP, 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 naturalprovability predicate with respect to a sufficiently simpleaxiomatization of \(T\). Thus for modal sentences \(A\):

It is not clear yet whether Condition 1 gives a lower bound on thescope of provability logic. For example, it is still an open questionwhether GL is the provability logic of \(I \Delta_0+\Omega_1\), atheory 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 soundwith respect to \(I \Delta_0+\Omega_1\), but except for some partialresults by Berarducci and Verbrugge (1993), providing arithmeticrealizations consistent with \(I \Delta_0+\Omega_1\) for a restrictedclass of sentences consistent with GL, the question remains open. Itsanswer may hinge on open problems in computational complexitytheory.

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

5.2 Interpretability logic

In order to be able to speak in a modal language about importantdistinctions between theories, researchers have extended provabilitylogic in many different ways. Let us mention a few. One extension isto add a binary modality \(\interprets\), where for a givenarithmetical theory \(T\), the modal sentence \(A \interprets B\) ismeant to stand for “\(T+B\) is interpretable in \(T+A\)”(Švejdar, 1983). De Jongh and Veltman (1990) investigated modalsemantics for several interpretability logics, while De Jongh andVisser (1991) proved the explicit fixed-point property for the mostimportant ones. Visser characterized the interpretability logic of themost common finitely axiomatized theories, and Berarducci andShavrukov independently characterized the one for PA, which is notfinitely axiomatizable. It appears that indeed, the interpretabilitylogic of finitely axiomatizable theories is different from theinterpretability logic of Peano Arithmetic (see Montagna 1987; Visser1990, 1998; Berarducci 1990, Shavrukov 1988; Joosten and Visser2000).

5.3 Propositional quantifiers

Another way to extend the framework of propositional provability logicis to add propositional quantifiers, so that one can expressprinciples like Goldfarb’s:

saying that for any two sentences there is a third sentence which isprovable if and only if either of the first two sentences is provable.This principle is provable in Peano Arithmetic (see e.g. Artemov andBeklemishev 1993). The set of sentences of GL with propositionalquantifiers 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\)-likeprovability operators, denoted by \([0]\) and \([1]\), with their dual\(\Diamond\)-like operators \(\langle 0\rangle\) and \(\langle1\rangle\), respectively. In Japaridze’s interpretation, one canthink of \([0]\) as standing for the standard provability predicate inPeano Arithmetic. On the other hand, \([1]\) corresponds to a strongerprovability predicate, namely \(\omega\)-provabilty.

Let us define the concepts that are needed to understand this intendedinterpretation of GLB. An arithmetical theory \(T\) is defined to be\(\omega\)-consistent if and only if for all formulas A withfree variable \(x\), \(T\vdash \neg\, A(I_n)\) for all \(n\) impliesthat \(T \not\vdash \exists x \, A(x)\); here, \(I_n\) is the numeralof \(n\), i.e., the term \(\bs\bs\ldots\bs 0\) with \(n\) occurrencesof the successor operator \(\bs\). Peano Arithmetic (PA) is the mostwell-known example of an \(\omega\)-consistent theory (see alsoGödel’s incompleteness theorems). Now let PA\(^+\) be the arithmetical theory whose axioms are those ofPA together with all sentences \(\forall x \, \neg \, A(x)\) such thatfor every \(n\), PA\(\vdash \neg \, A(I_n)\). Now\(\omega\)-provability is simply provability in PA\(^+\), so it is thedual of \(\omega\)-consistency.

Japaridze’s bimodal provability logic GLB can be axiomatized bythe axioms and rules of GL (seeSection 2), formulated separately for [0] and [1]. In addition, GLB has two mixedaxioms, 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 isdecidable and has a reasonable Kripke semantics, and it isarithmetically sound and complete with respect to Peano Arithmetic(Japaridze 1988, Boolos 1993).

A polymodal analogue of Japaridze’s GLB, named GLP, has receiveda lot of attention in recent years. GLP has infinitely many\(\Box\)-like provability operators, denoted by boxes \([n]\) forevery natural number \(n\), with their dual \(\Diamond\)-likeoperators \(\langle n\rangle\). Again, one can think of \([0]\) asstanding for the standard provability predicate in Peano Arithmetic,\(\langle 1\rangle\) for \(\omega\)-provability, etcetera. GLP hasbeen axiomatized by starting from the axioms and rules of GL (seeSection 2), formulated separately for each \([n]\). In addition, GLP has threemixed 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 been endowed with a Kripke semantics with respect to which itis complete, and has also been shown to be arithmetically completewith respect to Peano Arithmetic (see Beklemishev 2010a, 2011a). Justlike for GL, the decision problem for GLP is PSPACE-complete(Shapirovsky 2008), while its closed fragment is polynomial timedecidable (Pakhomov 2014).

Over the last three decades, a number of results have been provedabout the polymodal logic GLP of strong provability predicates. Herefollow some particularly fruitful topics:

• the closed fragment of GLP (see Ignatiev 1993; Beklemishev,Joosten and Vervoort 2005);
• GLP and proof-theoretic ordinals (Beklemishev 2004);
• Neighbourhood semantics for GLP (Shamkanov 2020);
• Interpolation theorems for GLP (see Beklemishev 2010b, Shamkanov2011);
• The relationship between topological semantics and set theory,among others particular large cardinal axioms and stationaryreflection (see Beklemishev 2011b; Beklemishev and Gabelaia 2013,2014; Fernández-Duque 2014; Aguilera and Fernández-Duque2017).

5.5 Predicate provability logic

Finally, one can of course study predicate provability logic. Thelanguage is that of predicate logic without function symbols, togetherwith the operator \(\Box\). Here, the situation becomes much morecomplex than in the case of propositional provability logic. To beginwith, the straightforward quantified version of GL does not have thefixed-point property, is not complete with respect to any class ofKripke frames, and is not arithmetically complete with respect toPeano Arithmetic (Montagna, 1984; see Rybakov 2023 for recentgeneralizations). The question then arises: Is there any nicelyaxiomatized predicate provability logic that is adequate, provingexactly the valid principles of provability? The answer isunfortunately a resounding no: Vardanyan (1986) has proved on thebasis of ideas by Artemov (1985a) that the set of sentences ofpredicate provability logic all of whose realizations are provable inPA is not even recursively enumerable but \(\Pi^0_2\)-complete, so ithas no reasonable axiomatization. Visser and De Jonge (2006) showedthat there is no escape from Vardanyan’s theorem by proving ageneralization: For a wide range of arithmetical theories \(T\), theset of sentences of predicate provability logic all of whoserealizations are provable in \(T\) turns out to be\(\Pi^0_2\)-complete as well. Recently, however, Borges and Joosten(2020, 2022) showed that a fragment of predicate provability logicbased on a strictly positive language containing the propositionalconnective \(\wedge\), the modal operator \(\Diamond\), and thequantifier \(\forall\) is arithmetically complete and stilldecidable.

5.6 Other generalizations

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

• the provability logic of intuitionistic arithmetic (see Troelstra1973; Visser 1982, 1999, 2002, 2008; Iemhoff 2000, 2001, 2003;Ardeshir and Mojtahedi 2018; Litak and Visser 2018, forthcoming;Mojtahedi 2022 [Other Internet Resources]; Visser and Zoethout 2021;van der Giessen and Iemhoff 2021; van der Giessen 2023; Shillito2023);
• classification of provability logics (see Visser 1980, Artemov1985b, Beklemishev 1989, Beklemishev et al. 1999);
• Rosser orderings and proof speed-up (see Guaspari and Solovay1979, Švejdar 1983, Montagna 1992);
• several kinds of bimodal provability logics with provabilityoperators for different theories (see Carlson 1986; Smoryński1985; Beklemishev 1994, 1996; Visser 1995);
• provability logics for standard provability combined with unusualprovability predicates externally enumerating PA, such asFeferman’s and Parikh’s provability predicates and slowprovability predicates (see Feferman 1960; Parikh 1971; Montagna 1978;Visser 1989; Carbone and Montagna 1990; Shavrukov 1994; Lindström1994, 2006; Henk and Pakhomov 2016 (Other Internet Resources));
• analysis of Gödel’s second incompleteness theorem usingprovability and interpretability logics (Visser 2016; 2020);
• the logic of explicit proofs (see Artemov 1994, 2001; Artemov andMontagna 1994; Yavorskaya 2001; Artemov and Iemhoff 2007; Kuznets andStuder 2019);
• correspondence between provability logic andjustification logics (see Artemov and Nogina 2005; Shamkanov 2016 (Other InternetResources); Fitting 2020);
• relevant provability logic based on therelevance logic R (see Mares 2000);
• applications of provability logic in proof theory (see Beklemishev1999, 2003, 2004, 2005, 2006);
• proof theory of propositional modal logics closely related to theprovability logic GL, namely, Grzegorczyk logic (Grz) and weakGrezgorczyk logic (wGrz) (see Litak 2007; Maksimova 2014; Goréand Ramanayake 2014; Dyckhoff and Negri 2016; Savateev and Shamkanov2019, 2021);
• positive provability logics and reflection calculus (seeBeklemishev 2012, 2014, 2018a, 2018b; Dashkov 2012);
• generalizations of the polymodal provability logic GLP, namelyprovability logics with transfinitely many modalities (see Beklemishevet al. 2014; Fernández-Duque and Joosten 2013a, 2013b, 2014,2018; Joosten 2021; Beklemishev and Pakhomov 2022);
• relations between provability logic and the \(\mu\)-calculus (seevan Benthem 2006, Visser 2005, Alberucci and Facchini 2009); and
• provability algebras, also called diagonalizable algebras orMagari algebras (see Magari 1975a, 1975b; Montagna 1979, 1980a, 1980b;Bernardi and D’Aquino 1988; Shavrukov 1993a, 1993b, 1997;Zambella 1994; for recent results on their elementary theories, seePakhomov 2012, 2014a (Other Internet Resources), 2015.

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

6. Philosophical significance

Even though propositional provability logic is a modal logic with akind of “necessity” operator, it withstands Quine’s(1976) controversial critique of modal notions as unintelligible,already because of its clear and unambiguous arithmeticinterpretation. 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 whichones should be tautologies. In fact, provability logic embodies allthe desiderata that Quine (1953) set out for syntactic treatments ofmodality.

Quine’s main arrows were pointed towards modal predicate logics,especially the construction of sentences that contain modal operatorsunder the scope of quantifiers (“quantifying in”). Inpredicate provability logic, however, where quantifiers range overnatural numbers, bothde dicto andde re modalitieshave straightforward interpretations, contrary to the case of othermodal logics (see the note on thede dicto /de re distinction). For example, formulas like

are not at all problematic. If the number \(n\) is assigned to \(x\),then \(\Box \,\exists y\,(y = x)\) is true with respect to thisassignment iff the sentence \(\exists y\,(y=I_n)\) is provable inPeano Arithmetic; here, \(I_n\) is the numeral of \(n\), i.e., theterm \(\bs\bs\ldots\bs 0\) with \(n\) occurrences of the successoroperator \(\bs\). This sentence is true for all \(n\) in the standardmodel of the natural numbers, and \(\forall x \,\Box\, \exists y \,(y= x)\) is even provable in Peano Arithmetic.

By the way, the Barcan Formula

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

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

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

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

Thus, it seems misguided to compare the strength of both notions or tocombine them in one modal system.

Since the 1940s, there has been a lot of interest among philosophersof mathematics in the concept of informal provability orabsoluteprovability (Gödel 1946, Kreisel 1967), includingcontroversies about its proper definition (see Leach-Krouse 2013;Kennedy 2014; Crocco 2019; for good discussions of thesecontroversies). Williamson (2016) gives the following definition:“A mathematical hypothesis isabsolutely provable ifand only if it can in principle be known by a normal mathematicalprocess.”. At any rate, it is clear that the concept of absoluteprovability is very different from the concept offormalprovability in a given formal system, which is the central notionin the rest of this article on provability logic.

Related to the concept of absolutely provable statements is that ofabsolutely undecidable statements, namely, those statements\(A\) for which neither \(A\) nor \(\neg A\) is absolutely provable.An interesting question is whether Gödel’s Disjunctionholds: Is it the case that either “the mind cannot be mechanized” or “there are absolutely undecidable statements”?Fascinating takes on this question can be found in (Koellner 2016,Leach-Krouse 2016, Williamson 2016).

Discussions of the consequences of Gödel’s incompletenesstheorems 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; Franzén1995; Lindström 2001) for good critical discussions of suchclaims.

All in all, formal provability is a precisely defined concept, muchmore so than truth and knowledge. Thus,self-reference within the scope of provability does not lead to semantic paradoxeslike the Liar. Instead, it has led to some of the most importantresults about mathematics, such as Gödel’s incompletenesstheorems.

Bibliography

General references on provability logic

• Artemov, S.N., 2006, “Modal Logic in Mathematics,” inP. Blackburn, et al. (eds.),Handbook of Modal Logic,Amsterdam: Elsevier, pp. 927–970.
• Artemov, S.N. and L.D. Beklemishev, 2004, “ProvabilityLogic,” inHandbook of Philosophical Logic, SecondEdition, D. Gabbay and F. Guenthner, eds., Volume 13, Dordrecht:Kluwer, pp. 229–403.
• Boolos, G., 1979,The Unprovability of Consistency: An Essayin Modal Logic, Cambridge: Cambridge University Press.
• –––, 1993,The Logic of Provability,New York and Cambridge: Cambridge University Press.
• de Jongh, D.H.J. and G. Japaridze, 1998, “The Logic ofProvability,” inHandbook of Proof Theory, Buss, S.R.(ed.), Amsterdam: North-Holland, pp. 475-546.
• Lindström, P., 1996, “Provability Logic—A ShortIntroduction,”Theoria, 52(1–2):19–61.
• Segerberg, K., 1971,An Essay in Classical Modal Logic,Uppsala: Filosofiska Föreningen och Filosofiska Institutionen vidUppsala Universitet.
• Švejdar, V., 2000, “On Provability Logic,”Nordic Journal of Philosophy, 4: 95–116.
• Smoryński, C., 1984, “Modal Logic andSelf-Reference,” in D.M. Gabbay and F. Guenthner (eds.),Handbook of Philosophical Logic (Volume II: Extensions ofClassical Logic), Dordrecht: Springer, pp. 441–495.
• Smoryński, C., 1985,Self-Reference and Modal Logic,New York: Springer-Verlag.
• Verbrugge, R. 1996, “Provability” inTheEncyclopedia of Philosophy (Supplement), D.M. Borchert (ed.), NewYork: Simon and Schuster MacMillan, pp. 476–478.
• Visser, A., 1998, “Provability Logic,” inRoutledge 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 Emergenceof a Mathematical Modality,”Studia Logica, 50(1):1–23.
• Gödel, K., 1933, “Eine Interpretation desintuitionistischen Aussagenkalküls,”Ergebnisse einesMathematischen Kolloquiums, 4: 39–40; translation “AnInterpretation of the Intuitionistic Propositional Calculus,” inK. Gödel,Collected Works, S. Feferman et al. (eds.),Oxford and New York: Oxford University Press, Volume 1, 1986, pp.300–302.
• –––, 1931, “Über FormalUnentscheidbare Sätze der Principia Mathematica und VerwandterSysteme I,”Monatshefte für Mathematik und Physik,38: 173–198.
• Halbach, V., and A. Visser, 2014, “The HenkinSentence,” in M. Mazano, I. Sain, and E. Alonso (eds.),TheLife and Work of Leon Henkin: Essays on His Contributions,Dordrecht: Springer International Publishing, pp. 249–263.
• Henkin, L., 1952, “A Problem Concerning Provability,”Journal of Symbolic Logic, 17: 160.
• –––, 1954, “Review of G. Kreisel: On aProblem of Leon Henkin’s,”Journal of SymbolicLogic, 19(3): 219–220.
• Hilbert, D. and P. Bernays, 1939,Grundlagen derMathematik, volume 2, Berlin/Heidelberg/New York:Springer-Verlag.
• de Jongh, D.H.J., forthcoming, “Notes on my ScientificLife,” in N. Bezhanishvili, R. Iemhoff and F. Yang (eds.),Dick de Jongh on Intuitionistic and Provability Logic, Cham:Springer.
• Kreisel, G., 1953, “On a Problem of LeonHenkin’s,”Indagationes Mathematicae, 15:405–406.
• Lewis, C.I., 1912, “Implication and the Algebra ofLogic,”Mind, 21: 522–531.
• Löb, M.H., 1955, “Solution of a Problem of LeonHenkin,”Journal of Symbolic Logic, 20:115–118.
• Macintyre, A.J. and H. Simmons, 1973, “Gödel’sDiagonalization 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.
• –––, 1975b, “Representation and DualityTheory for Diagonalizable Algebras,”Studia Logica,34(4): 305–313.
• Smiley, T.J., 1963, “The Logical Basis of Ethics,”Acta Philosophica Fennica, 16: 237–246.
• Smoryński, C., 1991, “The Development ofSelf-reference: Löb’s Theorem,” in T. Drucker (ed.),Perspectives on the History of Mathematical Logic, Basel:Birkhäuser, pp. 110–133.

Cut-elimination for provability logic

• Avron, A., 1984, “On Modal Systems Having ArithmeticalInterpretations,”The Journal of Symbolic Logic, 49(3):935–942.
• Bílková, M., 2016, “Uniform Interpolation inProvability Logics,” in J. van Eijck, R. Iemhoff, and J.J.Joosten (eds.),Liber Amicorum Alberti: A Tribute to AlbertVisser, London: College Publications, pp. 57–90.
• Goré, R. and R. Ramanayake, 2008, “Valentini’sCut-Elimination for Provability Logic Resolved,” inAdvancesin Modal Logic (Volume 7), C. Areces and R. Goldblatt (eds.),London: College Publications, pp. 67–86.
• Goré, R. and R. Ramanayake, 2012, “Valentini’sCut-Elimination for Provability Logic Resolved,”Review ofSymbolic Logic, 5(2): 212–238.
• Goré, R., Ramanayake, R., and Shillito, I., 2021,“Cut-Elimination for Provability Logic by TerminatingProof-Search: Formalised and Deconstructed Using Coq,” inAutomated Reasoning with Analytic Tableaux and Related Methods:30th International Conference, TABLEAUX 2021, Cham: SpringerInternational Publishing, pp. 299–313.
• Maksimova, L.L., 1989a, “A Continuum of Normal Extensions ofModal Provability Logic with the Interpolation Property,”Sibirskii Matematicheskii Zhurnal, 30(6): 122–131.
• Maksimova, L.L., 1989b, “Definability Theorems in NormalExtensions of the Probability Logic,”Studia Logica,48(4): 495–507.
• Negri, S., 2005, “Proof Analysis in Modal Logic,”Journal of Philosophical Logic, 50: 507–544.
• Negri, S., 2014, “Proofs and Countermodels in Non-classicalLogics,”Logica Universalis, 8(1): 25–60.
• Poggiolesi, F., 2009, “A Purely Syntactic and Cut-freeSequent Calculus for the Modal Logic of Provability,”TheReview of Symbolic Logic, 2(4): 593–611.
• Rautenberg, W., 1983, “Modal Tableau Calculi andInterpolation,”Journal of Philosophical Logic, 12(4):403–423.
• Sambin, G., and S. Valentini, 1982, “The Modal Logic ofProvability. The Sequential Approach,”Journal ofPhilosophical Logic, 11(3): 311–342.
• Shamkanov, D.S., 2011, “Interpolation Properties forProvability Logics GL and GLP,”Proceedings of the SteklovInstitute of Mathematics, 274(1): 303–316.
• –––, 2014, “Circular Proofs for theGödel-Löb Provability Logic,”MathematicalNotes, 96(4): 575–585.
• –––, 2020, “Non-well-founded Derivationsin the Gödel-Löb Provability Logic,”Review ofSymbolic Logic, 13(4): 776–796.
• Smoryński, C., 1978, “Beth’s Theorem andSelf-referential Sentences,”Studies in Logic and theFoundations of Mathematics, 96: 253–261.
• Valentini, S., 1983, “The Modal Logic of Provability:Cut-Elimination,”Journal of Philosophical Logic, 12:471–476.

The fixed point theorem

• van Benthem, J., forthcoming, “An Abstract Look at theFixed-Point Theorem for Provability Logic,” in N. Bezhanishvili,R. Iemhoff and F. Yang (eds.),Dick de Jongh on Intuitionistic andProvability Logic, Cham: Springer.
• de Jongh, D.H.J., and F. Montagna, 1988, “Provable FixedPoints,”Zeitschrift fur mathematische Logik und Grundlagender Mathematik, 34(3): 229–250.
• Lindström, P., 2006, “Note on Some Fixed PointConstructions in Provability Logic,”Journal ofPhilosophical Logic, 35(3): 225–230.
• Reidhaar-Olson, L., 1990, “A New Proof of the Fixed-pointTheorem of Provability Logic,”Notre Dame Journal of FormalLogic, 31(1): 37–43.
• Sambin, G., 1976, “An Effective Fixed Point Theorem inIntuitionistic Diagonalizable Algebras (The Algebraization of theTheories Which Express Theor, IX),”Studia Logica 35:345–361.
• Sambin, G., and S. Valentini, 1982, “The Modal Logic ofProvability. The Sequential Approach,”Journal ofPhilosophical Logic, 11(3): 311–342.

Possible worlds semantics and topological semantics

• Abashidze, M., 1985, “Ordinal Completeness of theGödel-Löb Modal System,” (in Russian) inIntensional 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. 2009, “Ordinal Completeness of BimodalProvability Logic GLB,” InInternational Tbilisi Symposiumon Logic, Language, and Computation, Berlin: Springer-Verlag, pp.1–15.
• Beklemishev, L.D., G. Bezhanishvili, and T. Icard, 2009, “OnTopological Models of GLP,” in R. Schindler (ed.),Ways ofProof Theory (Ontos Mathematical Logic: Volume 2), Frankfurt:Ontos Verlag, pp. 133–153.
• van Benthem, J.F.A.K., 1979, “Syntactic Aspects of ModalIncompleteness Theorems,”Theoria, 45(2):63–77.
• Blass, A., 1990, “Infinitary Combinatorics and ModalLogic,”Journal of Symbolic Logic, 55(2):761–778.
• Esakia, L., 1981, “Diagonal Constructions, Löb’sFormula and Cantor’s Scattered Spaces,” (in Russian), in Studies in Logic and Semantics, Z. Mikeladze (ed.), Tbilisi:Metsniereba, pp. 128–143.
• –––, 2003, “Intuitionistic Logic andModality via Topology,”Annals of Pure and AppliedLogic, 127: 155–170.
• Goré, R., 2009, “Machine Checking Proof Theory: AnApplication of Logic to Logic,” InICLA ’09:Proceedings of the 3rd Indian Conference on Logic and ItsApplications, Berlin: Springer-Verlag, pp. 23–35.
• Hakli, R. and S. Negri, 2012, “Does the Deduction TheoremFail for Modal Logic?,”Synthese 187(3):849–867.
• Holliday, W.H. and Litak, T., 2019, “Complete Additivity andModal Incompleteness,”The Review of Symbolic Logic,12(3): 487–535.
• Icard, T.F. III, 2011, “A Topological Study of the ClosedFragment 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 ofInvestigation of Provability, Thesis in Philosophy (in Russian),Moscow.
• McKinsey, J.C.C. and A. Tarski, 1944, “The Algebra ofTopology,”Annals of Mathematics, 45:141–191.
• Shillito, I., 2023,New Foundations for the Proof Theory ofBi-Intuitionistic and Provability Logics Mechanized in Coq, Ph.D.Thesis, Canberra: The Australian National University.
• Verbrugge, R., 2021, “Zero-One Laws for Provability Logic:Axiomatizing Validity in Almost All Models and Almost AllFrames,” in L. Libkin (ed.),Proceedings of the 36th AnnualACM/IEEE Symposium on Logic in Computer Science (LICS), Rome:IEEE Press.

Provability and Peano Arithmetic

• Davis, M., 1958,Computability and Unsolvability, NewYork, McGraw-Hill; reprinted with an additional appendix, New York,Dover Publications 1983.
• Feferman, S., 1960, “Arithmetization of Metamathematics in aGeneral Setting,”Fundamenta Mathematicae, 49(1):35–92.
• Hájek, P. and P. Pudlák, 1993,Metamathematicsof First-Order Arithmetic, Berlin: Springer-Verlag.
• Solovay, R.M., 1976, “Provability Interpretations of ModalLogic,”Israel Journal of Mathematics, 25:287–304.

The scope of provability logic: boundaries

• Berarducci, A. and R. Verbrugge, 1993, “On the ProvabilityLogic of Bounded Arithmetic,”Annals of Pure and AppliedLogic, 61: 75–93.
• Buss, S.R., 1986,Bounded Arithmetic, Naples:Bibliopolis.
• de Jongh, D.H.J., M. Jumelet and F. Montagna, 1991, “On theProof of Solovay’s Theorem,”Studia Logica,50(1): 51–70.
• Parikh, R., 1971, “Existence and Feasibility inArithmetic“,The Journal of Symbolic Logic, 36(3):494–508.

Interpretability logic

• Areces, C., Hoogland, E. and de Jongh, D.H.J., 2001,“Interpolation, Definability and Fixed-points inInterpretability Logics“, in M. Zakharyaschev, K. Segerberg, M.de Rijke and H. Wansing (eds.),Advances in Modal Logic(Volume 2), Stanford: CSLI Publications, pp. 35–58.
• Berarducci, A., 1990, “The Interpretability Logic of PeanoArithmetic,”Journal of Symbolic Logic, 55:1059–1089.
• Bílková, M., de Jongh, D. and Joosten, J.J., 2009,“Interpretability in PRA,”Annals of Pure and AppliedLogic, 161(2): 128–138.
• de Jongh, D.H.J., and F. Veltman, 1990, “Provability Logicsfor Relative Interpretability,” in P.P. Petkov (ed.),Mathematical Logic: Proceedings of the Heyting 1988 Summer Schoolin Varna, Bulgaria, Boston: Plenum Press, pp. 31–42.
• de Jongh, D.H.J., and A. Visser, 1991, “Explicit FixedPoints in Interpretability Logic,”Studia Logica,50(1): 39–49.
• Joosten, J.J., and Visser, A., 2000, “The InterpretabilityLogic of All Reasonable Arithmetical Theories,”Erkenntnis, 53(1-2): 3–26.
• Joosten, J.J., Mas Rovira, J., Mikec, L., and Vuković, M.,forthcoming, “An Overview of Verbrugge Semantics, a.k.a.Generalised Veltman Semantics,” in N. Bezhanishvili, R. Iemhoffand F. Yang (eds.),Dick de Jongh on Intuitionistic andProvability Logic, Cham: Springer.
• Mikec, L. and Vuković, M., 2020, “InterpretabilityLogics and Generalised Veltman Semantics,”The Journal ofSymbolic Logic, 85(2): 749–772.
• Montagna, F., 1987, “Provability in Finite Subtheories ofPA,”Journal of Symbolic Logic, 52(2):494–511.
• Shavrukov, V.Yu., 1988, “The Logic of RelativeInterpretability over Peano Arithmetic,” Technical Report No. 5,Moscow: Steklov Mathematical Institute (in Russian).
• Švejdar, V., 1983, “Modal Analysis of GeneralizedRosser Sentences,”Journal of Symbolic Logic, 48:986–999.
• Visser, A., 1990, “Interpretability Logic,” in P.P.Petkov (ed.),Mathematical Logic: Proceedings of the Heyting 1988Summer School in Varna, Bulgaria, Boston: Plenum Press, pp.175–209.
• –––, 1998, “An Overview ofInterpretability Logic,” in M. Kracht et al. (eds.),Advances in Modal Logic (Volume 1), Stanford: CSLIPublications, pp. 307–359.

Propositional quantifiers

• Artemov, S.N. and L.D. Beklemishev, 1993, “On PropositionalQuantifiers in Provability Logic,”Notre Dame Journal ofFormal Logic, 34: 401–419.
• Shavrukov, V.Yu., 1997, “Undecidability in DiagonalizableAlgebras,”Journal of Symbolic Logic, 62:79–116.

Japaridze’s bimodal and polymodal provability logics

• Beklemishev, L.D., 2004, “Provability Algebras andProof-Theoretic Ordinals, I,”Annals of Pure and AppliedLogic, 128: 103–123.
• –––, 2010a, “Kripke Semantics forProvability Logic GLP,”Annals of Pure and AppliedLogic, 161(6): 756–774.
• –––, 2010b, “On the Craig Interpolationand the Fixed Point Properties of GLP,” in S. Feferman et al.(eds.),Proofs, Categories and Computations (Tributes, 13),London: College Publications, pp. 49–60.
• –––, 2011a, “A Simplified Proof ofArithmetical Completeness Theorem for Provability Logic GLP,”Proceedings Steklov Institute of Mathematics, 274(1):25–33.
• –––, 2011b, “Ordinal Completeness ofBimodal Provability Logic GLB,” in N. Bezhanishvili et al.(eds.),Logic, Language, and Computation, 8th InternationalTbilisi Symposium TbiLLC 2009 (Lecture Notes in Computer Science:Volume 6618), Heidelberg: Springer, pp. 1–15.
• Beklemishev, L.D., and D. Gabelaia, 2013, “TopologicalCompleteness of the Provability Logic GLP,”Annals of Pureand Applied Logic, 164(12): 1201–1223.
• –––, 2014, “Topological Interpretations ofProvability Logic,“ in G. Bezhanishvili (ed.),Leo Esakia onDuality in Modal and Intuitionistic Logics (OutstandingContributions to Logic: Volume 4), Heidelberg: Springer, pp.257–290.
• Beklemishev, L.D., J. Joosten and M. Vervoort, 2005, “AFinitary Treatment of the Closed Fragment of Japaridze’sProvability Logic,”Journal of Logic and Computation,15(4): 447–463.
• Fernández-Duque, D. and J.J. Joosten, 2014,“Well-orders on the Transfinite Japaridze Algebra,”Logic Journal of the IGPL, 22 (6): 933–963.
• Fernández-Duque, D. and Joosten, J.J., 2018, “TheOmega-Rule Interpretation of Transfinite Provability Logic,”Annals of Pure and Applied Logic, 169(4): 333–371.
• Ignatiev, K.N., 1993, “On Strong Provability Predicates andthe Associated Modal Logics,”Journal of SymbolicLogic, 58: 249–290.
• Japaridze, G., 1988, “The Polymodal ProvabilityLogic,” InIntensional Logics and the Logical Structure ofTheories: Material from the Fourth Soviet-Finnish Symposium onLogic, Telavi, pp. 16–48.
• Pakhomov, F.N., 2014, “On the Complexity of the ClosedFragment of Japaridze’s Provability Logic,”Archivefor Mathematical Logic, 53(7-8): 949–967.
• Shamkanov, D., 2020, “Global Neighbourhood Completeness ofthe Provability Logic GLP,” in N. Olivetti, R. Verbrugge, S.Negri, and G. Sandu (eds.),Proceedings Advances in ModalLogic (Volume 13), London: College Publications, pp.581–595.

Predicate provability logic

• Artemov, S.N., 1985a, “Nonarithmeticity of Truth PredicateLogics of Provability,”Doklady Akademii Nauk SSSR,284: 270–271 (in Russian); English translation inSovietMathematics Doklady, 32: 403–405.
• Borges, A.A. and Joosten, J.J., 2020, “Quantified ReflectionCalculus with One Modality,” in N. Olivetti, R. Verbrugge, S.Negri, and G. Sandu (eds.),Proceedings Advances in ModalLogic (Volume 13), London: College Publications, pp.13–32.
• –––, 2022, “An Escape fromVardanyan’s Theorem,”The Journal of SymbolicLogic, first online 13 May 2022. doi:10.1017/jsl.2022.38
• Borges, A.A., 2022, “Towards a Coq Formalization of aQuantified Modal Logic,” in C. Benzmüller and J. Otten(eds.),Proceedings of the 4th Workshop on Automated Reasoning inQuantified Non-Classical Logics (ARQNL 2022), CEUR WorkshopProceedings, pp. 13–27.
• McGee, V. and G. Boolos, 1987, “The Degree of the Set ofSentences of Predicate Provability Logic that are True under EveryInterpretation,”Journal of Symbolic Logic, 52:165–171.
• Montagna, F., 1984, “The Predicate Modal Logic ofProvability,”Notre Dame Journal of Formal Logic,25(2): 179–189.
• Rybakov, M., 2023, “Predicate Counterparts of Modal Logicsof Provability: High Undecidability and Kripke Incompleteness,”Logic Journal of the IGPL, first online 28 February 2023.doi:10.1093/jigpal/jzad002
• Vardanyan, V.A., 1986, “Arithmetic Complexiy of PredicateLogics of Provability and their Fragments,”Doklady AkademiiNauk SSSR, 288: 11–14 (in Russian); English translation inSoviet Mathematics Doklady, 33: 569–572.
• Visser, A. and M. de Jonge, 2006, “No Escape fromVardanyan’s Theorem,”Archive of MathematicalLogic, 45(5): 539–554.

Other generalizations

• Aguilera, J.P. and Fernández-Duque, D., 2017, “StrongCompleteness of Provability Logic for Ordinal Spaces,”TheJournal of Symbolic Logic, 82(2): 608–628.
• Alberucci, L., and A. Facchini, 2009, “On Modalμ-Calculus and Gödel-Löb logic,”StudiaLogica, 91: 145–169.
• Ardeshir, M. and Mojtahedi, M., 2018, “The\(Σ_1\)-Provability Logic of HA,”Annals of Pure andApplied Logic, 169(10): 997–1043.
• Artemov, S.N., 1985b,“On Modal Logics AxiomatizingProvability,”Izvestiya Akadademii Nauk SSSR, SeriyaMatematicheskaya, 49(6): 1123–1154 (in Russian); Englishtranslation inMathematics of the USSR–Izvestiya,27(3): 402–429.
• –––, 1994, “Logic of Proofs,”Annals of Pure and Applied Logic, 67(2): 29–59.
• –––, 2001, “Explicit Provability andConstructive Semantics,”Bulletin of Symbolic Logic, 7:1–36.
• Artemov, S.N. and R. Iemhoff, 2007, “The BasicIntuitionistic Logic of Proofs,”Journal of SymbolicLogic, 72(2): 439–451.
• Artemov, S.N. and F. Montagna, 1994, “On First-orderTheories with Provability Operator,”Journal of SymbolicLogic, 59(4): 1139–1153.
• Artemov, S.N. and Nogina, E., 2005, “IntroducingJustification into Epistemic Logic,”Journal of Logic andComputation, 15(6): 1059–1073.
• Beklemishev, L.D., 1989, “On the Classification ofPropositional Provability Logics,”Izvestiya Akademii NaukSSSR, Seriya Matematicheskaya., 53(5): 915–943 (inRussian); English translation inMathematics of theUSSR–Izvestiya, 35 (1990) 247–275.
• –––, 1994, “On Bimodal Logics ofProvability,”Annals of Pure and Applied Logic, 68:115–160.
• –––, 1996, “Bimodal Logics for Extensionsof Arithmetical Theories,”Journal of Symbolic Logic,61: 91–124.
• –––, 1999, “Parameter-Free Induction andProvably Total Computable Functions,”Theoretical ComputerScience, 224: 13–33.
• –––, 2003, “Proof-theoretic Analysis byIterated Reflection,”Archive for Mathematical Logic,6(42): 515–552.
• –––, 2005, “Reflection Principles andProvability Algebras in Formal Arithmetic,”UspekhiMatematicheskikh Nauk, 60(2): 3–78. (in Russian); Englishtranslation in:Russian Mathematical Surveys, 60(2):197–268.
• –––, 2006, “The Worm Principle,” inLecture Notes in Logic 27. Logic Colloquium ’02, Z.Chatzidakis, P. Koepke, and W. Pohlers (eds.), Natick (MA): AK Peters,pp. 75–95.
• –––, 2012, “Calibrating Provability Logic:From Modal Logic to Reflection Calculus,” in T. Bolander, T.Braüner, S. Ghilardi, and L. Moss (eds.),Advances in ModalLogic (Volume 9), London: College Publications, pp.89–94.
• –––, 2014, “Positive Provability Logic forUniform Reflection Principles,”Annals of Pure and AppliedLogic, 165 (1): 82–105.
• –––, 2018a, “A Note on Strictly PositiveLogics and Word Rewriting Systems,” in S. Odintsov (ed.),Larisa Maksimova on Implication, Interpolation, andDefinability (Outstanding Contributions to Logic: Volume 15),Cham: Springer, pp.61–70.
• –––, 2018b, “Reflection Calculus andConservativity Spectra “,Russian Mathematical Surveys,73(4): 569–613.
• Beklemishev, L.D., D. Fernández-Duque, and J.J. Joosten,2014, “On Provability Logics with Linearly OrderedModalities,”Studia Logica, 102(3): 541–566.
• Beklemishev, L. D., and Pakhomov, F. N., 2022, “ReflectionAlgebras and Conservation Results for Theories of IteratedTruth,”Annals of Pure and Applied Logic, 173(5):103093.
• Beklemishev, L.D., M. Pentus and N. Vereshchagin, 1999,Provability, Complexity, Grammars, American MathematicalSociety Translations (Series 2, Volume 192).
• Beklemishev, L.D. and A. Visser, 2006, “Problems in theLogic of Provability,” in D.M. Gabbay, S.S. Goncharov and M.Zakharyashev (eds.),Mathematical Problems from Applied Logic I:Logics for the XXIst Century (International Mathematical Series,Volume 4), New York: Springer, pp. 77–136.
• van Benthem, J., 2006, “Modal Frame Correspondences andFixed-points,”Studia Logica, 83(1-3):133–155.
• Bernardi, C. and D’Aquino, P., 1988, “TopologicalDuality for Diagonalizable Algebras“,Notre Dame Journal ofFormal Logic, 29(3): 345–364.
• Carbone, A. and Montagna, F., 1990, “Much Shorter Proofs: ABimodal Investigation,”Mathematical Logic Quarterly,36(1): 47–66.
• Carlson, T., 1986, “Modal Logics with Several Operators andProvability Interpretations,”Israel Journal ofMathematics, 54(1): 14–24.
• Dashkov, E.V., 2012, “On the Positive Fragment of thePolymodal Provability Logic GLP,”Mathematical Notes,91 (3): 318–333.
• Dyckhoff, R and Negri, S., 2016, A Cut-free Sequent System forGrzegorczyk Logic, with an Application to theGödel–McKinsey–Tarski Embedding,Journal of Logicand Computation, 26: 169–187.
• Fernández-Duque, D., 2014, “The Polytopologies ofTransfinite Provability Logic,“Archive for MathematicalLogic, 53(3-4): 385–431.
• Fernández-Duque, D. and J.J. Joosten, 2013a,“Hyperations, Veblen Progressions, and Transfinite Iteration ofOrdinal Functions,”Annals of Pure and Applied Logic164 (7-8): 785–801, [available online].
• Fernández-Duque, D. and J.J. Joosten, 2013b, “Modelsof Transfinite Provability Logic,”Journal of SymbolicLogic, 78(2): 543–561, [available online].
• van der Giessen, I., 2023, “Admissible Rules for SixIntuitionistic Modal Logics,”Annals of Pure and AppliedLogic, 174(4): 103233.
• van der Giessen, I. and Iemhoff, R., 2021, “Sequent Calculifor Intuitionistic Gödel–Löb Logic,”NotreDame Journal of Formal Logic, 62(2): 221–246.
• Goré, R and Ramanayake, R., 2014, “Cut-eliminationfor Weak Grzegorczyk Logic Go,”Studia Logica, 102(1):1–27.
• Guaspari, D. and R.M. Solovay, 1979, “RosserSentences,”Annals of Mathematical Logic, 16:81–99.
• Iemhoff, R., 2000, “A Modal Analysis of some Principles ofthe Provability Logic of Heyting Arithmetic,” inAdvances inModal Logic (Volume 2), M. Zakharyashev et al. (eds.), Stanford:CSLI Publications, pp. 319–354.
• –––, 2001, “On the Admissible Rules ofIntuitionistic Propositional Logic,”Journal of SymbolicLogic, 66: 281–294.
• –––, 2003, “Preservativity Logic: AnAnalogue of Interpretability Logic for Constructive Theories,”Mathematical Logic Quarterly, 49(3): 1–21.
• Iemhoff, R., de Jongh, D. and Zhou, C., 2005, “Properties ofIntuitionistic Provability and Preservativity Logics,”LogicJournal of the IGPL, 13(6): 615–636.
• Joosten, J.J., 2021, “Münchhausen Provability,”The Journal of Symbolic Logic, 86(3): 1006–1034.
• Kuznets, R. and Studer, T., 2019,Logics of Proofs andJustifications, London: College Publications.
• Lindström, P., 1994, “The Modal Logic of ParikhProvability,”Filosofiska Meddelanden, GrönaSerien, Gothenburg: Göteborgs Universitetet.
• Lindström, P., 2006, “On Parikh Provability: AnExercise in Modal Logic,” in H. Lagerlund, S. Lindström,and R. Sliwinski (eds.),Modality Matters: Twenty-Five Essays inHonour of Krister Segerberg, Uppsala: Uppsala PhilosophicalStudies (Volume 53), pp. 53–287.
• Litak, L., 2007, “The Non-Reflexive Counterpart ofGrz,”Bulletin of the Section of Logic, 36(3–4):195–208.
• Litak, T. and Visser, A., 2018, “Lewis Meets Brouwer:Constructive Strict Implication,”IndagationesMathematicae, 29(1): 36–90.
• –––, forthcoming, “Lewisian Fixed PointsI: Two Incomparable Constructions,” in N. Bezhanishvili, R.Iemhoff and F. Yang (eds.),Dick de Jongh on Intuitionistic andProvability Logic, Cham: Springer.
• Maksimova, L.L., 2014, “The Lyndon Property and UniformInterpolation over the Grzegorczyk Logic,”SiberianMathematical Journal, 55(1): 118–124.
• Mares, E.D., 2000, “The Incompleteness of RGL,”Studia Logica, 65: 315–322.
• Mojtahedi, M., forthcoming, “The \(Σ_1\)-provabilitylogic of HA revisited,” in N. Bezhanishvili, R. Iemhoff and F.Yang (eds.),Dick de Jongh on Intuitionistic and ProvabilityLogic, Cham: Springer.
• Montagna, F.,1978, “On the algebraization of aFeferman’s predicate,”Studia Logica, 37(3):221–236.
• –––, 1979, “On the Diagonalizable Algebraof Peano Arithmetic,”Bollettino della Unione MatematicaItaliana, B(5), 16: 795–812.
• –––, 1980a, “Interpretations of theFirst-order Theory of Diagonalizable Algebras in PeanoArithmetic,”Studia Logica, 39: 347–354.
• –––, 1980b, “Undecidability of theFirst-order Theory of Diagonalizable Algebras, ”StudiaLogica, 39: 355–359.
• –––, 1992, “Polynomially andSuperexponentially Shorter Proofs in Fragments of Arithmetic,”Journal of Symbolic Logic, 57: 844–863.
• Pakhomov, F.N., 2012, “Undecidability of the ElementaryTheory of the Semilattice of GLP-words,”Sbornik:Mathematics, 203(8): 1211.
• Pakhomov, F.N., 2015, “On Elementary Theories of OrdinalNotation Systems Based on Reflection Principles,”Proceedings of the Steklov Institute of Mathematics, 289:194–212.
• Savateev, Y., and Shamkanov, D., 2019, “Cut Elimination forthe Weak Modal Grzegorczyk Logic via Non-well-founded Proofs,”in R. Iemhoff, M. Moortgat, M. and R. de Queiroz (eds.),Proceedings of WoLLIC 2019, Heidelberg: Springer, pp.569–583.
• –––, 2021, “Non-well-founded Proofs forthe Grzegorczyk Modal Logic,”The Review of SymbolicLogic, 14(1): 22–50.
• Shamkanov, D.S., 2016, “A Realization Theorem for theGödel–Löb Provability Logic,”Sbornik:Mathematics, 207(9): 1344–1360.
• Shapirovsky, I., 2008, “PSPACE-decidability ofJaparidze’s Polymodal Logic,”Advances in ModalLogic, 7: 289–304.
• Shavrukov, V.Yu., 1993a, “A Note on the DiagonalizableAlgebras of PA and ZF,”Annals of Pure and AppliedLogic, 61: 161–173.
• –––, 1993b, “Subalgebras of DiagonalizableAlgebras of Theories Containing Arithmetic,”DissertationesMathematicae, 323.
• –––, 1994, “A Smart Child ofPeano’s,”Notre Dame Journal of Formal Logic,35(2): 161–185.
• Troelstra, A.S., 1973,Metamathematical Investigation ofIntuitionistic Arithmetic and Analysis, Berlin:Springer-Verlag.
• Visser, A., 1980,Aspects of Diagonalization andProvability, Ph.D. Thesis, Utrecht: University of Utrecht.
• –––, 1982, “On the Completeness Principle:A Study of Provability in Heyting’s Arithmetic andExtensions,”Annals of Mathematical Logic, 22(3):263–295.
• –––, 1989, “Peano’s Smart Children:A Provability Logical Study of Systems with Built-inConsistency,”Notre Dame Journal of Formal Logic,30(2): 161–196.
• –––, 1995, “A Course on BimodalProvability Logic,”Annals of Pure and Applied Logic,73(1): 109–142.
• –––, 1999, “Rules and Arithmetics,”Notre Dame Journal of Formal Logic, 40(1):116–140.
• –––, 2002, “Substitutions of \(\Sigma_1\)Sentences: Explorations between Intuitionistic Propositional Logic andIntuitionistic Arithmetic,”Annals of Pure and AppliedLogic, 114: 227–271.
• –––, 2005, “Löb’s Logic Meetsthe μ-Calculus,” in A. Middeldorp, V. van Oostrom, F. vanRaamsdonk and R. de Vrijer (eds.),Processes, Terms and Cycles:Steps on the Road to Infinity, Berlin: Springer, pp.14–25.
• –––, 2008, “Closed Fragments ofProvability Logics of Constructive Theories,”Journal ofSymbolic Logic, 73: 1081–1096.
• –––, 2016, “The Second IncompletenessTheorem: Reflections and Ruminations,” in L. Horsten and P.Welch (eds.),Gödel’s Disjunction: The Scope and Limitsof Mathematical Knowledge, Oxford: Oxford University Press, pp.67–91.
• –––, 2020, “Another Look at the SecondIncompleteness Theorem,”The Review of Symbolic Logic,13(2): 269–295.
• Visser, A. and Zoethout, J., 2019, “Provability Logic andthe Completeness Principle,”Annals of Pure and AppliedLogic, 170(6): 718–753.
• Yavorskaya, T., 2001, “Logic of Proofs andProvability,”Annals of Pure and Applied Logic,113(1-3): 345–372.
• Zambella, D., 1994, “Shavrukov’s Theorem on theSubalgebras of Diagonalizable Algebras for Theories Containing \(I\Delta_0 + \exp\),”Notre Dame Journal of Formal Logic,35: 147–157.

Philosophical significance

• Crocco, G., 2019, “Informal and Absolute Proofs: SomeRemarks from a Gödelian Perspective,”Topoi, 38:561–575.
• Davis, M., 1990, “Is Mathematical InsightAlgorithmic?,” Commentary on Roger Penrose, The Emperor’sNew Mind,Behavioral and Brain Sciences, 13:659–660.
• –––, 1993, “How Subtle isGödel’s Theorem? More on Roger Penrose” (Commentaryon Roger Penrose, The Emperor’s New Mind),Behavioral andBrain Sciences, 16: 611–612.
• Egré, P., 2005, “The Knower Paradox in the Light ofProvability Interpretations of Modal Logics,”Journal ofLogic, Language, and Information, 14(1): 13–48.
• Franzén, T., 2005,Gödel’s Theorem: AnIncomplete Guide to its Use and Abuse, Boca Raton, Florida: CRCPress.
• Gödel, K., 1946, “Remarks Before the PrincetonBicentennial Conference on Problems in Mathematics,” reprintedin S. Feferman et al. (eds.),Kurt Gödel Collected Works,Volume II: Publications 1938–1975, New York, Oxford: OxfordUniversity Press, 1990, pp. 150–153.
• Kaplan, D. and R. Montague, 1960, “A ParadoxRegained,”Notre Dame Journal of Formal Logic, 1(3):79–90.
• Kennedy, J., 2014, “Gödel’s 1946 PrincetonBicentennial Lecture: An Appreciation,” in J. Kennedy (ed.),Interpreting Gödel: Critical Essays, Cambridge:Cambridh=ge University Press, pp.109–130.
• Koellner, P., 2016, “Gödel’s Disjunction,”in L. Horsten and P. Welch (eds.),Gödel’s Disjunction:The Scope and Limits of Mathematical Knowledge, Oxford: OxfordUniversity Press, pp. 148–188.
• Kreisel, G., 1967, “Informal Rigour and CompletenessProofs,” in I. Lakatos (ed.),Problems in the Philosophy ofMathematics, Amsterdam: North-Holland, pp. 138–157.
• Leach-Krouse, G.E., 2013, “Conceptions of AbsoluteProvability,” Ph.D. Thesis, Note Dame: Notre DameUniversity.
• Leach-Krouse, G.E., 2016, “Provability, Mechanism, and theDiagonal Problem,” in L. Horsten and P. Welch (eds.),Gödel’s Disjunction: The Scope and Limits ofMathematical Knowledge, Oxford: Oxford University Press, pp.211–242.
• Lindström, P, 2001, “Penrose’s NewArgument,”Journal of Philosophical Logic, 30:241–250.
• Montague, R., 1963, “Syntactical Treatments of Modality,with Corollaries on Reflection Principles and FiniteAxiomatizability,”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.
• –––, 1953, “Three Grades of ModalInvolvement,” inProceedings of the 11th InternationalCongress of Philosophy, Amsterdam: North-Holland, pp. 65-81;reprinted in W.V. Quine,The Ways of Paradox and OtherEssays, New York: Random House, 1966, pp. 156–174.
• de Vos, M., Verbrugge, R., and Kooi, B., 2023, “Solutions tothe Knower Paradox in the Light of Haack’s Criteria,”Journal of Philosophical Logic, 52: 1101–1132.
• Williamson, T., 2016, “Absolute Provability and SafeKnowledge of Axioms,” in L. Horsten and P. Welch (eds.),Gödel’s Disjunction: The Scope and Limits ofMathematical Knowledge, pp. 243–253.

Academic Tools

	How to cite this entry.
	Preview the PDF version of this entry at theFriends of the SEP Society.
	Look up topics and thinkers related to this entry at the Internet Philosophy Ontology Project (InPhO).
	Enhanced bibliography for this entryatPhilPapers, with links to its database.

Other Internet Resources

Papers and Presentations

• Férée, H., I. van der Giessen, S. van Gool, and I.Shillito, 2024, “Mechanised Uniform Interpolation for Modal Logics K, GL and iSL”, manuscript at arxiv.org.
• Fitting, M., 2020, “A Second GL Justification Logic,” manuscript available on the author’s website.
• Goré, R. and J. Kelly, 2007, “Automated Proof Search in Gödel-Löb Provability Logic,” presented at theBritish Logic Colloquium 2007.
• Henk, P., and Pakhomov, F., 2016, “Slow and Ordinary Provability for Peano Arithmetic,” manuscript at arxiv.org.
• Mojtahedi, M., 2022, “On Provability Logic of HA,” manuscript at arxiv.org.
• Pakhomov, F., 2014a, “On Elementary Theories of GLP-algebras,” manuscript at arxiv.org.
• Verbrugge, Rineke,Presentation slides on provability logic, slides, University of Groningen
• Visser, Albert, 1986,On formal provability versus human provability (in Dutch), online manuscript, University of Utrecht.

Other Sites

• Open problems in Provability Logic, maintained by Lev Beklemishev
• Mailing list Foundations of Mathematics, New York University

Related Entries

artificial intelligence: logic-based |computability and complexity |Curry’s paradox |Fitch’s paradox of knowability |Gödel, Kurt |Gödel, Kurt: incompleteness theorems |Hilbert, David: program in the foundations of mathematics |logic, history of: modal logic |logic: classical |logic: epistemic |logic: intuitionistic |logic: justification |logic: modal |logic: relevance |mathematics, philosophy of |mathematics: constructive |model theory |possible worlds |Principia Mathematica |proof theory: development of |Quine, Willard Van Orman |self-reference |set theory: independence and large cardinals |Turing, Alan

Acknowledgments

I would like to express my immense gratitude to Lev Beklemishev, whowas so kind as to write me a long letter in 2017, including manyliterature references to developments in provability logic as seenfrom his perspective. Thanks are also due to Albert Visser, SaraUckelman, Rajeev Goré, Giovanni Sambin, VítězslavŠvejdar, Sara Negri, Joost Joosten, Ian Shillito, WesleyHolliday, Revantha Ramanayake, Anupam Das, Shawn Standefer, TobyMeadows, Edson Bezerra, Nils Kürbis, and Tadeusz Litak for theirsuggestions of improvements and additions to the 2017 and/or 2024versions of this article.

This 2024 version of the article on provability logic is dedicated tothe memory of three Nestors of provability logic and themeta-mathematics of first-order arithmetic: Franco Montagna(1948–2015), Sol Feferman (1928–2016), and PetrHájek (1940–2016).