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?


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?

1 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.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .