Characters and fixed-points in provability logic.
Zachary L. Gleit, Warren Goldfarb · Notre Dame Journal of Formal Logic · 1989
Some basic theorems about provability logic -the system of modal logic that reflects the behavior of formalized provability predicates in theories such as arithmetic -are given simplified, model-theoretic proofs.The theorems include the Fixed Point Theorem of de Jongh and Sambin, the Craig Interpolation Theorem, and the Beth Definability Theorem.Attention is also paid to the complexity of models for formulas in this logic.Provability logic is the modal logic whose axioms are the tautologies and all formulas of the forms D (A -> B) -> (ΏΛ -• ΏB) and D (ΏA -• A) -> Q4, and whose inference rules are modus ponens and necessitation.This system has been known variously as K4W, L, G, GL, and PRL; we adopt the next to last of these monikers, and use "h" for provability in GL.GL is of interest since it reflects the behavior of formalized provability predicates in such theories as Peano Arithmetic (for details see [1] or [3]).A formula A is said to be modalized in a sentence letter p iff every occurrence of p in A lies in the scope of a D. The Fixed Point Theorem, due to de Jongh and Sambin, states that if A is modalized in p then there exists a formula H containing only sentence letters of A aside from p such that hD (p++A)*+ D (p H).Via the connection of GL with provability in formal theories, this theorem implies that sentences in such formal theories constructed from formalized provability predicates by "self-referential" techniques are provably equivalent to sentences involving no self-reference.In Section 1, we give a purely model-theoretic proof of the Fixed Point Theorem, which we think to be more perspicuous than the extant proofs.The *We would like to thank George Boolos for much generous assistance and many helpful suggestions, and in particular for simplifying the counterexample found in the fourth paragraph of Section 3. We are also grateful to Lisa Reidhaar-Olson for catching several errors in the penultimate draft.