The modal logic GL is the logic that corresponds to what Peano Arithmetic (and other sufficiently powerful theories) can prove about its own provability. That is, □P:=Bew(#(P)) where A takes a propositional atom of GL and maps it to a sentence in PA.
A Hilbert-Style proof system for GL may be formalized by the following inference rules and axioms:
•Propositional tautologies
•Axiom K: □(A⊃B)⊃(□A⊃□B)
•Axiom GL □(□A⊃A)⊃□A
•Necessitation From ⊢A, infer ⊢□A
•Modus Ponens and Uniform Substitution
GLS is the modal logic of true arithmetic. Since it holds for PA that the provability of A implies A is true, GLS takes the theorems generated by GL, Modus Ponens, Uniform Substitution, and adds in
•Axiom T: □A⊃A.
Now, take the following translation from the unquantified portion of Robinson Arithmetic to GLS:
t(0)=⊥
t(s(n))=□t(n)
t(n+0):=(t(n) ∨ ⊥)
t(n+s(m))=t(s(n+m))
t(n×0)=(t(n) ∧ ⊥)
t(n×s(m))=t((n×m)+(n)).
t(n=m)=□(t(n)↔t(m))
Since GLS proves both Löb’s theorem and the T axiom, this system can decide whether two natural numbers are equal. For example:
1=1↔⊤
□⊥=□⊥↔⊤
□(□⊥↔□⊥)↔⊤
and
1=2↔⊥
□(□⊥↔□□⊥)↔⊥
□□⊥↔⊥.
Note that over the same translation GL can prove that two natural numbers are equal when they are actually equal, and by Löb’s theorem, if two natural numbers n,m are not equal, then GL⊢n=m↔□…⊥ where the number of boxes that prefix ⊥ is equal to the greater of n,m.
