🚀 go-pugleaf

In article <1992Apr12.193331.11012@husc3.harvard.edu>, zeleny@zariski.harvard.edu (Mikhail Zeleny) writes:
[...]
> 
> Observe that Ralph says that S4 and S5 are *subsystems* of classical logic
> extended with the axiom: A iff \box A. In that, he is absolutely correct: a
> subsystem needn't contain the axiom in question, but only a deductively
> closed proper subset of its consequences, e.g. those generated by \box A
> \supset A in the presence of classical laws.  However, I am not sure
> whether he could do without an additional rule of inference, viz. the Rule
> of Necessitation:
> 
> 		A
> 	       ___
> 
> 	      \box A
> 
> which prima facie seems to be required for adequately characterizing S4 and
> S5, even if all of their theorems can probably be obtained by the above
> process.
> 
How, without the necessitation rule (and scheme K), can you get 

     p \supset \box (\box (p \supset q) \supset (\box p \supset \box q))

(which is a theorem of S4 and S5), without proving too much, e.g.

      p \supset \box p

(which is not a theorem of S4 and S5), where p is a propositional variable?

Greetings,

Marek Suchenek