KB³_E - B³_E with K Modal

---

Semantics

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

Modal Operators

Possibility

The value of a necessity sentence ◻A at \(w\) is the maximum value of its operand \(A\) at each world \(w'\) such that \(\langle\ w, w'\ \rangle\) is in \(R\).

Necessity

The value of a necessity sentence ◻A at \(w\) is the minimum value of its operand \(A\) at each world \(w'\) such that \(\langle\ w, w'\ \rangle\) is in \(R\).

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 B³_E.

⊗K₃Glut Closure

A ⊕, w₀

⋮

¬A ⊕, w₀

⊗

⊗FDEDesignation Closure

A ⊕, w₀

⋮

A ⊖, w₀

⊗

Rules

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

Modal Operator Rules

◇ Rules

◇⊕KFDEPossibility Designated

◇A ⊕, w₀

⋮

A ⊕, w₁

w₀Rw₁

◇⊖KFDEPossibility Undesignated

◇A ⊖, w₀

w₀Rw₁

⋮

A ⊖, w₁

¬◇⊕KFDEPossibility Negated Designated

¬◇A ⊕, w₀

⋮

◻¬A ⊕, w₀

¬◇⊖KFDEPossibility Negated Undesignated

¬◇A ⊖, w₀

⋮

◻¬A ⊖, w₀

◻ Rules

◻⊕KFDENecessity Designated

◻A ⊕, w₀

w₀Rw₁

⋮

A ⊕, w₁

◻⊖KFDENecessity Undesignated

◻A ⊖, w₀

⋮

A ⊖, w₁

w₀Rw₁

¬◻⊕KFDENecessity Negated Designated

¬◻A ⊕, w₀

⋮

◇¬A ⊕, w₀

¬◻⊖KFDENecessity Negated Undesignated

¬◻A ⊖, w₀

⋮

◇¬A ⊖, w₀

Operator Rules

¬ Rules

¬¬⊕FDEDouble Negation Designated

¬¬A ⊕, w₀

⋮

A ⊕, w₀

¬¬⊖FDEDouble Negation Undesignated

¬¬A ⊖, w₀

⋮

A ⊖, w₀

∧ Rules

∧⊕FDEConjunction Designated

A ∧ B ⊕, w₀

⋮

A ⊕, w₀

B ⊕, w₀

∧⊖FDEConjunction Undesignated

A ∧ B ⊖, w₀

⋮

A ⊖, w₀

B ⊖, w₀

¬∧⊕K³_WConjunction Negated Designated

¬(A ∧ B) ⊕, w₀

⋮

A ⊕, w₀

¬B ⊕, w₀

¬A ⊕, w₀

B ⊕, w₀

¬A ⊕, w₀

¬B ⊕, w₀

¬∧⊖K³_WConjunction Negated Undesignated

¬(A ∧ B) ⊖, w₀

⋮

A ⊖, w₀

¬A ⊖, w₀

B ⊖, w₀

¬B ⊖, w₀

A ⊕, w₀

B ⊕, w₀

∨ Rules

∨⊕K³_WDisjunction Designated

A ∨ B ⊕, w₀

⋮

A ⊕, w₀

¬B ⊕, w₀

¬A ⊕, w₀

B ⊕, w₀

A ⊕, w₀

B ⊕, w₀

∨⊖K³_WDisjunction Undesignated

A ∨ B ⊖, w₀

⋮

A ⊖, w₀

¬A ⊖, w₀

B ⊖, w₀

¬B ⊖, w₀

¬A ⊕, w₀

¬B ⊕, w₀

¬∨⊕FDEDisjunction Negated Designated

¬(A ∨ B) ⊕, w₀

⋮

¬A ⊕, w₀

¬B ⊕, w₀

¬∨⊖K³_WDisjunction Negated Undesignated

¬(A ∨ B) ⊖, w₀

⋮

A ∨ B ⊕, w₀

A ⊖, w₀

¬A ⊖, w₀

B ⊖, w₀

¬B ⊖, w₀

⊃ Rules

⊃⊕K³_WMaterial Conditional Designated

A ⊃ B ⊕, w₀

⋮

¬A ∨ B ⊕, w₀

⊃⊖K³_WMaterial Conditional Undesignated

