KFDE - FDE with K Modal

---

Semantics

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

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 similary as FDE, except with reference to a world:

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

⊗FDEDesignation Closure

A ⊕, w₀

⋮

A ⊖, w₀

⊗

Rules

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

Modal Operator Rules

◇ Rules

◇⊕Possibility Designated

◇A ⊕, w₀

⋮

A ⊕, w₁

w₀Rw₁

◇⊖Possibility Undesignated

◇A ⊖, w₀

w₀Rw₁

⋮

A ⊖, w₁

¬◇⊕Possibility Negated Designated

¬◇A ⊕, w₀

⋮

◻¬A ⊕, w₀

¬◇⊖Possibility Negated Undesignated

¬◇A ⊖, w₀

⋮

◻¬A ⊖, w₀

◻ Rules

◻⊕Necessity Designated

◻A ⊕, w₀

w₀Rw₁

⋮

A ⊕, w₁

◻⊖Necessity Undesignated

◻A ⊖, w₀

⋮

A ⊖, w₁

w₀Rw₁

¬◻⊕Necessity Negated Designated

¬◻A ⊕, w₀

⋮

◇¬A ⊕, w₀

¬◻⊖Necessity 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₀

¬∧⊕FDEConjunction Negated Designated

¬(A ∧ B) ⊕, w₀

⋮

¬A ⊕, w₀

¬B ⊕, w₀

¬∧⊖FDEConjunction Negated Undesignated

¬(A ∧ B) ⊖, w₀

⋮

¬A ⊖, w₀

¬B ⊖, w₀

∨ Rules

∨⊕FDEDisjunction Designated

A ∨ B ⊕, w₀

⋮

A ⊕, w₀

B ⊕, w₀

∨⊖FDEDisjunction Undesignated

A ∨ B ⊖, w₀

⋮

A ⊖, w₀

B ⊖, w₀

¬∨⊕FDEDisjunction Negated Designated

¬(A ∨ B) ⊕, w₀

⋮

¬A ⊕, w₀

¬B ⊕, w₀

¬∨⊖FDEDisjunction Negated Undesignated

¬(A ∨ B) ⊖, w₀

⋮

¬A ⊖, w₀

¬B ⊖, w₀

⊃ Rules

⊃⊕FDEMaterial Conditional Designated

A ⊃ B ⊕, w₀

⋮

¬A ⊕, w₀

B ⊕, w₀

⊃⊖FDEMaterial Conditional Undesignated

A ⊃ B ⊖, w₀

⋮

¬A ⊖, w₀

B ⊖, w₀

¬⊃⊕FDEMaterial Conditional Negated Designated

¬(A ⊃ B) ⊕, w₀

⋮

A ⊕, w₀

¬B ⊕, w₀

¬⊃⊖FDEMaterial Conditional Negated Undesignated

¬(A ⊃ B) ⊖, w₀

⋮

A ⊖, w₀

¬B ⊖, w₀

≡ Rules

≡⊕FDEMaterial Biconditional Designated

A ≡ B ⊕, w₀

⋮

¬A ⊕, w₀

¬B ⊕, w₀

B ⊕, w₀

A ⊕, w₀

≡⊖FDEMaterial Biconditional Undesignated

A ≡ B ⊖, w₀

⋮

A ⊖, w₀

¬B ⊖, w₀

¬A ⊖, w₀

B ⊖, w₀

¬≡⊕FDEMaterial Biconditional Negated Designated

¬(A ≡ B) ⊕, w₀

⋮

A ⊕, w₀

¬B ⊕, w₀

¬A ⊕, w₀

B ⊕, w₀

¬≡⊖FDEMaterial Biconditional Negated Undesignated

¬(A ≡ B) ⊖, w₀

⋮

¬A ⊖, w₀

¬B ⊖, w₀

B ⊖, w₀

A ⊖, 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₀

¬⚬⊕FDEAssertion Negated Designated

¬⚬A ⊕, w₀

⋮

¬A ⊕, w₀

¬⚬⊖FDEAssertion Negated Undesignated

¬⚬A ⊖, w₀

⋮

¬A ⊖, w₀

→ Rules

→⊕FDEConditional Designated

A → B ⊕, w₀

⋮

¬A ⊕, w₀

B ⊕, w₀

→⊖FDEConditional Undesignated

A → B ⊖, w₀

⋮

¬A ⊖, w₀

B ⊖, w₀

¬→⊕FDEConditional Negated Designated

¬(A → B) ⊕, w₀

⋮

A ⊕, w₀

¬B ⊕, w₀

¬→⊖FDEConditional Negated Undesignated

¬(A → B) ⊖, w₀

⋮

A ⊖, w₀

¬B ⊖, w₀

↔ Rules

↔⊕FDEBiconditional Designated

A ↔ B ⊕, w₀

⋮

¬A ⊕, w₀

¬B ⊕, w₀

B ⊕, w₀

A ⊕, w₀

↔⊖FDEBiconditional Undesignated

A ↔ B ⊖, w₀

⋮

A ⊖, w₀

¬B ⊖, w₀

