S5G₃ - G₃ with S5 Modal

Semantics 

S5G₃ semantics behave just like KG₃ semantics.

S5G₃ 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 

S5G₃ 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 

S5G₃ includes the K₃ and FDE closure rules.

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

⋮

¬A ⊕, w₀

⊗

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

⋮

A ⊖, w₀

⊗

Rules 

S5G₃ contains all the KG₃ 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

¬¬⊕G₃Double Negation Designated[source]: ¬¬A ⊕, w₀

⋮

¬A ⊖, w₀

¬¬⊖G₃Double 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₀

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

⋮

¬A ⊕, w₀

¬B ⊕, w₀

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

⋮

¬A ⊖, w₀

¬B ⊖, w₀

∨ Rules

∨⊕FDEDisjunction Designated[source]: A ∨ B ⊕, w₀

⋮

A ⊕, w₀

B ⊕, w₀

∨⊖FDEDisjunction Undesignated[source]: A ∨ B ⊖, w₀

⋮

A ⊖, w₀

B ⊖, w₀

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

⋮

¬A ⊕, w₀

¬B ⊕, w₀

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

⋮

¬A ⊖, w₀

¬B ⊖, w₀

⊃ Rules

⊃⊕G₃Material Conditional Designated[source]: A ⊃ B ⊕, w₀

⋮

¬A ∨ B ⊕, w₀

⊃⊖G₃Material Conditional Undesignated[source]: A ⊃ B ⊖, w₀

⋮

¬A ∨ B ⊖, w₀

¬⊃⊕G₃Material Conditional Negated Designated[source]: ¬(A ⊃ B) ⊕, w₀

⋮

¬(¬A ∨ B) ⊕, w₀

¬⊃⊖G₃Material Conditional Negated Undesignated[source]: ¬(A ⊃ B) ⊖, w₀

⋮

¬(¬A ∨ B) ⊖, w₀

≡ Rules

≡⊕G₃Material Biconditional Designated[source]: A ≡ B ⊕, w₀

⋮

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

≡⊖G₃Material Biconditional Undesignated[source]: A ≡ B ⊖, w₀

⋮

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

¬≡⊕G₃Material Biconditional Negated Designated[source]: ¬(A ≡ B) ⊕, w₀

⋮

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

¬≡⊖G₃Material Biconditional Negated Undesignated[source]: ¬(A ≡ B) ⊖, w₀

⋮

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

→ Rules

→⊕L₃Conditional Designated[source]: A → B ⊕, w₀

⋮

¬A ∨ B ⊕, w₀

A ⊖, w₀

B ⊖, w₀

¬A ⊖, w₀

¬B ⊖, w₀

→⊖L₃Conditional Undesignated[source]: A → B ⊖, w₀

⋮

A ⊕, w₀

B ⊖, w₀

A ⊖, w₀

¬A ⊖, w₀

¬B ⊕, w₀

¬→⊕G₃Conditional Negated Designated[source]: ¬(A → B) ⊕, w₀

⋮

A ⊕, w₀

¬B ⊕, w₀

A ⊖, w₀

¬A ⊖, w₀

¬B ⊕, w₀

¬→⊖G₃Conditional Negated Undesignated[source]: ¬(A → B) ⊖, w₀

⋮

¬A ⊕, w₀

¬B ⊖, w₀

↔ Rules

↔⊕G₃Biconditional Designated[source]: A ↔ B ⊕, w₀

⋮

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

↔⊖G₃Biconditional Undesignated[source]: A ↔ B ⊖, w₀

⋮

(A → B) ∧ (B → A) ⊖, w₀

¬↔⊕G₃Biconditional Negated Designated[source]: ¬(A ↔ B) ⊕, w₀

⋮

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

¬↔⊖G₃Biconditional Negated Undesignated[source]: ¬(A ↔ B) ⊖, w₀

⋮

¬((A → B) ∧ (B → A)) ⊖, 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₀

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

⋮

¬A ⊕, w₀

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

⋮

¬A ⊖, 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.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.ExistentialNegatedDesignated'>, <class 'pytableaux.logics.fde.Rules.ExistentialNegatedUndesignated'>, <class 'pytableaux.logics.fde.Rules.UniversalNegatedDesignated'>, <class 'pytableaux.logics.fde.Rules.UniversalNegatedUndesignated'>, <class 'pytableaux.logics.g3.Rules.DoubleNegationDesignated'>, <class 'pytableaux.logics.g3.Rules.DoubleNegationUndesignated'>, <class 'pytableaux.logics.g3.Rules.MaterialConditionalNegatedDesignated'>, <class 'pytableaux.logics.g3.Rules.MaterialConditionalUndesignated'>, <class 'pytableaux.logics.g3.Rules.MaterialConditionalDesignated'>, <class 'pytableaux.logics.g3.Rules.MaterialConditionalNegatedUndesignated'>, <class 'pytableaux.logics.g3.Rules.MaterialBiconditionalDesignated'>, <class 'pytableaux.logics.g3.Rules.MaterialBiconditionalNegatedDesignated'>, <class 'pytableaux.logics.g3.Rules.MaterialBiconditionalUndesignated'>, <class 'pytableaux.logics.g3.Rules.MaterialBiconditionalNegatedUndesignated'>, <class 'pytableaux.logics.g3.Rules.BiconditionalDesignated'>, <class 'pytableaux.logics.g3.Rules.BiconditionalNegatedUndesignated'>, <class 'pytableaux.logics.g3.Rules.BiconditionalUndesignated'>, <class 'pytableaux.logics.g3.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.ConjunctionNegatedDesignated'>, <class 'pytableaux.logics.fde.Rules.ConjunctionUndesignated'>, <class 'pytableaux.logics.fde.Rules.DisjunctionDesignated'>, <class 'pytableaux.logics.fde.Rules.DisjunctionNegatedUndesignated'>, <class 'pytableaux.logics.l3.Rules.ConditionalDesignated'>, <class 'pytableaux.logics.l3.Rules.ConditionalUndesignated'>, <class 'pytableaux.logics.g3.Rules.ConditionalNegatedUndesignated'>, <class 'pytableaux.logics.g3.Rules.ConditionalNegatedDesignated'>), (<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'>,))

S5G3 - G3 with S5 Modal