On the nonexistence of certain normal forms in the logic of provability

Extract

G is the system of propositional modal logic whose axioms are all tautologies and all sentences □(A → B) → (□A → □B) and □(□A → A) → □A and whose rules are modus ponens and necessitation. For the connections between G and provability in formal systems, see [3] and [2].

A letterless sentence is a modal sentence that contains no sentence letters at all. In [1] the author showed (in effect) the existence of simple normal forms in G for letterless sentences: every letterless sentence is equivalent in G to a truth-functional compound of sentences ⋄^r ⊤ (⋄⁰B = B; ⋄^r+1B = ⋄ ⋄^r+1 B. ⊤ is the 0-ary connective that is always evaluated as true; we assume that the language contains ⊤ as a primitive.)

A family of sets {H_n}_n∈ω of modal sentences that contain no sentence letters other than some fixed one (say p) was introduced by Solovay in [3]: H₀ = the set of sentences equivalent in G to one of p, −p, ⊤, and ⊥; H_n+x = the set of sentences equivalent in G to a truth-functional combination of sentences ⋄^rB, where r ∈ ω and B ∈ H_n. (This definition of the H_n's differs inessentially from the one given in [3].) Since r may = 0, H_n ⊆ H_n+1 and thus if m ≤ n, H_m ⊆ H_n; every modal sentence containing no letter other than p is in some H_n. It follows from the normal form theorem for letterless sentences that every letterless sentence is in H₁.

In [3] Solovay stated without proof a result about the sets H_n: for every n, H_n ⊊ H_n+1; equivalently, for every n, there is a sentence containing no letter other than p not in H_n. Thus the existence of a normal form for letterless sentences is a very special feature of these sentences, for Solovay's result shows that normal forms like those obtainable for letterless sentences are not to be found in general. He takes this result to be one reason for regarding the Lindenbaum algebra in G of sentences containing no letter other than p as much more complicated than that of letterless sentences.