Why isn't 4 a theorem of K? and Can I use Show boxes in modal logic?

Question

In my basic logic course if I want to prove A ⊃ B then I would do the following:

1 Show A ⊃ B

2 A Assumption for Conditional derivation.

3 Stuff.....

4 Show B

5 More stuff....

6 B [or some contradiction]

Then because B [ or some contradiction] appeared in line 6 then this closes a box around lines 5 and 6, then I can cross out the word "Show" in line 4 and I get to now use B in the general part of my proof. But because B is now available then I have proven A ⊃ B and can box lines 2 through 6 and cross out "Show" on line 1.

---

In modal logic, we have the Rule of Necessitation (N): If A is a theorem, so is □A.

So I'm quite surprised that 4 is an axiom that needs to be added. S4 is the system based off of K plus the addition axioms T and 4. But if I can do proofs in modal logic like I did them in ordinary logic, then why isn't it immediate that 4 is a theorem?

"Proof"

1 Show □A ⊃ □□A

2 □ A assumption for Conditional Derivation

3 □(□A). by N

Yeah, obviously this isn't cool. I can construct a frame that proves 4 isn't a theorem of T. Let 1,2,3 be three different worlds such that 1R1, 2R2, 3R3, 1R2, and 2R3 with A true at 1 and 2 and false at 3. Then □A is true at 1 and false at 2, therefore □□A is false at 1 (hence 4 could not be a theorem for if it were then because □A is true at 1, Modus Ponens would give us □□A true at 1 but it's also false, a contradiction).

---

So I realize that 4 needs to be an axiom, but I just don't understand why the Show boxes don't carry over to Modal logic, or do they need to be modified in some way?

Answer 1

Yes, you can use show boxes in Modal Logic Proofs. It also helps when you use Indirect Derivation (aka Reductio Ad absurdum) proofs for innermost nested show box.

---

In the show box method of proof, as I remember learning it, each nested Show statement is a possible world, a frame, within the scope of the World outside of it.

1) Show □A->□□A Line 7, Direct Derivation

2) □A Assume Conditional Derivation

3) A By Line 2, (T)

5) Show A->□A Line 6, direct derivation

6) □A Line 2

7) □A->□□A By Line 5, (K)

Line 5 expresses a frame relationship between 1R2.

---

I believe your confusion stems from the fact that The Rule of Necessitation is not an inference rule for use in derivations but a rule concerning the treatment of theorems.

The most interesting and powerful result of the weak system (K) is this:

The Distribution Axiom: □(A→B) → (□A→□B).

In (T), If something is Necessary, then it is actual, so: □P -> P . It is the case that if something is actual, then it follows in a world consequent to it though, which is what this implies.

BUT! If a formula is a THEOREM,then per Zeman: "We use the terms 'thesis' and 'theorem' interchangeably here; either refers to a formula deducible from the null set of hypotheses, that is, to a formula provable within the system in question."

This allows us to import the theorems' truth values from antecedent worlds into those worlds that follow from them--which makes perfect sense when you reflect on it.

---