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 :
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.
About you doubt :
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)$.
You can see also Provability Logic.
About S5, it is a "well-known" system of Modal Logic.