0

The semantic version of the deduction theorem says that $\{A_{1}, …, A_{n}\}\vDash$ B $\iff \vDash A_{1}, …, A_{n} \to$ B. I read that the deduction theorem does not hold in modal logic, but upon looking deeper they always only seem to talk about the syntactic version ($\vdash$) of the deduction theorem.

So does the semantic deduction theorem hold in Modal Logic?

God
  • 95
  • This kind of thing depends very sensitively on the details of how things are defined (both on the semantic and syntactic side) and I wouldn't say categorically that the deduction theorem fails on the syntactic side, but rather 'it's complicated'. So, how are you defining ${A_1,\ldots, A_n}\models_K B$, precisely? – spaceisdarkgreen Nov 16 '23 at 03:10
  • 1
    On the syntactic side: The usual reason people say the deduction theorem doesn't hold is because there is the necessitation rule (from $A$, $\square A$ follows) but clearly, $A\to \square A$ is not valid. But if you restrict the necessitation rule to require somehow that $A$ has been unconditionally proven, then you can recover the deduction theorem. – spaceisdarkgreen Nov 16 '23 at 03:14
  • @spaceisdarkgreen I define it as follows (informally spoken): If A1, …, An are true then so is B in any interpretation of a K model. I just feel that the semantic deduction theorem must be true, it is so intuitive, and I mean I kind of prove it, dont I? If not, maybe someone can give a concrete counterexample. I am sick and tired to prove some A $\vDash$ B and then to need to prove again $\vDash$ A $\to$ B (for some model like K or S4 or S5) with almost the exact wording. – God Nov 16 '23 at 06:28
  • That's not a precise definition at all. Likewise your proof doesn't show much of anything: you just keep saying 'true' and 'false' as if this is classical logic and there's only one notion. Here's a counterexample: If $A \models_K B$ means that for any Kripke frame where $A$ is true at all worlds, $B$ is true at all worlds (i.e. global consequence), then $A\models_K \square A.$ Whereas you can throw a dart and hit a countermodel to $\models_K A\to \square A.$ On the other hand, it clearly holds if $A\models B$ is local consequence (in any frame if $A$ is true at some world, so is $B$). – spaceisdarkgreen Nov 16 '23 at 06:44
  • A $\vDash_{K}$ B is shorthand for: A in $w_{i}$ $\vDash_{K}$ B in $w_{i}$. So a statement in modal logic can always only be true relative to a certain world afaik. Is that what you mean with local consequence? Do you think the semantic deduction theorem is true there and maybe you can show me how to prove it. – God Nov 16 '23 at 08:31
  • I just added the „local consequence“ to my question to make it more precise. – God Nov 16 '23 at 08:57
  • See Raul Hakli & Sara Negri, Does the deduction theorem fail for modal logic (2010) and see this post. – Mauro ALLEGRANZA Nov 16 '23 at 14:01
  • @MauroALLEGRANZA Your post is about syntactic deduction theorem. I wanna know about the semantic one. Can I at least take away in a nutshell that what I have written is not correct and the semantic deduction theorem holds not that easy than I think? – God Nov 16 '23 at 16:24
  • Things a similar: we cannot have both unrestricted Nec rule and unrestricted DT, otherwise we can have $\vdash P \to \square P$, which is not valid, that means that the proof system is not sound. – Mauro ALLEGRANZA Nov 16 '23 at 18:31
  • Simarly, we cannot validate the semantical statement: "if $P \vDash \square P$, then $P \to \square P$ is valid". – Mauro ALLEGRANZA Nov 16 '23 at 18:34
  • @God I still don’t know if I follow what your conventions are, and I think the overall situation is more complicated than you think. But the local version of the semantic “deduction theorem” is just a reiteration of the reasoning for classical logic, so may well be as easy as you think. Keep in mind it’s not really “fair” since the version of deductive consequence for which the deduction theorem fails is designed to align with global semantic consequence, not local. – spaceisdarkgreen Nov 16 '23 at 18:34
  • See the paper linked above and into my post for all details. – Mauro ALLEGRANZA Nov 16 '23 at 18:35
  • @God (My personal preference is to emphasize local consequence and restrict the necessitation rule as in my second comment, in which case we have alignment and the deduction theorem holds for both syntax and semantics.) – spaceisdarkgreen Nov 16 '23 at 18:44
  • Whenever someone mentions NEC rule it is confusing Semantics with Syntax. Here we shall only talk within the realm of $\vDash$. The counterexample would be to give me any model where P $\vDash$ Q holds but not $\vDash$ P $\to$ Q. That’s the interesting part of the semantic deduction theorem. Since P $\vDash \square$P is simply false for you can easily construct some model where P is true in w1, but not in w2, and only w1Rw2, it cannot be such an example. – God Nov 17 '23 at 04:15
  • See Hakli & Negri linked above: Conclusions. "The problem can be understood semantically through the distinction between validity inference and truth inference.We find that inference should be understood as truth inference, as this notion is the one used in proving a completeness theorem for labelled systems of modal logic. It also corresponds to our intuitive notion of valid reasoning: It is generally thought that the distinctive property of deductive reasoning—as opposed to inductive or abductive reasoning—is that deductive reasoning is truth-preserving: ... 1/2 – Mauro ALLEGRANZA Nov 17 '23 at 08:20
  • If the premisses are true, the conclusion should be true as well. However, the unrestricted rule of necessitation is not truth-preserving, it is only validity-preserving." 2/2 – Mauro ALLEGRANZA Nov 17 '23 at 08:20

1 Answers1

0

I am able to answer my own question. First I found a YT-video where a professor of philosophy specifically talks about the semantic version of the deduction theorem, proving it for propositional logic and then confirms that it also holds for Modal Logic (of course just relative to a model and a certain world $w_{i}$, so for instance for a T-model it would look like this: $V(w_{i})\{A_{1}, …, A_{n}\}\vDash_{T}$ $V(w_{i})$B $\iff \vDash_{T} V(w_{i})$$(A_{1}, …, A_{n} \to$ B). Here is the link: https://www.youtube.com/watch?v=WuLCL2q8Lx4

I even asked him specifically in the comment section, so here is what he wrote:

Me: So the semantic deduction theorem, i.e. {A1, …, An} |= B iff |= A1, …, An -> B, does also hold in Modal Logic (of course not globally but just for a particular model)?

Him: Yes, it holds in modal logic, because propositional logic holds at each world. So anywhere where the premises are true, their conjunction is also true, and if B follows, then any world will support the corresponding material implication.

Here is a more formal proof from someone with more knowledge than mine that looks spot on:

$\begin{aligned}(\Gamma\cup\{A\}\models B) &\iff \forall M\colon\forall w\in W(M)\colon (M,w\models\Gamma\cup\{A\})\to (M,w\models B)\\ &\iff \forall M\colon\forall w\in W(M)\colon (M,w\models\Gamma)\land (M,w\models A)\to (M,w\models B)\\ &\iff \forall M\colon\forall w\in W(M)\colon (M,w\models\Gamma)\to ((M,w\models A)\to (M,w\models B))\\ &\iff \forall M\colon\forall w\in W(M)\colon (M,w\models\Gamma)\to (M,w\models A\to B)\\ &\iff (\Gamma\models A\to B)\end{aligned}$

All what I wrote refers to the notion of the local semantic consequence where we look at a certain world to check if there is a semantic consequence in this certain world. In a notion of a global semantic consequence the semantic deduction theorem might not hold, that is another topic.

Feel free to add things I missed or might be of educational value.

God
  • 95