Difficulty understanding the admissibility of a rule in logic

Question

I am trying to understand the concept of admissibility in logic. Wikipedia says a rule is admissible if adding it to a system does not result in new theoriems. It then gives $\frac{\square p}{p}$ as an admissible but not derivable rule in modal logic $K$. I understand that it's not derivable but how is it admissible? doesn't adding this rule lead to a new tautology $\square p \rightarrow p$?

Answer 1

Here is an example. Consider the classical Deduction Theorem, represented here by $p \vdash q \vDash p \to q$. The proof of this is a meta-proof, i.e. a proof that it outside of the logical system. Typically, it constructs a new proof from an existing proof. Replacement theorems are proven in the same manner.

So, the above is admissible in any logical system that has a proof for the Deduction Theorem. It does not increase the number of theorems, it simply makes some of those theorems easier.

The Deduction Theorem is not itself a theorem in the system, it is a theorem of the system. So, it cannot itself be derived in the system. But, every use of it, is in a theorem that can be derived in the system -- just not as conveniently.

So the Deduction Theorem is admissible, but not derivable.

Note that the Wikipedia example only leads to a rule if it contains the Deduction Theorem. But, in that case, the tautology must already be derivable in the system.

Answer 2

I am not actually sure about this, but it seems that our version of deduction theorem here fails in modal logic (formulated as Hilbert system), because proving this theorem in classical propositional logic (in Hilbert system) involves the inference rules substitution and modus ponens for induction (see the proof here, start reading at "Now let us assume the induction hypothesis..."). Now that we add a new rule, $\frac{\square p}{p}$, the proof doesn't work anymore. Hence, we cannot simply deduce $\square p \rightarrow p$.

I said "our version" above because this looks complicated, see "Hakli and Negri, Does the deduction theorem fail for modal logic?".