S5B³_E - B³_E with S5 Modal

Semantics 

S5B³_E semantics behave just like KB³_E semantics.

S5B³_E 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 

S5B³_E 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 

S5B³_E includes the K₃ and FDE closure rules.

⊗K₃Glut Closure[source]: A ⊕, w₀

⋮

¬A ⊕, w₀

⊗

⊗FDEDesignation Closure[source]: A ⊕, w₀

⋮

A ⊖, w₀

⊗

Rules 

S5B³_E contains all the KB³_E rules plus the S5 access rules.

Access Rules

R+S4Transitive[source]: w₀Rw₁

w₁Rw₂

⋮

w₀Rw₂

R≤TReflexive[source]: A, w₀

⋮

w₀Rw₀

R⌯S5Symmetric[source]: w₀Rw₁

⋮

w₁Rw₀

Operator Rules

¬ Rules

¬¬⊕FDEDouble Negation Designated[source]: ¬¬A ⊕, w₀

⋮

A ⊕, w₀

¬¬⊖FDEDouble Negation Undesignated[source]: ¬¬A ⊖, w₀

⋮

A ⊖, w₀

∧ Rules

∧⊕FDEConjunction Designated[source]: A ∧ B ⊕, w₀

⋮

A ⊕, w₀

B ⊕, w₀

∧⊖FDEConjunction Undesignated[source]: A ∧ B ⊖, w₀

⋮

A ⊖, w₀

B ⊖, w₀

¬∧⊕K³_WConjunction Negated Designated[source]: ¬(A ∧ B) ⊕, w₀

⋮

A ⊕, w₀

¬B ⊕, w₀

¬A ⊕, w₀

B ⊕, w₀

¬A ⊕, w₀

¬B ⊕, w₀

¬∧⊖K³_WConjunction Negated Undesignated[source]: ¬(A ∧ B) ⊖, w₀

⋮

A ⊖, w₀

¬A ⊖, w₀

B ⊖, w₀

¬B ⊖, w₀

A ⊕, w₀

B ⊕, w₀

∨ Rules

∨⊕K³_WDisjunction Designated[source]: A ∨ B ⊕, w₀

⋮

A ⊕, w₀

¬B ⊕, w₀

¬A ⊕, w₀

B ⊕, w₀

A ⊕, w₀

B ⊕, w₀

∨⊖K³_WDisjunction Undesignated[source]: A ∨ B ⊖, w₀

⋮

A ⊖, w₀

¬A ⊖, w₀

B ⊖, w₀

¬B ⊖, w₀

¬A ⊕, w₀

¬B ⊕, w₀

¬∨⊕FDEDisjunction Negated Designated[source]: ¬(A ∨ B) ⊕, w₀

⋮

¬A ⊕, w₀

¬B ⊕, w₀

¬∨⊖K³_WDisjunction Negated Undesignated[source]: ¬(A ∨ B) ⊖, w₀

⋮

A ∨ B ⊕, w₀

A ⊖, w₀

¬A ⊖, w₀

B ⊖, w₀

¬B ⊖, w₀

⊃ Rules

⊃⊕K³_WMaterial Conditional Designated[source]: A ⊃ B ⊕, w₀

⋮

¬A ∨ B ⊕, w₀

⊃⊖K³_WMaterial Conditional Undesignated[source]: A ⊃ B ⊖, w₀

⋮

¬A ∨ B ⊖, w₀

¬⊃⊕K³_WMaterial Conditional Negated Designated[source]: ¬(A ⊃ B) ⊕, w₀

⋮

¬(¬A ∨ B) ⊕, w₀

¬⊃⊖K³_WMaterial Conditional Negated Undesignated[source]: ¬(A ⊃ B) ⊖, w₀

⋮

¬(¬A ∨ B) ⊖, w₀

≡ Rules

≡⊕K³_WMaterial Biconditional Designated[source]: A ≡ B ⊕, w₀

⋮

(A ⊃ B) ∧ (B ⊃ A) ⊕, w₀

≡⊖B³_EMaterial Biconditional Undesignated[source]: A ≡ B ⊖, w₀

⋮

A ⊖, w₀

¬A ⊖, w₀

B ⊖, w₀

¬B ⊖, w₀

A ⊕, w₀

¬B ⊕, w₀

¬A ⊕, w₀

B ⊕, w₀

¬≡⊕K³_WMaterial Biconditional Negated Designated[source]: ¬(A ≡ B) ⊕, w₀

⋮

¬((A ⊃ B) ∧ (B ⊃ A)) ⊕, w₀

¬≡⊖B³_EMaterial Biconditional Negated Undesignated[source]: ¬(A ≡ B) ⊖, w₀

⋮

A ⊖, w₀

¬A ⊖, w₀

B ⊖, w₀

¬B ⊖, w₀

¬A ⊕, w₀

¬B ⊕, w₀

A ⊕, w₀

B ⊕, w₀

Quantifier Rules

∃ Rules

∃⊕FDEExistential Designated[source]: ∃xFx ⊕, w₀

⋮

Fa ⊕, w₀

∃⊖FDEExistential Undesignated[source]: ∃xFx ⊖, w₀

⋮

Fa ⊖, w₀

¬∃⊕FDEExistential Negated Designated[source]: ¬∃xFx ⊕, w₀

⋮

∀x¬Fx ⊕, w₀

¬∃⊖FDEExistential Negated Undesignated[source]: ¬∃xFx ⊖, w₀

