KG₃ - G₃ with K Modal

Semantics 

A KG₃ frame comprises the interpretation of sentences and predicates at a world. A KG₃ model comprises a non-empty collection of KG₃ frames, a world access relation \(R\), and a set of constants (the domain).

The semantics for predication, quantification, and truth-functional operators are the same as G₃.

Consequence 

Logical Consequence is defined just as in KFDE.

Logical Consequence

C is a Logical Consequence of A iff all models where A has a desginated value at \(w_0\) are models where C also has a designated value at \(w_0\).

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 

The closure rules are the same as G₃.

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

⋮

¬A ⊕, w₀

⊗

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

⋮

A ⊖, w₀

⊗

Rules 

Non-modal rules for KG₃ are exactly like their G₃ counterparts, with the addition of carrying over the world marker from the target node(s).

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.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.kfde.Rules.NecessityDesignated'>, <class 'pytableaux.logics.kfde.Rules.PossibilityUndesignated'>), (<class 'pytableaux.logics.kfde.Rules.NecessityUndesignated'>, <class 'pytableaux.logics.kfde.Rules.PossibilityDesignated'>), (<class 'pytableaux.logics.fde.Rules.ExistentialDesignated'>, <class 'pytableaux.logics.fde.Rules.ExistentialUndesignated'>), (<class 'pytableaux.logics.fde.Rules.UniversalDesignated'>, <class 'pytableaux.logics.fde.Rules.UniversalUndesignated'>))

KG3 - G3 with K Modal

Modal Operator Rules

◇ Rules

◻ Rules