KLP - LP with K Modal

Semantics 

A KLP frame comprises the interpretation of sentences and predicates at a world. A KLP model comprises a non-empty collection of KLP 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 LP.

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_{1} R w_{2}$ , indicating that the pair $⟨ w_{1}, w_{2} ⟩$ 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 LP.

⊗LPGap Closure[source]: A ⊖, w₀

⋮

¬A ⊖, w₀

⊗

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

⋮

A ⊖, w₀

⊗

Rules 

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

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₀

¬∧⊕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

⊃⊕FDEMaterial Conditional Designated[source]: A ⊃ B ⊕, w₀

⋮

¬A ⊕, w₀

B ⊕, w₀

⊃⊖FDEMaterial Conditional Undesignated[source]: A ⊃ B ⊖, w₀

⋮

¬A ⊖, w₀

B ⊖, w₀

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

⋮

A ⊕, w₀

¬B ⊕, w₀

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

⋮

A ⊖, w₀

¬B ⊖, w₀

≡ Rules

≡⊕FDEMaterial Biconditional Designated[source]: A ≡ B ⊕, w₀

⋮

¬A ⊕, w₀

¬B ⊕, w₀

B ⊕, w₀

A ⊕, w₀

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

⋮

A ⊖, w₀

¬B ⊖, w₀

¬A ⊖, w₀

B ⊖, w₀

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

⋮

A ⊕, w₀

¬B ⊕, w₀

¬A ⊕, w₀

B ⊕, w₀

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

⋮

¬A ⊖, w₀

¬B ⊖, w₀

B ⊖, w₀

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

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

⋮

¬A ⊕, w₀

B ⊕, w₀

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

⋮

¬A ⊖, w₀

B ⊖, w₀

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

⋮

A ⊕, w₀

¬B ⊕, w₀

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

⋮

A ⊖, w₀

¬B ⊖, w₀

↔ Rules

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

⋮

¬A ⊕, w₀

¬B ⊕, w₀

B ⊕, w₀

A ⊕, w₀

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

⋮

A ⊖, w₀

¬B ⊖, w₀

¬A ⊖, w₀

B ⊖, w₀

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

⋮

A ⊕, w₀

¬B ⊕, w₀

¬A ⊕, w₀

B ⊕, w₀

¬↔⊖FDEBiconditional Negated Undesignated[source]: ¬(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[source]

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.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.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'>))