TK³_W - K³_W with T Modal

Semantics 

TK³_W semantics behave just like KK³_W semantics.

TK³_W includes the T reflexive restriction on the access relation for models.

Reflexivity

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

Tableaux 

TK³_W 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 

TK³_W includes the K₃ and FDE closure rules.

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

⋮

¬A ⊕, w₀

⊗

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

⋮

A ⊖, w₀

⊗

Rules 

TK³_W contains all the KK³_W rules plus the T Reflexive rule.

The Reflexive rule applies to an open branch b when there is a node n on b with a world w but there is not a node where w accesses w (itself).

Access Rules

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

⋮

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₀

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

⋮

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

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

⋮

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

¬≡⊖K³_WMaterial 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₀

→ Rules

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

⋮

¬A ∨ B ⊕, w₀

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

⋮

¬A ∨ B ⊖, w₀

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

⋮

¬(¬A ∨ B) ⊕, w₀

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

⋮

¬(¬A ∨ B) ⊖, w₀

↔ Rules

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

⋮

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

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

⋮

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

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

⋮

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

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

⋮

¬((A ⊃ B) ∧ (B ⊃ 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.DisjunctionNegatedDesignated'>, <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.k3w.Rules.ConditionalDesignated'>, <class 'pytableaux.logics.k3w.Rules.ConditionalUndesignated'>, <class 'pytableaux.logics.k3w.Rules.ConditionalNegatedDesignated'>, <class 'pytableaux.logics.k3w.Rules.ConditionalNegatedUndesignated'>, <class 'pytableaux.logics.k3w.Rules.MaterialBiconditionalDesignated'>, <class 'pytableaux.logics.k3w.Rules.MaterialBiconditionalUndesignated'>, <class 'pytableaux.logics.k3w.Rules.MaterialBiconditionalNegatedDesignated'>, <class 'pytableaux.logics.k3w.Rules.MaterialBiconditionalNegatedUndesignated'>, <class 'pytableaux.logics.k3w.Rules.BiconditionalDesignated'>, <class 'pytableaux.logics.k3w.Rules.BiconditionalUndesignated'>, <class 'pytableaux.logics.k3w.Rules.BiconditionalNegatedDesignated'>, <class 'pytableaux.logics.k3w.Rules.BiconditionalNegatedUndesignated'>, <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.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.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.fde.Rules.ExistentialDesignated'>, <class 'pytableaux.logics.fde.Rules.ExistentialUndesignated'>), (<class 'pytableaux.logics.fde.Rules.UniversalDesignated'>, <class 'pytableaux.logics.fde.Rules.UniversalUndesignated'>))

TK3W - K3W with T Modal