# Can natural deduction be incorporated into SQML?

EDIT - From the SEP

3.4 Propositional Modal Logic (S5)

(1) □(φ → ψ)→ (□φ → □ψ)

(2) □φ → φ

(3) ◇φ → □◇φ

Rule of Necessitation (RN): □φ follows from φ

(3) is precisely what I have in my demonstration, yet I've been corrected.

If φ is possible then by substitution a contradiction is possible, that is, ◇P ∧ ~P. But all tautologies are necessary, so □~(P ∧ ~P), which is equivalent to ~◇P ∧ ~P. Now by conjunction ◇X ∧ ~◇X. Now by explosion □◇φ is true. So if ◇φ then ◇X ∧ ~◇X, and if ◇X ∧ ~◇X, then □◇φ. Now by hypothetical syllogism

◇φ → □◇φ, which is (3).

Thus (3) seems intuitively true. And you don't need to memorize it as an axiom, since it's immediately derivable using NEC, as the first three lines of my demonstration show.

Also, I was told RN (i.e. NEC) is not a rule of inference. Now I'm confused...help.

I was considering S5, of SQML.

◊☐φ → ☐φ

You can prove it using natural deduction.

`````` 1. ◊P                 [OSC1]
2. ☐◊P                [1;NEC]
3. ◊P→☐◊P            [1-2;CSC1]
4. ~☐~P→☐~☐~P       [3;Df]
5. ~☐~P→~~☐~☐~P     [4;DN]
6. ~☐~P→~◊☐~P        [5;Df]
7. ◊☐~P→☐~P          [6;trans]
8. ◊☐Q→☐Q           [7;Df]
``````

So my question is can natural deduction be incorporated into SQML? If it can, then you can prove S5, thereby reducing the axioms by one.

Also, does the deduction theorem hold in SQML, and if not, why not?

• SQML is just S5+FOL, so I don’t know what you mean. The same issues surrounding the deduction theorem in both Modal Logic and First-Order Logic are present. If you don’t use the Generalization Rule, then you just have to worry about Necessitation. Basically, you can do Universal Intro when the name you’re operating on does not occur in any assumptions, while Necessitation may only be done on formulas derived from strict sub-proofs. Commented May 27 at 0:29

You can't use the necessitation rule like that. It is a rule of proof rather than a rule of inference, so it is better written as:

``````   ⊢ P
------   NEC
⊢ □P
``````

A rule of inference would look like the following, where Γ is an arbitrary set of sentences, (and it would be incorrect):

``````  Γ ⊢ P
-------   (incorrect)
Γ ⊢ □P
``````

Your line 1 is not a theorem of any normal modal logic, so you cannot use it to derive 2. In fact, if ◇P were an axiom, then it would entail ◇⊥ as a special case, and this is ruled out by NEC, since we have ⊢ ¬⊥ as a theorem of the underlying logic, and hence by NEC we get ⊢ □¬⊥ which is equivalent to ⊢ ¬◇⊥.

You may use natural deduction rules with modal logic, rather than using Hilbert style axioms. You may also use the sequent calculus. In any event, axiom 5 is not derivable from the other axioms.

As to the question of whether the deduction theorem holds in modal logic, there has been some debate on the subject. See, for example, Raul Hakli and Sara Negri, "Does the deduction theorem fail for modal logic?" Synthese 187 (3), pp. 849-867 (2012). Hakli and Negri's view is that the deduction theorem does hold provided we understand logical consequence in the conventional manner as truth preserving. The apparent problems with the deduction theorem arise because Hilbert systems are often understood as being validity preserving rather than truth preserving.

The necessitation rule does not say that □φ follows from φ. It says that if φ is a theorem of the modal logic then so is □φ. That is why I stated the rule the way I did above. There is an important difference between saying that □φ follows from φ and saying that ⊢ □φ follows from ⊢ φ.

It is important to distinguish between sentences that are logically contingent and those that are theorems of the logic. If ◇φ is a theorem of the logic then we can substitute any sentence for φ and it will be a theorem. This will include ◇⊥ and, as I showed above, any logic that includes ◇⊥ as a theorem is not consistent with the necessitation rule. On the other hand, if ◇φ is a logically contingent sentence then it does not entail ◇⊥ but it also means you cannot infer □◇φ from it.

As to the issue of a what constitutes a rule of inference... It is not uncommon to distinguish a rule of inference from a rule of proof. A rule of inference holds for logically contingent sentences as well as theorems; a rule of proof holds for theorems of the logic only.

In effect it is the same as the distinction between a derivable rule and an admissible rule. Suppose you have a rule

``````   Γ
---
B
``````

where Γ is a set of sentences and B is a sentence. In proof-theoretic terms, the rule is derivable if Γ ⊢ B. The rule is admissible if for every instance of the rule, B is a theorem whenever all the sentences in Γ are theorems. In model-theoretic terms, a rule is derivable if for any interpretation under which all the sentences in Γ are true, B is also true under that interpretation. A rule is admissible if, whenever each sentence in Γ is true under all interpretations, B is also true under all interpretations. In crude terms, derivable rules preserve truth; admissible rules preserve theoremhood or validity. All derivable rules are admissible, but not all admissible rules are derivable in general.

• how does ◇P entail ◇⊥ as a special case? Can you prove that explicitly. The thing is, I've never used the ⊥ symbol in any of my proofs, so I don't understand it. I know it means false, but false isn't a statement, so I just don't get it. Commented May 27 at 7:23
• If ◇P is a theorem, then by substitution any sentence can be put in place of P, including A ∧ ¬A, or ⊥ itself. ⊥ can be understood in slightly different ways: as a proposition that is a logical falsehood, as a zero-place connective that always returns the value false, as a placeholder that says in effect "insert your favourite contradiction here", or as a dead end in a proof process. Commented May 27 at 9:35