Deduction theorem in modal logic

Question

I am looking for a semantic for deduction theorem in modal logic,I wanna find a semantic way to prove this theorem,but I wasn't successful.tnx for your help

Answer 1

You can see :

• Raul Hakli & Sara Negri, Does the deduction theorem fail for modal logic (2010), for a detailed discussion of the Deduction Th in modal logic.

See in particular page 6 for a discussion about an :

argument for the failure of the deduction theorem [...] based on Kripke semantics.

---

The "issue" with the proof of the Deduction Th for modal logic is the "interaction" with the Necessitation rule : NEC.

If we consider the following proof from premises :

1) $P$ --- premise

2) $\square P$ --- from 1) by NEC

we have a proof of $\square P$ from $P$, i.e. $P \vdash \square P$.

Thus, with an "unrestricted" Deduction Th we can derive the invalid :

$P \to \square P$.

See Sider's book suggested in Bruno's answer below, for the restrictions to be applied in order to prove the Deduction Th in some systems of modal logic.

Answer 2

For a more basic account of the subject you can refer to:

• Theodore Sider, Logic for Philosophy, Ch. 6, p. 178

The author provides simple proofs of soundness, completeness and the deduction theorem for a variety of modal systems.

However, the book does not cover strong soundness and strong completeness though, since the notion of proof from a set involves more complicated issues with the presence of the necessitation rule (see Mauro's answer above).