I have a question about the necessitation rule in normal modal logics. Using an axiomatic system, once I proved $P$ I can apply necessitation and prove that $P$ is necessary ($\Box P$). In tableaux, once I prove $P$, I do not see how the rules allow me to infer $\Box P$.

What I mean essentially, is that tableaux only allows to prove formulas and does not capture, as far as I can see, the provability relation used in the necessitation rule. When you assume $P$ and try to prove $\Box P$ in tableaux, what you are essentially trying to prove is $P \to\Box P$, which is of course not provable.

Therefore, if $\Box P$ is inferred from the assumption $P$ in a normal modal logic but it cannot be proved in the corresponding tableaux system, how can the tableaux system be a complete procedure for the corresponding modal logic?

One example is the following, for the modal logic KD [1] p. 45. Assume the following set of assumptions:

  1. $\Box \neg q$
  2. $q \Rightarrow \Box p$
  3. $q$
  4. $p \Rightarrow q$

Which abstracts the gentle murder paradox of standard deontic logic.

You can infer $\Box q$ using the following steps:

  1. from (2) and (3) infer $\Box p$
  2. from (4) and the inheritance principle (based on the necessitation rule) infer $\Box p \Rightarrow \Box q$
  3. from (5) and (6) infer $\Box q$
  4. contradiction since $\Box q \wedge \Box\neg q$ is inferrable and contradicts deontic consistency

Now, I was wondering how to imitate this proof using a tableau system for KD (K would be enough here). For example (using unsigned prefix tableaux):

  1. a. $\Box \neg q$
  2. a. $q \Rightarrow \Box p$
  3. a. $q$
  4. a. $p \Rightarrow q$
  5. a. $\neg (\Box q)$ (negation of the goal)
  6. a. $\neg q$ | a. $\Box p$ (on 2)
  7. closed (6 and 3) | $\Box p$
  8. b. $\neg q$ (from 5 and working only on the right branch)
  9. b. $p$ (from 6)

Now, in order to close the proof, I would need to elevate (4) into $\Box p \Rightarrow \Box q$ but there is no such rule in talbeaux.

The result, as far as I can see, is that a theorem of KD cannot be proved in tableaux.

Thank you,

[1] Navarro, Pablo E., and Jorge L. Rodríguez. Deontic logic and legal systems. Cambridge University Press, 2014.

  • $\begingroup$ Question : the necessitation rule is : "if $\vdash \varphi$, then $\vdash \square \varphi$". How can you apply it to the assumption 4 ? $\endgroup$ – Mauro ALLEGRANZA Jun 27 '18 at 11:11
  • $\begingroup$ See Standard Deontic Logic : Rule (OB Nec) : "If $⊢ p$, then $⊢ \text {OB} p$". $\endgroup$ – Mauro ALLEGRANZA Jun 28 '18 at 7:38
  • $\begingroup$ And see your textbook, page 21 : the "necessitation rule (if $\vdash \alpha$, then $\vdash \text N \alpha$)." $\endgroup$ – Mauro ALLEGRANZA Jun 28 '18 at 7:43
  • $\begingroup$ IMO, your error is due to a sloppiness in the text: discussing the Good Samaritan Paradoxes (page 45) we read: "Here (7’) $p → q$ represents a stronger conditional (strict conditional) than the simple material conditional." The strict conditional is "a conditional governed by a modal operator. The formula $\Box (p \to q)$ says that $p$ strictly implies $q$." Unfortunately, the authors have used the same symbol : $\to$ of the so-called material conditional. $\endgroup$ – Mauro ALLEGRANZA Jun 28 '18 at 7:51
  • $\begingroup$ If so, we have that 4) above is $\Box (p \to q)$ and we may apply the modal axiom $(A_2)$ [page 21] to get : $\Box p \to \Box q$. $\endgroup$ – Mauro ALLEGRANZA Jun 28 '18 at 7:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.