# Applying the necessitation rule in semantic tableaux

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  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,

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

• Question : the necessitation rule is : "if $\vdash \varphi$, then $\vdash \square \varphi$". How can you apply it to the assumption 4 ? – Mauro ALLEGRANZA Jun 27 '18 at 11:11
• See Standard Deontic Logic : Rule (OB Nec) : "If $⊢ p$, then $⊢ \text {OB} p$". – Mauro ALLEGRANZA Jun 28 '18 at 7:38
• And see your textbook, page 21 : the "necessitation rule (if $\vdash \alpha$, then $\vdash \text N \alpha$)." – Mauro ALLEGRANZA Jun 28 '18 at 7:43
• 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. – Mauro ALLEGRANZA Jun 28 '18 at 7:51
• 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$. – Mauro ALLEGRANZA Jun 28 '18 at 7:53