# Theorems of GL in modal logic

So I've been reading George Boolos' "The Logic of Provability" and he's explaining different systems of modal logic. He's taken as his basic symbols → (implication), □ (necessity), ⊥ (falsehood), a countable infinity of sentence letters (p, q, ...), and a countable infinity of sentence variables (A, B, ...). Negation ¬ is defined as ¬A = (A → ⊥), truth is defined as ⊤ = ¬⊥, possibility is defined as ◇ = ¬□¬. From ¬ and → we know that all other logical operators can be derived.

Then, a realisation * of a modal system is basically a way to write in arithmetic the sentences of modal logic. So, for example, if we wanted to take □ to mean "provability" (as we eventually will in this book), then A* is defined recursively as:

• p* = p, for all sentence letters p;
• ⊥* = ⊥;
• (B → C)* = (B* → C*), for all sentences B and C;
• □(B)* = Bew('B*'), for all sentences B, as per Gödel Incompleteness.

Then he talks about a few modal logic systems, including one called GL (for Gödel-Löb) and one called S5 (no idea what that stands for). All modal logic systems have all tautologies as axioms, all sentences of the form (□(A → B) → (□A → □B)) as axioms (those are called the distribution axioms), and the rules of inference are modus ponens and necessitation (that is, from A, infer □A). GL has the axiom (□(□A → A) → □A) for all sentences A in addition to those others; S5 doesn't, but it has (□A → A) instead.

Then he wants to demonstrate that (□(□p → p) → □p) is not a theorem of S5 and that (□p → p) is not a theorem of GL thusly:

We shall now show that □p → p is not a theorem of GL and that GL is consistent: Define A* by ⊥* = ⊥, p* = p (for all sentence letters p), (A→ B)* = (A* → B*), and □(A)* = ⊤. (Then A* is the result of taking □ to be the verum operator in A.) If A is a tautology, so is A*; if A is a distribution axiom, then A* is ⊤ → (⊤ →⊤); and if A is a sentence □(□B → B) → □B, then A* = ⊤ → ⊤. Moreover, if A* and (A → B)* are tautologies, so is B*, and if A* is a tautology, then so is □(A)* = ⊤. Thus if A is a theorem of GL, A* is a tautology. But (□p → p)* = (⊤ → p), which is not a tautology. Thus, □p → p is not a theorem of GL (...).

Then to prove the other thing for S5 he uses similar reasoning, but using the realisation that □(A)* = A*. Except...

...what???? I don't get it! He says "if A* is a tautology, then so is □(A)* = ⊤", but the way he's defined , even if A is false, it is still the case that □(A) = ⊤, so even if A is not a theorem of GL, it can still be a tautology! How does that prove anything at all?

The idea of an independence proof (in general) is :

• (i) define a "sort of" interpretation (in this case : $*$) for formulae, starting from atomic ones : $\bot, p, \ldots$

• (ii) show that all axioms have a certain "property" : in this case, are tautologies, i.e. they are equivalent to $\top$

• (iii) show that the rules of inference preserve that "property" : i.e. if $A^*$ is a tautology, then also $\square (A)^*$ is.

Finally :

• (iv) show that the "property" does not hold for the formula we want to prove to be un-derivable in the system.

Thus, the formula $(\square p \rightarrow p)$ under this "interpretation" becomes : $(\square p \rightarrow p)^* = \square (p)^* \rightarrow p^* = \top \rightarrow p$, by the "rules for translation" of $*$, and we have that : $\top \rightarrow p$ is not a tautology.

Thus, the formula lacks the "property" in question and so it is not "producible" in the system : thus, is not a theorem of it.

He says "if $A^*$ is a tautology, then so is $\square(A)^* = \top$", but the way he's defined , even if $A$ is false, it is still the case that $\square(A)^* = \top$, so even if $A$ is not a theorem of GL, it can still be a tautology!

it is not so : if $A$ is an axiom it is a tautology, and so is $A^*$.

About the necessitation rule, it "produces" valid formulae from already proved ones. Thus, if I have proved $A$, $A$ is a theorem.

Recall that, in GL, $\square$ is $Bew$, that means "provable".

Thus, if $A$ is a tehorem I've already proved it and so I'm licensed to assert $\square A$ i.e. $Bew(A)$.

About S5, it is a "well-known" system of Modal Logic.

• He hasn't established that in GL, ◻ is Bew yet, though. He has just defined GL as "all tautologies + distribution axioms + modus ponens + necessitation + Löb's theorem", no mention of Bew at all, as a sytem of modal logic that makes no reference to arithmetic. Furthermore, "if A is an axiom it is a tautology, and so is A∗"; fine, but even if A is not an axiom, ◻(A)* is a tautology by definition. * preserves tautologies, but it also creates them where there were none. Also, if you apply that realisation to S5, does that not make □p → p also not a theorem of that realisation?
– Red
Commented Dec 2, 2014 at 10:39
• @PedroCarvalho - "even if $A$ is not an axiom, $\square(A)^*$ is a tautology by definition. $*$ preserves tautologies, but it also creates them where there were none." NO: you apply rules of inference starting from axioms to produce theorems; thus, if you have derived $A$, it is a theorem and so a "correct" tautology, under the $*$ interpretation. So you apply necessitatio rule and you produce a new tautology. The $Bew$ "explanation" (you are right) is an analogy with the modal case: why we agree on the necessitation rule ? 1/2 Commented Dec 2, 2014 at 10:44
• Because if I have derived $A$ from axioms (i.e. $A$ is a theorem) it is a "logical truth"; thus, it is "necessarily true" and so I'm licensed to derive $\square A$ from $A$. 2/2 Commented Dec 2, 2014 at 10:45
• What you say doesn't contradict what I said, though, at least I don't think so? As far as I understand, * is supposed to be a way to write any sentence at all in the language of arithmetic. So, for example, ◻(⊥)* = ⊤ because ◻(A)* = ⊤ no matter the contents of A. So with * I've just created a new tautology (namely, ◻(⊥)*) where there previously was none. Furthermore, this still doesn't explain why I couldn't use this same * to prove that □p → p is not a theorem of S5.
– Red
Commented Dec 2, 2014 at 10:51
• Right, but we don't need to derive it for it to become a tautology in the language of arithmetic under *. However, I think I understand. Even though it may produce new tautologies, * preserves all existing ones, and it leaves some sentences as non-tautologies, therefore all sentences that aren't tautologies under * are necessarily not theorems, even if there are some tautologies under * that aren't theorems.
– Red
Commented Dec 2, 2014 at 11:00