I came a cross two Hilbert proofs
In S4(first proof):
- $p \rightarrow K p$ (necessitation)
- $\neg K p \rightarrow K \neg Kp $ (substitution, 1)
In T(second proof):
- $q \rightarrow K q$ (necessitation)
- $ K p \rightarrow KKp $ (substitution, 1)
To me these two proof have some error inside them. The rules that I use are: The tautologies of first-order propositional logic as axioms, the axiom for modal distribution, the rule for modus ponens, the rule for necessitation, and the rule for substitution.
System T is system K plus the truth axiomsystem S4 is system T plus the axiom of positive introspection system S5 is system S4 plus the axiom of negative introspection
These proofs can't be correct right? Because in the first proof in S4 the second line derivation, is the A3 axiom which is not derivable in S4 and in the second prove the second line derivation, is the A2 axiom which is not derivable in T.
Could somebody indicate and explain the errors in these derivations?
(I think first that the necessity rule can be only allowed on something that is proved and can't be introduced by it's self. Then the substitution part I don't completely understand how this proof is constructed ,but in substitution you replace a formula for (maybe a more complex) formula, can somebody maybe explain how this is wrongly applied?)