5

Are there natural deduction rules for the S5 modal operators that mirror the introduction and elimination rules for quantifiers in predicate logic? I recall seeing somewhere rules like the following:

Necessity introduction: if you have a strict sub-proof of A (with no hypothesis) then you can infer □A

Necessity elimination: □A implies A

Possibility introduction: A implies ◇A

Possibility elimination: if you have a strict sub-proof of B from hypothesis A, then from ◇A you can infer B

Where for necessity introduction and possibility elimination there are restrictions on the modal scope of A, B, and the statements that can be imported into the strict sub-proofs (like the restrictions on the appearance of the free variable in universal generalization and existential instantiation).

Intuitively, it seems like the rules should be:

Necessity introduction: if you have a strict sub-proof of A (with no hypothesis) then you can infer □A

Necessity elimination: □A implies A

Possibility introduction: A implies ◇A

Possibility "elimination": if you have a strict sub-proof of B from hypothesis A, then from ◇A you can infer ◇B (note the addition of the possibility operator to B)

Where the restriction is just that you can import necessary statements by removing an initial necessity operator. But this doesn't give S5. My question is whether a stronger version of the rules exists.

Improve this question

3 Answers 3

Reset to default
1

I worked out what I was looking for. The following rules of inference added to ones for classical propositional calculus give S5 modal logic:

Definition: an essentially modal statement is one of the form □A, ~□A, ◇A, or ~◇A.

Necessity introduction: if you have a strict sub-proof of A (with no hypothesis) then you can infer □A, where any previous statements you reassert into the strict sub-proof must be essentially modal.

Necessity elimination: □A implies A

Possibility introduction: A implies ◇A

Possibility elimination: if you have a strict sub-proof of B from hypothesis A, then from ◇A you can infer B, where both the conclusion B and any previous statements you reassert into the strict sub-proof must be essentially modal.

These rules of inference allow you to prove all the usual axioms for S5 as well as the dual relationships ◇A=~□~A and □A=~◇~A (so they don't have to be put in by hand, and possibility and necessity are treated as equally fundamental).

Edit: the definition of essentially modal statements can be expanded in the following way without changing the logic:

  • Any statement of the form □A or ◇A is essentially modal.
  • The negation of an essentially modal statement is essentially modal.
  • The conjunction, disjunction, implication, or equivalence between two essentially modal statements is essentially modal.
  • (For quantified S5 modal logic) The universal or existential quantification over an essentially modal statement is essentially modal.
Improve this answer
4
  • 1
    I'm not that up on modal logic but I'm confused about possibility elimination, are you saying that if we have □(A→B) (as would seem to be implied by a strict sub-proof of B from hypothesis A) along with ◇A, we can infer that B is true, without a □ or ◇ in front of it? (i.e. a proof that B is true in 'our' world) That doesn't seem right but I'm probably misunderstanding what you're saying.
    – Hypnosifl
    Commented May 27, 2021 at 16:36
  • Basically, if you have □(A→B) and ◇A, you can infer B, as long as B has one of the forms □C, ~□C, ◇C, or ~◇C for some C. Also, it is statements of those forms which can be imported into strict subproofs.
    – Matt Dickau
    Commented May 28, 2021 at 2:11
  • @MattDickau one can easily prove in K ⊢ □(A→B)→(◇A→◇B), so given □(A→B) and ◇A, even in K ⊢ ◇A→◇B, then ⊢ ◇B. So your last axiom is simply in your system ⊢ ◇B→B (or generically ⊢ ◇A→A). Regarding your 3rd axiom as I mentioned earlier it's derivable in reflexive T (your 2nd axiom) ⊢ A→◇A since it's accessible to itself, so seems it's unnecessary. Also I don't see how you can derive transitivity in your system ⊢ □A→□□A?
    – Double Knot
    Commented May 28, 2021 at 3:52
  • @DoubleKnot, strictly speaking, these are all deduction rules, not axioms. My last deduction rule does not allow ⊢ ◇B→B for arbitrary B. What it does allow is ⊢ ◇XB→XB where X is one of □, ~□, ◇, or ~◇. My third deduction rule is not derivable from the second one because I am treating ◇ as primitive, not defining it via ◇=~□~. And transitivity is easily derivable because the first deduction rule gives ⊢ XB→□XB for any of the operators X that I listed.
    – Matt Dickau
    Commented May 28, 2021 at 14:58
0

S5 := T + 5 and T := K + M, where axiom 5 := ◇p → □◇p, M (Reflexivity Axiom) := □p → p, and K is the simplest normal modal system which has Necessitation Rule N and Distribution Axiom K.

Based on above definition and axioms, regarding your "Necessity introduction", this is what Necessitation Rule in system K exactly does, that is p → □p which can be interpreted as if p is a theorem, then □p is likewise a theorem.

Regarding your "Necessity elimination", this is exactly the Reflexivity Axiom M defined above for S5.

Regarding your "Possibility introduction", this can be trivially proved by adding Brouwer's axiom B (p → □◇p) with above Reflexivity axiom M in S5.

Regarding your "Possibility elimination", in system K we can prove □(A→B) → (◇A→◇B) (you can see detailed derivation in a previous PSE question's comment here if interested), but if you really want (A→B) → (◇A→◇B), then it seems to be the only possibility is that the formula (A→B) is a tautological theorem then we can invoke the above Necessitation Rule N in system K, then we can arrive at (A→B) → □(A→B), then Modus Ponens, we can have (A→B) → (◇A→◇B).

Improve this answer
5
  • Thanks for the response; this doesn't answer my question however. Of course one can add whatever axioms are needed to get S5, e.g. <>[]A -> []A to the rules I gave in the second set (which I think is equivalent to T if I'm getting the terminology right). My question is whether there is a set of 4 rules, structurally similar to the generalization and instantiation rules for quantifiers, which give S5 all by themselves.
    – Matt Dickau
    Commented May 22, 2021 at 3:49
  • @MattDickau another S5 equivalent axiom systems is to change 5 to B+4, where B is the Brouwer's axiom, and 4 is □p → □□p. Either set is to restrict the accessibility relation R of the Kripke frame to be Euclidean. Hope this is helpful...
    – Double Knot
    Commented May 22, 2021 at 4:54
  • 1
    p → □p is not a theorem of S5. The N rule is that ⊢p ⇒ ⊢□p, where ⇒ is a meta-level implication.
    – Bumble
    Commented May 22, 2021 at 10:09
  • @Bumble thx for your comment above, yes by definition of normal modal logic it's required to be closed under N rule which is actually an inference schema, so strictly speaking it's a meta-level implication.
    – Double Knot
    Commented May 22, 2021 at 20:19
  • @MattDickau it's a well known proposition is modal logic, KM5=KMB4 = KDB4 = KDB5.
    – Double Knot
    Commented May 25, 2021 at 5:45
0

It is possible to express S5 using natural deduction style rules rather than axioms. However, it is a fair bit more complex than just a single introduction and elimination rule for box and diamond. There is an article here that sets out one approach:

https://projecteuclid.org/download/pdf_1/euclid.ndjfl/1093888133

An alternative is to use the sequent calculus, which can give a cut-free and decidable system. The following article describes how S5 can be represented using the sequent calculus.

A Cut-Free Simple Sequent Calculus for Modal Logic S5

Improve this answer
1
  • The second linked article is no longer available at that address. The reference for it is: Francesca Poggiolesi, A Cut-Free Simple Sequent Calculus for Modal Logic S5. Review of Symbolic Logic, Cambridge University Press, 2008, 1 (1), pp. 3-15.
    – Bumble
    Commented Aug 7 at 7:19

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .