S5LP - LP with S5 Modal

---

Semantics

S5LP semantics behave just like KLP semantics.

S5LP includes the access relation restrictions on models of S5:

Reflexivity

In every model, for each world \(w\), \(\langle\ w,w\ \rangle\) is in the access relation.

Transitivity

In every model, for each world \(w\), and each world \(w'\), for any world \(w''\) such that \(\langle\ w,w'\ \rangle\) and \(\langle\ w',w''\ \rangle\) are in the access relation, then \(\langle\ w,w''\ \rangle\) is in the access relation.

Symmetry

In every model, for each world \(w\) and each world \(w'\), if \(\langle\ w,w'\ \rangle\) is in the access relation, then so is \(\langle\ w',w\ \rangle\).

Tableaux

S5LP tableaux are constructed just like KFDE system tableaux.

Nodes

Nodes for many-valued modal tableaux come in two types:

• A node consisting of a sentence, a designation marker (⊕ or ⊖), and a world.

• An access node like \(w_1Rw_2\), indicating that the pair \(\langle\ w_1, w_2\ \rangle\) is in the access relation \(R\).

Trunk

To build the trunk for an argument, add a designated node with each premise at world \(w_0\), followed by an undesignated node with the the conclusion at world \(w_0\).

To build the trunk for the argument A₁ ... A_n ∴ B write:

A₁ ⊕, w₀

⋮

A_n ⊕, w₀

B ⊖, w₀

Closure

S5LP includes the LP and FDE closure rules.

⊗LPGap Closure

A ⊖, w₀

⋮

¬A ⊖, w₀

⊗

⊗FDEDesignation Closure

A ⊕, w₀

⋮

A ⊖, w₀

⊗

Rules

S5LP contains all the KFDE rules plus the S5 access rules.

Access Rules

R+S4Transitive

w₀Rw₁

w₁Rw₂

⋮

w₀Rw₂

R≤TReflexive

A, w₀

⋮

w₀Rw₀

R⌯S5Symmetric

w₀Rw₁

⋮

w₁Rw₀

Modal Operator Rules

◇ Rules

◇⊕KFDEPossibility Designated

◇A ⊕, w₀

⋮

A ⊕, w₁

w₀Rw₁

◇⊖KFDEPossibility Undesignated

◇A ⊖, w₀

w₀Rw₁

⋮

A ⊖, w₁

¬◇⊕KFDEPossibility Negated Designated

¬◇A ⊕, w₀

⋮

◻¬A ⊕, w₀

¬◇⊖KFDEPossibility Negated Undesignated

¬◇A ⊖, w₀

⋮

◻¬A ⊖, w₀

◻ Rules

◻⊕KFDENecessity Designated

◻A ⊕, w₀

w₀Rw₁

⋮

A ⊕, w₁

◻⊖KFDENecessity Undesignated

◻A ⊖, w₀

⋮

A ⊖, w₁

w₀Rw₁

¬◻⊕KFDENecessity Negated Designated

¬◻A ⊕, w₀

⋮

◇¬A ⊕, w₀

¬◻⊖KFDENecessity Negated Undesignated

¬◻A ⊖, w₀

⋮

◇¬A ⊖, w₀

Operator Rules

¬ Rules

¬¬⊕FDEDouble Negation Designated

¬¬A ⊕, w₀

⋮

A ⊕, w₀

¬¬⊖FDEDouble Negation Undesignated

¬¬A ⊖, w₀

⋮

A ⊖, w₀

∧ Rules

∧⊕FDEConjunction Designated

A ∧ B ⊕, w₀

⋮

A ⊕, w₀

B ⊕, w₀

∧⊖FDEConjunction Undesignated

A ∧ B ⊖, w₀

⋮

A ⊖, w₀

B ⊖, w₀

¬∧⊕FDEConjunction Negated Designated

¬(A ∧ B) ⊕, w₀

⋮

¬A ⊕, w₀

¬B ⊕, w₀

¬∧⊖FDEConjunction Negated Undesignated

¬(A ∧ B) ⊖, w₀

⋮

¬A ⊖, w₀

¬B ⊖, w₀

∨ Rules

∨⊕FDEDisjunction Designated

A ∨ B ⊕, w₀

⋮

A ⊕, w₀

B ⊕, w₀

∨⊖FDEDisjunction Undesignated

A ∨ B ⊖, w₀

⋮

A ⊖, w₀

B ⊖, w₀

¬∨⊕FDEDisjunction Negated Designated

¬(A ∨ B) ⊕, w₀

⋮

¬A ⊕, w₀

¬B ⊕, w₀

¬∨⊖FDEDisjunction Negated Undesignated

¬(A ∨ B) ⊖, w₀

⋮

¬A ⊖, w₀

¬B ⊖, w₀

⊃ Rules

⊃⊕FDEMaterial Conditional Designated

A ⊃ B ⊕, w₀

⋮

¬A ⊕, w₀

B ⊕, w₀

⊃⊖FDEMaterial Conditional Undesignated

A ⊃ B ⊖, w₀

⋮

¬A ⊖, w₀

B ⊖, w₀

¬⊃⊕FDEMaterial Conditional Negated Designated

¬(A ⊃ B) ⊕, w₀

⋮

A ⊕, w₀

¬B ⊕, w₀

¬⊃⊖FDEMaterial Conditional Negated Undesignated

¬(A ⊃ B) ⊖, w₀

⋮

A ⊖, w₀

¬B ⊖, w₀

≡ Rules

≡⊕FDEMaterial Biconditional Designated

A ≡ B ⊕, w₀

⋮

¬A ⊕, w₀

¬B ⊕, w₀

B ⊕, w₀

A ⊕, w₀

≡⊖FDEMaterial Biconditional Undesignated

A ≡ B ⊖, w₀

⋮

A ⊖, w₀

¬B ⊖, w₀

¬A ⊖, w₀

B ⊖, w₀

¬≡⊕FDEMaterial Biconditional Negated Designated

¬(A ≡ B) ⊕, w₀

⋮

A ⊕, w₀

¬B ⊕, w₀

¬A ⊕, w₀

B ⊕, w₀

¬≡⊖FDEMaterial Biconditional Negated Undesignated

¬(A ≡ B) ⊖, w₀

⋮

¬A ⊖, w₀

¬B ⊖, w₀

B ⊖, w₀

A ⊖, w₀

Quantifier Rules

∃ Rules

∃⊕FDEExistential Designated

∃xFx ⊕, w₀

⋮

Fa ⊕, w₀

∃⊖FDEExistential Undesignated

∃xFx ⊖, w₀

⋮

Fa ⊖, w₀

¬∃⊕FDEExistential Negated Designated

¬∃xFx ⊕, w₀

⋮

∀x¬Fx ⊕, w₀

¬∃⊖FDEExistential Negated Undesignated

¬∃xFx ⊖, w₀

⋮

∀x¬Fx ⊖, w₀

∀ Rules

∀⊕FDEUniversal Designated

∀xFx ⊕, w₀

⋮

Fa ⊕, w₀

∀⊖FDEUniversal Undesignated

∀xFx ⊖, w₀

⋮

Fa ⊖, w₀

¬∀⊕FDEUniversal Negated Designated

¬∀xFx ⊕, w₀

⋮

∃x¬Fx ⊕, w₀

¬∀⊖FDEUniversal Negated Undesignated

¬∀xFx ⊖, w₀

⋮

∃x¬Fx ⊖, w₀

Compatibility Rules

⚬ Rules

⚬⊕FDEAssertion Designated

⚬A ⊕, w₀

⋮

A ⊕, w₀

⚬⊖FDEAssertion Undesignated

⚬A ⊖, w₀

⋮

A ⊖, w₀

¬⚬⊕FDEAssertion Negated Designated

¬⚬A ⊕, w₀

⋮

¬A ⊕, w₀

¬⚬⊖FDEAssertion Negated Undesignated

¬⚬A ⊖, w₀

⋮

¬A ⊖, w₀

→ Rules

→⊕FDEConditional Designated

A → B ⊕, w₀

⋮

¬A ⊕, w₀

B ⊕, w₀

→⊖FDEConditional Undesignated

A → B ⊖, w₀

⋮

¬A ⊖, w₀

B ⊖, w₀

¬→⊕FDEConditional Negated Designated

¬(A → B) ⊕, w₀

⋮

A ⊕, w₀

¬B ⊕, w₀

¬→⊖FDEConditional Negated Undesignated

¬(A → B) ⊖, w₀

⋮

A ⊖, w₀

¬B ⊖, w₀

↔ Rules

↔⊕FDEBiconditional Designated

A ↔ B ⊕, w₀

⋮

¬A ⊕, w₀

¬B ⊕, w₀

B ⊕, w₀

A ⊕, w₀

↔⊖FDEBiconditional Undesignated

A ↔ B ⊖, w₀

⋮

A ⊖, w₀

¬B ⊖, w₀

¬A ⊖, w₀

B ⊖, w₀

¬↔⊕FDEBiconditional Negated Designated

¬(A ↔ B) ⊕, w₀

⋮

A ⊕, w₀

¬B ⊕, w₀

¬A ⊕, w₀

B ⊕, w₀

¬↔⊖FDEBiconditional Negated Undesignated

¬(A ↔ B) ⊖, w₀

⋮

¬A ⊖, w₀

¬B ⊖, w₀

B ⊖, w₀

A ⊖, w₀

Notes

References

• Priest, Graham. An Introduction to Non-Classical Logic: From If to Is. Cambridge University Press, 2008.

class Rules

closure: tuple[type[ClosingRule], ...] = (<class 'pytableaux.logics.lp.Rules.GapClosure'>, <class 'pytableaux.logics.fde.Rules.DesignationClosure'>)

groups: tuple[tuple[type[Rule], ...], ...] = ((<class 'pytableaux.logics.fde.Rules.AssertionDesignated'>, <class 'pytableaux.logics.fde.Rules.AssertionUndesignated'>, <class 'pytableaux.logics.fde.Rules.AssertionNegatedDesignated'>, <class 'pytableaux.logics.fde.Rules.AssertionNegatedUndesignated'>, <class 'pytableaux.logics.fde.Rules.ConjunctionDesignated'>, <class 'pytableaux.logics.fde.Rules.ConjunctionNegatedUndesignated'>, <class 'pytableaux.logics.fde.Rules.DisjunctionNegatedDesignated'>, <class 'pytableaux.logics.fde.Rules.DisjunctionUndesignated'>, <class 'pytableaux.logics.fde.Rules.MaterialConditionalNegatedDesignated'>, <class 'pytableaux.logics.fde.Rules.MaterialConditionalUndesignated'>, <class 'pytableaux.logics.fde.Rules.ConditionalUndesignated'>, <class 'pytableaux.logics.fde.Rules.ConditionalNegatedDesignated'>, <class 'pytableaux.logics.fde.Rules.ExistentialNegatedDesignated'>, <class 'pytableaux.logics.fde.Rules.ExistentialNegatedUndesignated'>, <class 'pytableaux.logics.fde.Rules.UniversalNegatedDesignated'>, <class 'pytableaux.logics.fde.Rules.UniversalNegatedUndesignated'>, <class 'pytableaux.logics.fde.Rules.DoubleNegationDesignated'>, <class 'pytableaux.logics.fde.Rules.DoubleNegationUndesignated'>, <class 'pytableaux.logics.kfde.Rules.PossibilityNegatedDesignated'>, <class 'pytableaux.logics.kfde.Rules.PossibilityNegatedUndesignated'>, <class 'pytableaux.logics.kfde.Rules.NecessityNegatedDesignated'>, <class 'pytableaux.logics.kfde.Rules.NecessityNegatedUndesignated'>), (<class 'pytableaux.logics.s4.Rules.Transitive'>,), (<class 'pytableaux.logics.kfde.Rules.NecessityDesignated'>, <class 'pytableaux.logics.kfde.Rules.PossibilityUndesignated'>), (<class 'pytableaux.logics.kfde.Rules.NecessityUndesignated'>, <class 'pytableaux.logics.kfde.Rules.PossibilityDesignated'>), (<class 'pytableaux.logics.t.Rules.Reflexive'>,), (<class 'pytableaux.logics.fde.Rules.ConjunctionNegatedDesignated'>, <class 'pytableaux.logics.fde.Rules.ConjunctionUndesignated'>, <class 'pytableaux.logics.fde.Rules.DisjunctionDesignated'>, <class 'pytableaux.logics.fde.Rules.DisjunctionNegatedUndesignated'>, <class 'pytableaux.logics.fde.Rules.MaterialConditionalDesignated'>, <class 'pytableaux.logics.fde.Rules.MaterialConditionalNegatedUndesignated'>, <class 'pytableaux.logics.fde.Rules.MaterialBiconditionalDesignated'>, <class 'pytableaux.logics.fde.Rules.MaterialBiconditionalNegatedDesignated'>, <class 'pytableaux.logics.fde.Rules.MaterialBiconditionalUndesignated'>, <class 'pytableaux.logics.fde.Rules.MaterialBiconditionalNegatedUndesignated'>, <class 'pytableaux.logics.fde.Rules.ConditionalDesignated'>, <class 'pytableaux.logics.fde.Rules.ConditionalNegatedUndesignated'>, <class 'pytableaux.logics.fde.Rules.BiconditionalDesignated'>, <class 'pytableaux.logics.fde.Rules.BiconditionalNegatedDesignated'>, <class 'pytableaux.logics.fde.Rules.BiconditionalUndesignated'>, <class 'pytableaux.logics.fde.Rules.BiconditionalNegatedUndesignated'>), (<class 'pytableaux.logics.fde.Rules.ExistentialDesignated'>, <class 'pytableaux.logics.fde.Rules.ExistentialUndesignated'>), (<class 'pytableaux.logics.fde.Rules.UniversalDesignated'>, <class 'pytableaux.logics.fde.Rules.UniversalUndesignated'>), (<class 'pytableaux.logics.s5.Rules.Symmetric'>,))