1

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

Mauro ALLEGRANZA
  • 94,169
fateme jl
  • 197

2 Answers2

2

You can see :

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.

Mauro ALLEGRANZA
  • 94,169
  • tnx,but I can't undrestand this sentence in page 6 "In more general terms, the above statement is actually asking more than the deduction theorem, as it hides an inference from admissibility to derivability." I wasn't able to find the reason of relation between this sentence and cut example. – fateme jl May 08 '15 at 13:45
  • @fatima - regarding admissibility vs derivability of rules, see this post. In classical logic the two concepts coincide; not so in other logics, like the intuitionistic logic or modal system. See there for references. – Mauro ALLEGRANZA May 09 '15 at 15:53
1

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

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).

Bruno Bentzen
  • 3,362