This post works through some technical details in the Gödel-Löb provability logic , especially as they are relevant to a paper by LaVictoire et al discussed in the previous post. Subsection 4.2 of that post explores as a useful tool for the task at hand, deferring some standard technical details until this post.
After reviewing some definitions in Section 1, Section 2 covers the normal form theorem, from which it follows that sentences of without propositional variables can be algorithmically classified as true or false in the standard model of arithmetic. By contrast, the Kripke semantics covered in the final Section 4 allows any formula (with or without variables) to be algorithmically classified as provable or unprovable in . My main source for these sections is George Boolos’ The Logic of Provability.
(Another point of contrast: Solovay’s completeness theorem, which we do not cover here, establishes that the formulas proved in are exactly those which whose every instance is provable in Peano Arithmetic, with propositional variables replaced by Gödel numbers of arithmetical sentences, and the modality replaced by ‘s provability predicate. It is the right-to-left implication that is non-trivial.)
Section 3 gives Per Lindström’s simple proof of the fixed point theorem for as in his article Provability Logic: A Short Introduction. The fixed point theorem is analogous to Gödel’s diagonal lemma for constructing self-referential sentences, and is actually the main result needed by LaVictoire et al.
Recall that formulas in are built up from , the propositional variables , , etc., the connective (from which the other standard connectives can be derived), and the modal symbol intended to capture the behavior of the provability predicate in Peano Arithmetic. The axioms for are:
- All propositional tautologies
- Formal Löb’s theorem: .
The rules of inference are:
- Modus Ponens: From and , conclude
- Necessitation: From , conclude .
Before moving on to the normal form theorem, we list two useful redundant axioms (in that they are theorems), and one useful redundant rule of inference:
- Alternate distribution:
- Formal necessitation:
- Löb’s rule: From , conclude .
2. Normal Forms
There’s an effective procedure for determining the truth or falsity of sentences without propositional variables. For example, the sentence is not provable in , but is true when interpreted in the standard model as the statement that Peano Arithmetic is consistent.
This sentence is one of a whole family of true sentences , for expressing that there’s no proof that there’s a proof (and so forth…) of . Here means , and means .
The following normal form theorem says that any sentence without propositional variables is provably equivalent to a propositional combination of sentences of the form ; such a sentence is said to be in normal form. Since is false for all , one can compute the truth value of a normal form sentence by simply deleting every symbol in it, and computing the value of the propositional combination of ‘s that remains!
Or viewed another way, since for (by the schema , or trivially if ), any normal form sentence is decidable from a sufficiently strong (true) hypothesis . That is, when is at least as large as the highest “power” on a in , then either
This is a kind of completeness theorem for .
Theorem 1 (Normal Form Theorem) For any sentence with no propositional variables, there is [one can construct] a normal form sentence with .
Proof: Obviously is in normal form, and if and are provably equivalent to normal form sentences and , then
with in normal form.
If , then by Necessitation. Then distributes correctly over and such that . Thus to complete the proof, it suffices to show that can be put in normal form whenever is in normal form.
Fix such , and put it in conjunctive normal form; that is, with some manipulation via propositional tautologies, we can write an equivalent sentence which is a conjunction of disjunctions of ‘s and ‘s. Since the provably distributes over conjunctions, it suffices to show for such a disjunction that is equivalent to a normal form sentence.
So let be just such a disjunction,
for some finite index sets and . We can assume without loss of generality that , by adding to , which is akin to replacing with . Using the schema and its contrapositive, we can rewrite by replacing each of the “big” disjunctions with its weakest disjunct. If , then with , ,
If , then is equivalent to (i.e. to ), and hence so is , as by Necessitation.
In the final case , we’ll use (1) to show that is equivalent to . For the right-to-left implication, start with the tautology
By Necessitation and distribution,
Also using Necessitation and distribution in (1), we can see that the consequent implies (actually is equivalent to) .
For the left-to-right implication, since (and so ),
The hypothesis is equivalent to , and the consequent looks amenable to Löb’s theorem. That is, introduce another with Necessitation and distribution
Then by the Löb axiom for , we have
completing the proof.
3. Fixed Point Theorem
The fixed point theorem establishes that supports self-referential sentences, provided all self-reference occurs within the scope of a .
Specifically, we say that a formula is modalized in if every occurrence of is within the scope of a . For instance is not modalized in , but is. To provide a suitable notation for substitution, we often write a formula as , understanding that needn’t actually occur in and that there may be variables distinct from occurring in .
Given another sentence , write for the result of substituting for all occurrences of in , relying on context to make clear which variable is to be replaced with . Note that unlike systems such as first-order logic (or the lambda calculus or programming languages), there’s no such thing as a “bound variable” in , so substitution can be performed naïvely.
Moreover, is unique up to provable equivalence: any other fixed point of has .
Two familiar examples of (the uniqueness clause of) the fixed point theorem have or . Interpreted as statements of Peano Arithmetic, fixed points of the first are the Gödel sentences asserting their own unprovability. It’s fairly straightforward to show that such sentences are equivalent in to , hence Gödel’s second incompleteness theorem falls out of his proof of the first. As expected then, is the unique fixed point of in .
Fixed points of the second are the “truth-teller” sentences asserting their own provability. In , they are proved by Löb’s theorem; in , is the unique fixed point of .
The proof of the fixed point theorem in this section is taken from Lindström’s Provability Logic: A Short Introduction. It seems to be the simplest proof around. Boolos’ The Logic of Provability provides three alternate proofs, the first of which is not much longer than this, provided one has already developed the Kripke semantics (as in Section 4); Lindström’s proof is purely syntactic.
To prove the fixed point theorem, we’ll need some lemmas to the effect that substitution preserves logical equivalence as you would expect. To get one of the inductions to go through, we have to introduce the slightly awkward notation to stand for . Since and and so forth are all theorems of , implies every member of the family for . But the is necessary, since is not a theorem of , despite the fact that if then (and hence .
Two useful, easily proved facts about are:
- , , and are all provably equivalent.
- and are provably equivalent.
- (b) If , then .
Proof: We’ll prove (a) by induction on . Note that (b) then follows from (a), because if , then by Necessitation, hence by (a) and Modus Ponens. (Although (b) could be proved directly by a similar induction, which we would do if we didn’t need the stronger (a) for Lemmas 4 and 5.)
In the base case for (a) where is , , or for ,
trivially, and actually without requiring the part of (here the consequent is , , or respectively). The first inductive case, when is for some formulas , is also easy.
In the case where is , we assume inductively that
so by Necessitation and distribution
The distributes correctly over both and such that the consequent implies , i.e. implies .
By one of our useful facts about above, the in the hypothesis can be replaced with without changing its meaning; then we can strengthen the hypothesis by changing to . Putting these two observations together,
The fixed point theorem is also proved by an induction on complexity, though it takes a different form. As one should expect, most of the difficulty is in handling the ‘s.
Lemma 4 below treats this case, constructing fixed points for formulas of the form . Before giving its proof, we show that it’s a relatively straight path from there to the existence clause of the full fixed point theorem. Uniqueness is proved in Lemma 5.
- Note that if is modalized in , then can be decomposed as for some formulas , only containing variables from , and with not containing . The decomposition is not unique: if you construct it by induction on , you will have opportunities (namely at the step) to simplify the decomposition (namely by combining like terms; more complex simplification may be possible as well). As a trivial example, can be decomposed as either:
- , and , and (demonstrating no simplification), or
- and (demonstrating simplification).
- In the case when , i.e. when can be decomposed as , simply use the assumed lemma to produce a fixed point of ,
By Lemma 3 (b), it follows that is a fixed point of .
- For higher , it helps to consider systems for of formulas to be solved. That is, we wish to produce formulas with
for , under the constraint that none of appear in and any other variable in is also present in .
- It is proved by induction on that such systems can be solved; the base case is Lemma 4. Suppose size systems can be solved, and fix a size system of and . Solve the smaller system for just , producing formulas for with
Then find a fixed point for by Lemma 4, and “backsolve”: solves the original size system.
- The fixed point theorem falls out: given , let be a solution to the system , and let . Then applications of Lemma 3 (b) show that is a fixed point of .
- It may be of interest to solve systems of equivalences for general formulas modalized in each . This is in particular the application needed in the LaVictoire et al paper discussed in the previous post. The argument two bullet points above uses the special case of the fixed point theorem (aka Lemma 4) to solve such systems when each also begins with a ; with the general fixed point theorem established, one solves arbitrary modalized systems by a completely analogous procedure.
So to construct fixed points, we just need to prove Lemma 4. It’s actually not that hard.
Proof: Observe for any formulas and that if , then by introduction of another (by Necessitation and distribution) and the fact that , we also have
Apply this observation to the tautology
Rearrange the above:
then introduce another , and use formal Löb’s theorem for :
In particular, if and , then substituting for above will give .
Proof: Decompose as . By Lemma 3 (a),
for . Use the same trick as at the end of the proof of Lemma 3: introduce a , distribute, and note that can be replaced with just to get
for . Introducing another gives
By the above two lines and , we have
Then applying Lemma 3 (a) times,
Note: this is where it is critical that is modalized in . If we hadn’t gone through the above, we’d only have , with the stronger hypothesis. In fact, for the non-modalized formula , (3) is clearly false, or else we’d have by Löb’s rule.
Now by some propositional rearrangements of (3) (which wouldn’t be possible with in the hypothesis), we have
Introduce and distribute another to apply the Löb axiom to the consequent, getting
Combining the last two lines,
the proof is completed by noting that distributes over just as does.
4. Kripke Semantics
Models for Gödel-Löb are described by the Kripke semantics, a formalization of the old (probably confused) notion of “possible worlds”. The benefit of studying the Kripke semantics is that there is a class of finite models such that a formula is proved in if and only if every model in the class satisfies . This shows that the theorems of are a computable set: a two-threaded program enumerating both proofs and finite models can decide in finite time whether or not is a theorem.
Actually, the proof gives a bit more: for a given formula , one can derive a primitive recursive upper bound (in the length of ) on the size of the smallest model not satisfying . Thus the theorems of are actually primitive recursive.
In this section we present the Kripke semantics only as they are relevant to ; in other modal logics, other types of relations will be more appropriate than partial orders.
- A finite Kripke model for is a tuple . Here is a non-empty finite set “of worlds”, and is a (strict) partial ordering (it is irreflexive and transitive). Also, is an arbitrary “satisfaction” relation from to propositional variables.
- Then is extended to all formulas with
- iff or
- iff (the only interesting one).
All the derived connectives then behave as expected, e.g. iff .
- Because of the superficial similarity with the forcing relation from set theory, some texts use the forcing symbol instead of . But unlike set theoretic forcing, it is not generally the case if and , then ! Note, though, by transitivity of , that this does hold if is of the form .
- Further note that minimal worlds (with nothing than them) satisfy for every , and in particular satisfy . This is partially “corrected” as you move up the ordering: non-minimal worlds do not satisfy , and so satisfy instead. More generally, a world at height (where we say minimal worlds have height , and non-minimal worlds have height plus the maximum height of all lesser worlds) satisfies (and lower powers) and (and higher powers). Thus ancestors satisfy strictly fewer statements starting with than do their descendants.
- We also say a model satisfies , also written , to mean that every satisfies . Note that does not imply , but only that there is some with .1
That the family of finite Kripke models is sufficient to capture all syntactic behavior of is the content of the modal soundness and completeness theorems.
Modal completeness is proved in the contrapositive by constructing models for arbitrary non-theorems.
It’s worth pointing out that finite trees are still complete for . By a tree, we mean a (strict) partial order such that for every node , the set of is linearly ordered by . This strengthening is established by outlining a simple procedure for “straightening out” an arbitrary finite partial order, so that the modal completeness theorem for trees will follow easily from the modal completeness theorem as it is stated above (modal soundness is unaffected).
Boolos does this as follows:
- Given a finite Kripke model , let be the set of all non-empty decreasing sequences in , so is still finite.
- Order by reverse end-extension, e.g. and so forth. This order clearly satisfies the tree property.
- Define a satisfaction relation on by if and only if the smallest world in the sequence in the original model .
- This makes into a model which satisfies exactly the same formulas as .
Note that we don’t require a tree to have a maximum “root” node, so it might be more accurate to call our trees forests, consisting of several independent trees. Of course, if the modal completeness theorem can construct a forest-shaped model not satisfying a certain formula , then there’s a single-rooted tree within that forest which (is itself a Kripke model and) also doesn’t satisfy , so modal completeness still holds for the family of trees with a maximum node.
We conclude the section with proofs of modal soundness and completeness.
Proof of modal soundness: Propositional tautologies and the distribution schema are all “obviously” satisfied in all models, and Modus Ponens preserves satisfaction. Necessitation also preserves satisfaction in a model: if every satisfies , then in particular every does, so every satisfies .
Then we just need to show that the Löb axiom is satisfied in every model, which is a bit more interesting. Suppose . That is, suppose
which can be expanded again to
The conclusion we wish to derive is expanded as
so the Löb axiom can be read as an induction principle for the satisfaction relation. There are no infinite descending chains in a finite model (transitivity plus irreflexivity forbids cycles), so the induction principle holds, and the Löb axiom is satisfied.
Before moving on to modal completeness, we note that there’s one other kind of converse to the modal soundness theorem which may be worth pointing out. The definition of Kripke models can be stated perfectly well if is an arbitrary relation on an arbitrary (not necessarily finite) set . As mentioned, other types of are more appropriate to other modal logics. But it turns out that the only kind of ‘s which will satisfy a modal soundness theorem for are the well-founded strict partial orders. (And it should be clear that the proof of the modal soundness theorem goes through just fine when is merely well-founded, instead of finite.)
Proof of modal completeness: If a formula is not proved in , we need to construct a Kripke model with .
Worlds in the model we construct will be sets of modal formulas. The idea is that for each in a finite Kripke model, the relation picks out the set of formulas that hold at . When constructing our model, we’ll want fine control over which formulas are satisfied where, so we’ll construct in terms of . Actually, what we’ll have is (almost) , and we’ll do this in a way such that set membership (as in, ) will define a valid satisfaction relation (). To guide our construction, here are some properties that ‘s have in finite models:
- is consistent in that doesn’t refute any finite conjunction of formulas in .
- is complete, in that for every , either or is in .
- If and , then both and belong to . Actually contains strictly more formulas of the form than does , by the earlier observation about heights.
Then the basic idea is that for any formula not proved by , the singleton is consistent, and can be extended to a complete consistent set . If we do everything correctly so that defines a valid satisfaction relation, then .
But since we want to construct a finite model, we can’t just take to be the set of consistent, complete sets of formulas. Rather, we want to be the set of “consistent, complete sets of formulas relative to the subformulas of “. (Subformulas are defined in the obvious way: is a subformula of , of , of , and of , and “is a subformula of” is a transitive relation.)
So with reference to the list of properties above, let be the set of all sets of subformulas of and negations of subformulas of such that is consistent (the conjunction is not disproved by ) and -complete (for any subformula of , either or lies in ). Then say iff both
- For every in , both and belong to ;
- There is a subformula of which belongs to but not .
The relation is transitive by (1) and irreflexive by (2), and still contains an extension of .
Finally, we want to use set membership to define a satisfaction relation. Namely for , and each propositional variable , put iff (in particular, if does not appear in , though this choice is not essential). Extend to more complex formulas as required in the definition of the Kripke models.
We need to be compatible with set membership (for subformulas of and their negations). This is proved by induction on the complexity of formulas, and the only non-trivial step is dealing with , so it’s the only one we’ll treat. Specifically, we need to show that a subformula of belongs to if and only if for all , belongs to . The relation defined above clearly satisfies the left-to-right implication.
Conversely, suppose does not belong to ; we need to construct with in .
We construct such by extending the following set to an element of . This will be possible assuming is consistent, and the definition of will guarantee . Here consists of:
- All and all , for in
- (to get , we just need some not in , but is the obvious choice here).
Thus the last thing we need to prove is that is consistent, so suppose towards contradiction that it isn’t. Let enumerate those sentences with , so that the inconsistency of implies
where is the abbreviation from Section 3.
The consequent above is almost ready for Löb’s theorem; use the familiar trick of introducing a and distributing it over the . This also distributes over the conjunction, and recall that reduces to . Then using Löb’s theorem on the consequent,
Since every is in , this shows that cannot belong to consistent . Since is actually a subformula of , it follows that belongs to by -completeness. But does not belong to , so must actually be consistent, and the construction goes through.
- This definition follows Boolos’ text. Lindström’s article requires models to have a maximum “root” world, and says a model satisfies iff the root does. Then in Lindström’s version, and are equivalent. However, it seems to me that Lindström’s models fail the Necessitation axiom, as satisfaction at the root does not imply satisfaction at lower worlds, except for formulas starting with .