¬A ⊖, w₀

B ⊖, w₀

¬↔⊕FDEBiconditional Negated Designated

¬(A ↔ B) ⊕, w₀

⋮

A ⊕, w₀

¬B ⊕, w₀

¬A ⊕, w₀

B ⊕, w₀

¬↔⊖FDEBiconditional Negated Undesignated

¬(A ↔ B) ⊖, w₀

⋮

¬A ⊖, w₀

¬B ⊖, w₀

B ⊖, w₀

A ⊖, w₀

Notes

• Like FDE, there are no logical truths.

• The standard modal operator interdefinabilities hold: ◻A ⟛ ¬◇¬A and ¬◻A ⟛ ◇¬A.

• Modal forms of modus ponens fail, e.g. ◻(A → B), ◇A ⊬ ◇B.

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.fde.Rules.DesignationClosure'>,)

class PossibilityDesignated(tableau, /, **opts)

◇⊕

◇A ⊕, w₀

⋮

A ⊕, w₁

w₀Rw₁

Parameters:

tableau (Tableau) --

Helpers: Mapping[type[Rule.Helper], Any] = mappingproxy({<class 'pytableaux.proof.helpers.AplSentCount'>: None, <class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=True)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Possibility>}), pred=(<NodeDesignation:(designated=True)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Possibility>), ignore_ticked=True), <class 'pytableaux.proof.helpers.QuitFlag'>: None, <class 'pytableaux.proof.helpers.MaxWorlds'>: Config(operators=qsetf({<Operator: Possibility>, <Operator: Necessity>}))})

Helper classes mapped to their settings.

score_candidate(target, /)

Overrides AdzHelper closure score

Return type:

float

group_score(target, /)

Return type:

float

NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}

branching: int = 0

The number of additional branches created.

defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})

designation: bool | None = True

legend: tuple[tuple[str, Any], ...] = ((Legend.operator, Operator.Possibility), (Legend.designation, True))

The rule class legend.

name: str = 'PossibilityDesignated'

The rule class name.

negated: bool | None = None

operator: Operator | None = (90, 1)

predicate: Predicate | None = None

quantifier: Quantifier | None = None

timer_names: Sequence[str] = qsetf({'search', 'apply'})

StopWatch names to create in timers mapping.

class PossibilityNegatedDesignated(tableau, /, **opts)

¬◇⊕

¬◇A ⊕, w₀

⋮

◻¬A ⊕, w₀

Parameters:

tableau (Tableau) --

Helpers: Mapping[type[Rule.Helper], Any] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=True)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Possibility(negated)>}), pred=(<NodeDesignation:(designated=True)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Possibility(negated)>), ignore_ticked=True)})

Helper classes mapped to their settings.

NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}

branching: int = 0

The number of additional branches created.

defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})

designation: bool | None = True

legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.Possibility), (Legend.designation, True))

The rule class legend.

name: str = 'PossibilityNegatedDesignated'

The rule class name.

negated: bool | None = True

operator: Operator | None = (90, 1)

predicate: Predicate | None = None

quantifier: Quantifier | None = None

timer_names: Sequence[str] = qsetf({'search', 'apply'})

StopWatch names to create in timers mapping.

class NecessityDesignated(tableau, /, **opts)

◻⊕

◻A ⊕, w₀

w₀Rw₁

⋮

A ⊕, w₁

Parameters:

tableau (Tableau) --

ticking: bool = False

Whether this is a ticking rule.

Helpers: Mapping[type[Rule.Helper], Any] = mappingproxy({<class 'pytableaux.proof.helpers.NodeCount'>: None, <class 'pytableaux.proof.helpers.NodesWorlds'>: None, <class 'pytableaux.proof.helpers.WorldIndex'>: None, <class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=True)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Necessity>}), pred=(<NodeDesignation:(designated=True)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Necessity>), ignore_ticked=True), <class 'pytableaux.proof.helpers.QuitFlag'>: None, <class 'pytableaux.proof.helpers.MaxWorlds'>: Config(operators=qsetf({<Operator: Possibility>, <Operator: Necessity>}))})

Helper classes mapped to their settings.

score_candidate(target, /)

Return type:

float

group_score(target, /)

Return type:

float

example_nodes()

NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}

branching: int = 0

The number of additional branches created.

defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})

designation: bool | None = True

legend: tuple[tuple[str, Any], ...] = ((Legend.operator, Operator.Necessity), (Legend.designation, True))

The rule class legend.

name: str = 'NecessityDesignated'

The rule class name.

negated: bool | None = None

operator: Operator | None = (100, 1)

predicate: Predicate | None = None

quantifier: Quantifier | None = None

timer_names: Sequence[str] = qsetf({'search', 'apply'})

StopWatch names to create in timers mapping.

class PossibilityNegatedUndesignated(tableau, /, **opts)

¬◇⊖

¬◇A ⊖, w₀

⋮

◻¬A ⊖, w₀

Parameters:

tableau (Tableau) --

Helpers: Mapping[type[Rule.Helper], Any] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=False)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Possibility(negated)>}), pred=(<NodeDesignation:(designated=False)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Possibility(negated)>), ignore_ticked=True)})