A ⊃ B ⊖, w₀

⋮

¬A ∨ B ⊖, w₀

¬⊃⊕K³_WMaterial Conditional Negated Designated

¬(A ⊃ B) ⊕, w₀

⋮

¬(¬A ∨ B) ⊕, w₀

¬⊃⊖K³_WMaterial Conditional Negated Undesignated

¬(A ⊃ B) ⊖, w₀

⋮

¬(¬A ∨ B) ⊖, w₀

≡ Rules

≡⊕K³_WMaterial Biconditional Designated

A ≡ B ⊕, w₀

⋮

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

≡⊖B³_EMaterial Biconditional Undesignated

A ≡ B ⊖, w₀

⋮

A ⊖, w₀

¬A ⊖, w₀

B ⊖, w₀

¬B ⊖, w₀

A ⊕, w₀

¬B ⊕, w₀

¬A ⊕, w₀

B ⊕, w₀

¬≡⊕K³_WMaterial Biconditional Negated Designated

¬(A ≡ B) ⊕, w₀

⋮

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

¬≡⊖B³_EMaterial Biconditional Negated Undesignated

¬(A ≡ B) ⊖, w₀

⋮

A ⊖, w₀

¬A ⊖, w₀

B ⊖, w₀

¬B ⊖, w₀

¬A ⊕, w₀

¬B ⊕, w₀

A ⊕, w₀

B ⊕, w₀

Quantifier Rules

∃ Rules

∃⊕FDEExistential Designated

∃xFx ⊕, w₀

⋮

Fa ⊕, w₀

∃⊖FDEExistential Undesignated

∃xFx ⊖, w₀

⋮

Fa ⊖, w₀

¬∃⊕FDEExistential Negated Designated

¬∃xFx ⊕, w₀

⋮

∀x¬Fx ⊕, w₀

¬∃⊖FDEExistential Negated Undesignated

¬∃xFx ⊖, w₀

⋮

∀x¬Fx ⊖, w₀

∀ Rules

∀⊕FDEUniversal Designated

∀xFx ⊕, w₀

⋮

Fa ⊕, w₀

∀⊖FDEUniversal Undesignated

∀xFx ⊖, w₀

⋮

Fa ⊖, w₀

¬∀⊕FDEUniversal Negated Designated

¬∀xFx ⊕, w₀

⋮

∃x¬Fx ⊕, w₀

¬∀⊖FDEUniversal Negated Undesignated

¬∀xFx ⊖, w₀

⋮

∃x¬Fx ⊖, w₀

Compatibility Rules

⚬ Rules

⚬⊕FDEAssertion Designated

⚬A ⊕, w₀

⋮

A ⊕, w₀

⚬⊖FDEAssertion Undesignated

⚬A ⊖, w₀

⋮

A ⊖, w₀

¬⚬⊕B³_EAssertion Negated Designated

¬⚬A ⊕, w₀

⋮

A ⊖, w₀

¬⚬⊖B³_EAssertion Negated Undesignated

¬⚬A ⊖, w₀

⋮

A ⊕, w₀

→ Rules

→⊕B³_EConditional Designated

A → B ⊕, w₀

⋮

¬⚬A ∨ ⚬B ⊕, w₀

→⊖B³_EConditional Undesignated

A → B ⊖, w₀

⋮

A ⊕, w₀

B ⊖, w₀

¬→⊕B³_EConditional Negated Designated

¬(A → B) ⊕, w₀

⋮

A ⊕, w₀

B ⊖, w₀

¬→⊖B³_EConditional Negated Undesignated

¬(A → B) ⊖, w₀

⋮

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

↔ Rules

↔⊕B³_EBiconditional Designated

A ↔ B ⊕, w₀

⋮

¬⚬A ∨ ⚬B ⊕, w₀

¬⚬B ∨ ⚬A ⊕, w₀

↔⊖B³_EBiconditional Undesignated

A ↔ B ⊖, w₀

⋮

¬⚬A ∨ ⚬B ⊖, w₀

¬⚬B ∨ ⚬A ⊖, w₀

¬↔⊕B³_EBiconditional Negated Designated

¬(A ↔ B) ⊕, w₀

⋮

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

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

¬↔⊖B³_EBiconditional Negated Undesignated

¬(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

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