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