Why is it OK to use deduction theorem, though? In standard modal logics like K and S5 the deduction theorem doesn’t hold (otherwise you could assume P, use necessitation to get []P, and then use deduction theorem to get P → []P as a theorem).
Well, the deduction theorem is a fact about PA (and, propositional logic), so it’s okay to use as long as ⊢means “PA can prove”.
But you’re right that it doesn’t mix seamlessly with the (outer) necessitation rule. Necessitation is a property of “⊢”, but not generally a property of “X⊢”. When PA can prove something, it can prove that it can prove it. By contrast, if PA+X can prove Y, that does mean that PA can prove that PA+X can prove Y (because PA alone can work through proofs in a Gödel encoding), but it doesn’t mean that PA+X can prove that PA can prove Y. This can be seen by example, by setting X=Y=¬□(1=0)”.
As for the case where you want ⊢ to refer to K or S5 instead of PA provability, those logics are still built on propositional logic, for which the deduction theorem does hold. So if you do the deduction only using propositional logic from theorems in ⊢ along with an additional assumption X, then the deduction theorem applies. In particular, inner necessitation and box distributivity are both theorems of ⊢ for every A and B you stick into them (rather than meta theorems about ⊢, which is what necessitation is). So the application of the deduction theorem here is still valid.
Still, the deduction theorem isn’t safe to just use willy nilly along with the (outer) necessitation rule, so I’ve just added a caveat about that:
Note that from X⊢A we cannot conclude X⊢□A, because □ still means “PA can prove”, and not “PA+X can prove”.
Why is it OK to use deduction theorem, though? In standard modal logics like K and S5 the deduction theorem doesn’t hold (otherwise you could assume P, use necessitation to get []P, and then use deduction theorem to get P → []P as a theorem).
Well, the deduction theorem is a fact about PA (and, propositional logic), so it’s okay to use as long as ⊢means “PA can prove”.
But you’re right that it doesn’t mix seamlessly with the (outer) necessitation rule. Necessitation is a property of “⊢”, but not generally a property of “X⊢”. When PA can prove something, it can prove that it can prove it. By contrast, if PA+X can prove Y, that does mean that PA can prove that PA+X can prove Y (because PA alone can work through proofs in a Gödel encoding), but it doesn’t mean that PA+X can prove that PA can prove Y. This can be seen by example, by setting X=Y=¬□(1=0)”.
As for the case where you want ⊢ to refer to K or S5 instead of PA provability, those logics are still built on propositional logic, for which the deduction theorem does hold. So if you do the deduction only using propositional logic from theorems in ⊢ along with an additional assumption X, then the deduction theorem applies. In particular, inner necessitation and box distributivity are both theorems of ⊢ for every A and B you stick into them (rather than meta theorems about ⊢, which is what necessitation is). So the application of the deduction theorem here is still valid.
Still, the deduction theorem isn’t safe to just use willy nilly along with the (outer) necessitation rule, so I’ve just added a caveat about that:
Thanks for calling this out.