Helper classes mapped to their settings.

NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}

branching: int = 0

The number of additional branches created.

defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})

designation: bool | None = False

legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.Possibility), (Legend.designation, False))

The rule class legend.

name: str = 'PossibilityNegatedUndesignated'

The rule class name.

negated: bool | None = True

operator: Operator | None = (90, 1)

predicate: Predicate | None = None

quantifier: Quantifier | None = None

timer_names: Sequence[str] = qsetf({'search', 'apply'})

StopWatch names to create in timers mapping.

class PossibilityUndesignated(tableau, /, **opts)

◇⊖

◇A ⊖, w₀

w₀Rw₁

⋮

A ⊖, w₁

Parameters:

tableau (Tableau) --

Helpers: Mapping[type[Rule.Helper], Any] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=False)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Possibility>}), pred=(<NodeDesignation:(designated=False)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Possibility>), ignore_ticked=True), <class 'pytableaux.proof.helpers.QuitFlag'>: None, <class 'pytableaux.proof.helpers.MaxWorlds'>: Config(operators=qsetf({<Operator: Possibility>, <Operator: Necessity>})), <class 'pytableaux.proof.helpers.NodeCount'>: None, <class 'pytableaux.proof.helpers.NodesWorlds'>: None, <class 'pytableaux.proof.helpers.WorldIndex'>: None})

Helper classes mapped to their settings.

NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}

branching: int = 0

The number of additional branches created.

defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})

designation: bool | None = False

legend: tuple[tuple[str, Any], ...] = ((Legend.operator, Operator.Possibility), (Legend.designation, False))

The rule class legend.

name: str = 'PossibilityUndesignated'

The rule class name.

negated: bool | None = None

operator: Operator | None = (90, 1)

predicate: Predicate | None = None

quantifier: Quantifier | None = None

timer_names: Sequence[str] = qsetf({'search', 'apply'})

StopWatch names to create in timers mapping.

class NecessityNegatedDesignated(tableau, /, **opts)

¬◻⊕

¬◻A ⊕, w₀

⋮

◇¬A ⊕, w₀

Parameters:

tableau (Tableau) --

Helpers: Mapping[type[Rule.Helper], Any] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=True)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Necessity(negated)>}), pred=(<NodeDesignation:(designated=True)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Necessity(negated)>), ignore_ticked=True)})

Helper classes mapped to their settings.

NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}

branching: int = 0

The number of additional branches created.

defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})

designation: bool | None = True

legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.Necessity), (Legend.designation, True))

The rule class legend.

name: str = 'NecessityNegatedDesignated'

The rule class name.

negated: bool | None = True

operator: Operator | None = (100, 1)

predicate: Predicate | None = None

quantifier: Quantifier | None = None

timer_names: Sequence[str] = qsetf({'search', 'apply'})

StopWatch names to create in timers mapping.

class NecessityUndesignated(tableau, /, **opts)

◻⊖

◻A ⊖, w₀

⋮

A ⊖, w₁

w₀Rw₁

Parameters:

tableau (Tableau) --

Helpers: Mapping[type[Rule.Helper], Any] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=False)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Necessity>}), pred=(<NodeDesignation:(designated=False)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Necessity>), ignore_ticked=True), <class 'pytableaux.proof.helpers.QuitFlag'>: None, <class 'pytableaux.proof.helpers.MaxWorlds'>: Config(operators=qsetf({<Operator: Possibility>, <Operator: Necessity>})), <class 'pytableaux.proof.helpers.AplSentCount'>: None})

Helper classes mapped to their settings.

NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}

branching: int = 0

The number of additional branches created.

defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})

designation: bool | None = False

legend: tuple[tuple[str, Any], ...] = ((Legend.operator, Operator.Necessity), (Legend.designation, False))

The rule class legend.

name: str = 'NecessityUndesignated'

The rule class name.

negated: bool | None = None

operator: Operator | None = (100, 1)

predicate: Predicate | None = None

quantifier: Quantifier | None = None

timer_names: Sequence[str] = qsetf({'search', 'apply'})

StopWatch names to create in timers mapping.

class NecessityNegatedUndesignated(tableau, /, **opts)

¬◻⊖

¬◻A ⊖, w₀

⋮

◇¬A ⊖, w₀

Parameters:

tableau (Tableau) --

Helpers: Mapping[type[Rule.Helper], Any] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=False)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Necessity(negated)>}), pred=(<NodeDesignation:(designated=False)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Necessity(negated)>), ignore_ticked=True)})

Helper classes mapped to their settings.

NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}

branching: int = 0

The number of additional branches created.

defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})

designation: bool | None = False

legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.Necessity), (Legend.designation, False))

The rule class legend.

name: str = 'NecessityNegatedUndesignated'

The rule class name.

negated: bool | None = True

operator: Operator | None = (100, 1)

predicate: Predicate | None = None

quantifier: Quantifier | None = None

timer_names: Sequence[str] = qsetf({'search', 'apply'})

StopWatch names to create in timers mapping.

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