The following comes from Blackburn's text on Modal Logic:
Remark 1.41 Warning: there is a pitfall that is very easy to fall into if you are used to working with natural deduction systems: we cannot freely make and discharge assumptions in the Hilbert system K. The following ‘proof’ shows what can go wrong if we do:
- $p$ (assumption)
- $\square p$ (generalisation: 1)
- $p\to\square p$ (discharge assumption)
So we have ‘proved’ $p\to\square p$! This is obviously wrong: this formula is not valid, hence it is not K-provable. And it should be clear where we have gone wrong: we cannot use assumptions as input to generalization, for, as we have already remarked, this rule does not preserve satisfiability. Generalization is there to enable us to generate new validities from old. It is not a local rule of inference.
I'm not able to understand what the problem really is! I know that $p\to\square p$ is not valid, so something is definitely wrong. Could someone please explain this in detail?
Which part is incorrect (of the three steps above)? I think it's okay to make the assumption $p$. The problem probably lies in the second part, but I'm not sure why we cannot use generalization/necessitation on assumptions (even though the author has explained it - I do not get it).
It'd be very helpful if someone could help me understand this better!