⋮

∀x¬Fx ⊖, w₀

∀ Rules

∀⊕FDEUniversal Designated[source]: ∀xFx ⊕, w₀

⋮

Fa ⊕, w₀

∀⊖FDEUniversal Undesignated[source]: ∀xFx ⊖, w₀

⋮

Fa ⊖, w₀

¬∀⊕FDEUniversal Negated Designated[source]: ¬∀xFx ⊕, w₀

⋮

∃x¬Fx ⊕, w₀

¬∀⊖FDEUniversal Negated Undesignated[source]: ¬∀xFx ⊖, w₀

⋮

∃x¬Fx ⊖, w₀

Compatibility Rules

⚬ Rules

⚬⊕FDEAssertion Designated[source]: ⚬A ⊕, w₀

⋮

A ⊕, w₀

⚬⊖FDEAssertion Undesignated[source]: ⚬A ⊖, w₀

⋮

A ⊖, w₀

¬⚬⊕B³_EAssertion Negated Designated[source]: ¬⚬A ⊕, w₀

⋮

A ⊖, w₀

¬⚬⊖B³_EAssertion Negated Undesignated[source]: ¬⚬A ⊖, w₀

⋮

A ⊕, w₀

→ Rules

→⊕B³_EConditional Designated[source]: A → B ⊕, w₀

⋮

¬⚬A ∨ ⚬B ⊕, w₀

→⊖B³_EConditional Undesignated[source]: A → B ⊖, w₀

⋮

A ⊕, w₀

B ⊖, w₀

¬→⊕B³_EConditional Negated Designated[source]: ¬(A → B) ⊕, w₀

⋮

A ⊕, w₀

B ⊖, w₀

¬→⊖B³_EConditional Negated Undesignated[source]: ¬(A → B) ⊖, w₀

⋮

¬(¬⚬A ∨ ⚬B) ⊖, w₀

↔ Rules

↔⊕B³_EBiconditional Designated[source]: A ↔ B ⊕, w₀

⋮

¬⚬A ∨ ⚬B ⊕, w₀

¬⚬B ∨ ⚬A ⊕, w₀

↔⊖B³_EBiconditional Undesignated[source]: A ↔ B ⊖, w₀

⋮

¬⚬A ∨ ⚬B ⊖, w₀

¬⚬B ∨ ⚬A ⊖, w₀

¬↔⊕B³_EBiconditional Negated Designated[source]: ¬(A ↔ B) ⊕, w₀

⋮

¬(¬⚬A ∨ ⚬B) ⊕, w₀

¬(¬⚬B ∨ ⚬A) ⊕, w₀

¬↔⊖B³_EBiconditional Negated Undesignated[source]: ¬(A ↔ B) ⊖, w₀

⋮

A ⊖, w₀

B ⊖, w₀

A ⊕, w₀

B ⊕, w₀

Notes 

References 

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

class Rules[source]

closure: tuple[type[ClosingRule], ...] = (<class 'pytableaux.logics.k3.Rules.GlutClosure'>, <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.b3e.Rules.AssertionNegatedDesignated'>, <class 'pytableaux.logics.b3e.Rules.AssertionNegatedUndesignated'>, <class 'pytableaux.logics.fde.Rules.ConjunctionDesignated'>, <class 'pytableaux.logics.fde.Rules.DisjunctionNegatedDesignated'>, <class 'pytableaux.logics.b3e.Rules.ConditionalNegatedDesignated'>, <class 'pytableaux.logics.b3e.Rules.ConditionalUndesignated'>, <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.k3w.Rules.MaterialConditionalDesignated'>, <class 'pytableaux.logics.k3w.Rules.MaterialConditionalUndesignated'>, <class 'pytableaux.logics.k3w.Rules.MaterialConditionalNegatedDesignated'>, <class 'pytableaux.logics.k3w.Rules.MaterialConditionalNegatedUndesignated'>, <class 'pytableaux.logics.b3e.Rules.ConditionalDesignated'>, <class 'pytableaux.logics.b3e.Rules.ConditionalNegatedUndesignated'>, <class 'pytableaux.logics.k3w.Rules.MaterialBiconditionalDesignated'>, <class 'pytableaux.logics.k3w.Rules.MaterialBiconditionalNegatedDesignated'>, <class 'pytableaux.logics.b3e.Rules.BiconditionalDesignated'>, <class 'pytableaux.logics.b3e.Rules.BiconditionalUndesignated'>, <class 'pytableaux.logics.b3e.Rules.BiconditionalNegatedDesignated'>, <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.ConjunctionUndesignated'>, <class 'pytableaux.logics.b3e.Rules.BiconditionalNegatedUndesignated'>), (<class 'pytableaux.logics.k3w.Rules.DisjunctionDesignated'>, <class 'pytableaux.logics.k3w.Rules.DisjunctionUndesignated'>, <class 'pytableaux.logics.k3w.Rules.ConjunctionNegatedDesignated'>, <class 'pytableaux.logics.k3w.Rules.ConjunctionNegatedUndesignated'>, <class 'pytableaux.logics.k3w.Rules.DisjunctionNegatedUndesignated'>), (<class 'pytableaux.logics.b3e.Rules.MaterialBiconditionalUndesignated'>, <class 'pytableaux.logics.b3e.Rules.MaterialBiconditionalNegatedUndesignated'>), (<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'>,))

S5B3E - B3E with S5 Modal