K - Kripke Normal Modal Logic

K is the foundation of so-called normal modal logics. It adds modal operators ◻ and ◇ to CFOL.

---

Semantics

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

Truth Values

Common labels for the values include:

T	1	true
F	0	false

Truth Tables

The value of a sentence with a truth-functional operator is determined by the values of its operands according to the following tables.

Negation
	¬
T	F
F	T

Conjunction
∧	T	F
T	T	F
F	F	F

Disjunction
∨	T	F
T	T	T
F	T	F

Defined Operators

The Material Conditional ⊃ is definable in terms of disjunction:

A ⊃ B \(:=\) ¬A ∨ B

Likewise the Material Biconditional ≡ is defined in terms of ⊃ and ∧:

A ≡ B \(:=\) (A ⊃ B) ∧ (B ⊃ A)

Material Conditional
⊃	T	F
T	T	F
F	T	T

Material Biconditional
≡	T	F
T	T	F
F	F	T

Compatibility Tables

K does not have separate Assertion or Conditional operators, but we include tables and rules for them, for cross-compatibility.

Assertion
	⚬
T	T
F	F

Conditional
→	T	F
T	T	F
F	T	T

Biconditional
↔	T	F
T	T	F
F	F	T

Predication

The value of predicated sentences are handled in terms of a predicate's extension.

A sentence with n-ary predicate \(P\) over parameters \(\langle a_0, ... ,a_n\rangle\) has the value T iff \(\langle a_0, ... ,a_n\rangle\) is in the extension of \(P\).

Quantification

Existential

An existential sentence is true just when the sentence resulting in the subsitution of some constant in the domain for the variable is true.

Universal

A universal sentence is true just when the sentence resulting in the subsitution of each constant in the domain for the variable is true.

Modal Operators

Possibility

A possibility sentence is true at \(w\) iff its operand is true at \(w'\) for some \(w'\) such that \(\langle\ w, w'\ \rangle\) in the access relation.

Necessity

A necessity sentence ◻A is true at \(w\) iff its operand A is true at \(w'\) for each \(w'\) such that \(\langle\ w, w'\ \rangle\) is in the access relation.

Consequence

Logical Consequence is defined similary as CPL, except with reference to a world:

Logical Consequence

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

Tableaux

Nodes

Nodes for bivalent modal tableaux come in two types:

• A sentence-world pair like \(A, w\), indicating that \(A\) is true at \(w\).

• 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 node with each premise, with world \(w_0\), followed by a node with the negation of the conclusion with world \(w_0\).

To build the trunk for the argument A₁ ... A_n ∴ B write:

A₁, w₀

⋮

A_n, w₀

¬B, w₀

Closure

⊗Contradiction Closure

A, w₀

⋮

¬A, w₀

⊗

⊗¬=Self Identity Closure

⋮

a ≠ a, w₀

⊗

⊗¬E!Non Existence Closure

⋮

¬E!a, w₀

⊗

Rules

In general, rules for connectives consist of two rules per connective: a plain rule, and a negated rule. The special case of negation only one rule for double negation.

There is also a special rule for the Identity predicate.

Additional rules are given for the quantifiers.

Operator Rules

¬ Rules

¬¬Double Negation

¬¬A, w₀

⋮

A, w₀

∧ Rules

∧Conjunction

A ∧ B, w₀

⋮

A, w₀

B, w₀

¬∧Conjunction Negated

¬(A ∧ B), w₀

⋮

¬A, w₀

¬B, w₀

∨ Rules

∨Disjunction

A ∨ B, w₀

⋮

A, w₀

B, w₀

¬∨Disjunction Negated

¬(A ∨ B), w₀

⋮

¬A, w₀

¬B, w₀

⊃ Rules

⊃Material Conditional

A ⊃ B, w₀

⋮

¬A, w₀

B, w₀

¬⊃Material Conditional Negated

¬(A ⊃ B), w₀

⋮

A, w₀

¬B, w₀

≡ Rules

≡Material Biconditional

A ≡ B, w₀

⋮

¬A, w₀

¬B, w₀

B, w₀

A, w₀

¬≡Material Biconditional Negated

¬(A ≡ B), w₀

⋮

A, w₀

¬B, w₀

¬A, w₀

B, w₀

Modal Operator Rules

◇ Rules

◇Possibility

◇A, w₀

⋮

A, w₁

w₀Rw₁

¬◇Possibility Negated

¬◇A, w₀

⋮

◻¬A, w₀

◻ Rules

◻Necessity

◻A, w₀

w₀Rw₁

⋮

A, w₁

¬◻Necessity Negated

¬◻A, w₀

⋮

◇¬A, w₀

Predicate Rules

= Rules

=Identity Indiscernability

Fa, w₀

a = b, w₀

⋮

Fb, w₀

Quantifier Rules

∃ Rules

∃Existential

∃xFx, w₀

⋮

Fa, w₀

¬∃Existential Negated

¬∃xFx, w₀

⋮

∀x¬Fx, w₀

∀ Rules

∀Universal

∀xFx, w₀

⋮

Fa, w₀

¬∀Universal Negated

¬∀xFx, w₀

⋮

∃x¬Fx, w₀

Compatibility Rules

⚬ Rules

⚬Assertion

⚬A, w₀

⋮

A, w₀

¬⚬Assertion Negated

¬⚬A, w₀

⋮

¬A, w₀

→ Rules

→Conditional

A → B, w₀

⋮

¬A, w₀

B, w₀

¬→Conditional Negated

¬(A → B), w₀

⋮

A, w₀

¬B, w₀

↔ Rules

↔Biconditional

A ↔ B, w₀

⋮

¬A, w₀

¬B, w₀

B, w₀

A, w₀

¬↔Biconditional Negated

¬(A ↔ B), w₀

⋮

A, w₀

¬B, w₀

¬A, w₀

B, w₀

Notes

References

Futher Reading

• Stanford Encyclopedia on Modal Logic

class Rules

class ContradictionClosure(tableau, /, **opts)

⊗

A, w₀

⋮

¬A, w₀

⊗

A branch closes when a sentence and its negation both appear on a node with the same world on the branch.

Parameters:

tableau (Tableau) --

example_nodes()

Helpers: Mapping[type[Rule.Helper], Any] = mappingproxy({<class 'pytableaux.proof.helpers.BranchTarget'>: None})

Helper classes mapped to their settings.

branching: int = 0

The number of additional branches created.

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

legend: tuple[tuple[str, Any], ...] = ((Legend.closure, True),)

The rule class legend.

name: str = 'ContradictionClosure'

The rule class name.

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

StopWatch names to create in timers mapping.

class SelfIdentityClosure(tableau, /, **opts)

⊗¬=

⋮

a ≠ a, w₀

⊗

A branch closes when a sentence of the form a ≠ a appears on the branch at any world.

Parameters:

tableau (Tableau) --

negated: bool | None = True

predicate: Predicate | None = <Predicate: Identity>

node_will_close_branch(node, branch, /)

Return type:

bool

example_nodes()

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.NodeSentence'>: <NodeSentence:predicate=Identity(negated)>}), pred=(<NodeSentence:predicate=Identity(negated)>,), ignore_ticked=True), <class 'pytableaux.proof.helpers.PredNodes'>: Config(ignore_ticked=True), <class 'pytableaux.proof.helpers.BranchTarget'>: None})

Helper classes mapped to their settings.

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

branching: int = 0

The number of additional branches created.

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

legend: tuple[tuple[str, Any], ...] = ((Legend.closure, True), (Legend.negated, Operator.Negation), (Legend.predicate, <Predicate: Identity>))

The rule class legend.

name: str = 'SelfIdentityClosure'

The rule class name.

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

StopWatch names to create in timers mapping.

class NonExistenceClosure(tableau, /, **opts)

⊗¬E!

⋮

¬E!a, w₀

⊗

A branch closes when a sentence of the form ¬E!a appears on the branch at any world.

Parameters:

tableau (Tableau) --

negated: bool | None = True

predicate: Predicate | None = <Predicate: Existence>

node_will_close_branch(node, branch, /)

example_nodes()

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.NodeSentence'>: <NodeSentence:predicate=Existence(negated)>}), pred=(<NodeSentence:predicate=Existence(negated)>,), ignore_ticked=True), <class 'pytableaux.proof.helpers.PredNodes'>: Config(ignore_ticked=True), <class 'pytableaux.proof.helpers.BranchTarget'>: None})

Helper classes mapped to their settings.

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

branching: int = 0

The number of additional branches created.

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

legend: tuple[tuple[str, Any], ...] = ((Legend.closure, True), (Legend.negated, Operator.Negation), (Legend.predicate, <Predicate: Existence>))

The rule class legend.

name: str = 'NonExistenceClosure'

The rule class name.

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

StopWatch names to create in timers mapping.

class DoubleNegation(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:()>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Negation(negated)>}), pred=(<NodeDesignation:()>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Negation(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 = None

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

The rule class legend.

name: str = 'DoubleNegation'

The rule class name.

negated: bool | None = True

operator: Operator | None = (20, 1)

predicate: Predicate | None = None

quantifier: Quantifier | None = None

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

StopWatch names to create in timers mapping.

class Assertion(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:()>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Assertion>}), pred=(<NodeDesignation:()>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Assertion>), 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 = None

legend: tuple[tuple[str, Any], ...] = ((Legend.operator, Operator.Assertion),)

The rule class legend.

name: str = 'Assertion'

The rule class name.

negated: bool | None = None

operator: Operator | None = (10, 1)

predicate: Predicate | None = None

quantifier: Quantifier | None = None

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

StopWatch names to create in timers mapping.

class AssertionNegated(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:()>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Assertion(negated)>}), pred=(<NodeDesignation:()>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Assertion(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 = None

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

The rule class legend.

name: str = 'AssertionNegated'

The rule class name.

negated: bool | None = True

operator: Operator | None = (10, 1)

predicate: Predicate | None = None

quantifier: Quantifier | None = None

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

StopWatch names to create in timers mapping.

class Conjunction(tableau, /, **opts)

∧

A ∧ B, w₀

⋮

A, w₀

B, 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:()>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Conjunction>}), pred=(<NodeDesignation:()>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Conjunction>), 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 = None

legend: tuple[tuple[str, Any], ...] = ((Legend.operator, Operator.Conjunction),)

The rule class legend.

name: str = 'Conjunction'

The rule class name.

negated: bool | None = None

operator: Operator | None = (30, 2)

predicate: Predicate | None = None

quantifier: Quantifier | None = None

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

StopWatch names to create in timers mapping.

class ConjunctionNegated(tableau, /, **opts)

¬∧

¬(A ∧ B), w₀

⋮

¬A, w₀

¬B, 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:()>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Conjunction(negated)>}), pred=(<NodeDesignation:()>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Conjunction(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 = 1

The number of additional branches created.

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

designation: bool | None = None

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

The rule class legend.

name: str = 'ConjunctionNegated'

The rule class name.

negated: bool | None = True

operator: Operator | None = (30, 2)

predicate: Predicate | None = None

quantifier: Quantifier | None = None

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

StopWatch names to create in timers mapping.

class Disjunction(tableau, /, **opts)

∨

A ∨ B, w₀

⋮

A, w₀

B, 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:()>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Disjunction>}), pred=(<NodeDesignation:()>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Disjunction>), 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 = 1

The number of additional branches created.

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

designation: bool | None = None

legend: tuple[tuple[str, Any], ...] = ((Legend.operator, Operator.Disjunction),)

The rule class legend.

name: str = 'Disjunction'

The rule class name.

negated: bool | None = None

operator: Operator | None = (40, 2)

predicate: Predicate | None = None

quantifier: Quantifier | None = None

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

StopWatch names to create in timers mapping.

class DisjunctionNegated(tableau, /, **opts)

¬∨

¬(A ∨ B), w₀

⋮

¬A, w₀

¬B, 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:()>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Disjunction(negated)>}), pred=(<NodeDesignation:()>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Disjunction(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 = None

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

The rule class legend.

name: str = 'DisjunctionNegated'

The rule class name.

negated: bool | None = True

operator: Operator | None = (40, 2)

predicate: Predicate | None = None

quantifier: Quantifier | None = None

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

StopWatch names to create in timers mapping.

class MaterialConditional(tableau, /, **opts)

⊃

A ⊃ B, w₀

⋮

¬A, w₀

B, 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:()>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=MaterialConditional>}), pred=(<NodeDesignation:()>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=MaterialConditional>), 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 = 1

The number of additional branches created.

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

designation: bool | None = None

legend: tuple[tuple[str, Any], ...] = ((Legend.operator, Operator.MaterialConditional),)

The rule class legend.

name: str = 'MaterialConditional'

The rule class name.

negated: bool | None = None

operator: Operator | None = (50, 2)

predicate: Predicate | None = None

quantifier: Quantifier | None = None

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

StopWatch names to create in timers mapping.

class MaterialConditionalNegated(tableau, /, **opts)

¬⊃

¬(A ⊃ B), w₀

⋮

A, w₀

¬B, 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:()>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=MaterialConditional(negated)>}), pred=(<NodeDesignation:()>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=MaterialConditional(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 = None

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

The rule class legend.

name: str = 'MaterialConditionalNegated'

The rule class name.

negated: bool | None = True

operator: Operator | None = (50, 2)

predicate: Predicate | None = None

quantifier: Quantifier | None = None

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

StopWatch names to create in timers mapping.

class MaterialBiconditional(tableau, /, **opts)

≡

A ≡ B, w₀

⋮

¬A, w₀

¬B, w₀

B, 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:()>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=MaterialBiconditional>}), pred=(<NodeDesignation:()>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=MaterialBiconditional>), 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 = 1

The number of additional branches created.

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

designation: bool | None = None

legend: tuple[tuple[str, Any], ...] = ((Legend.operator, Operator.MaterialBiconditional),)

The rule class legend.

name: str = 'MaterialBiconditional'

The rule class name.

negated: bool | None = None

operator: Operator | None = (60, 2)

predicate: Predicate | None = None

quantifier: Quantifier | None = None

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

StopWatch names to create in timers mapping.

class MaterialBiconditionalNegated(tableau, /, **opts)

¬≡

¬(A ≡ B), w₀

⋮

A, w₀

¬B, w₀

¬A, w₀

B, 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:()>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=MaterialBiconditional(negated)>}), pred=(<NodeDesignation:()>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=MaterialBiconditional(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 = 1

The number of additional branches created.

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

designation: bool | None = None

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

The rule class legend.

name: str = 'MaterialBiconditionalNegated'

The rule class name.

negated: bool | None = True

operator: Operator | None = (60, 2)

predicate: Predicate | None = None

quantifier: Quantifier | None = None

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

StopWatch names to create in timers mapping.

class Conditional(tableau, /, **opts)

→

A → B, w₀

⋮

¬A, w₀

B, 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:()>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Conditional>}), pred=(<NodeDesignation:()>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Conditional>), 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 = 1

The number of additional branches created.

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

designation: bool | None = None

legend: tuple[tuple[str, Any], ...] = ((Legend.operator, Operator.Conditional),)

The rule class legend.

name: str = 'Conditional'

The rule class name.

negated: bool | None = None

operator: Operator | None = (70, 2)

predicate: Predicate | None = None

quantifier: Quantifier | None = None

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

StopWatch names to create in timers mapping.

class ConditionalNegated(tableau, /, **opts)

¬→

¬(A → B), w₀

⋮

A, w₀

¬B, 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:()>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Conditional(negated)>}), pred=(<NodeDesignation:()>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Conditional(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 = None

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

The rule class legend.

name: str = 'ConditionalNegated'

The rule class name.

negated: bool | None = True

operator: Operator | None = (70, 2)

predicate: Predicate | None = None

quantifier: Quantifier | None = None

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

StopWatch names to create in timers mapping.

class Biconditional(tableau, /, **opts)

↔

A ↔ B, w₀

⋮

¬A, w₀

¬B, w₀

B, 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:()>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Biconditional>}), pred=(<NodeDesignation:()>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Biconditional>), 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 = 1

The number of additional branches created.

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

designation: bool | None = None

legend: tuple[tuple[str, Any], ...] = ((Legend.operator, Operator.Biconditional),)

The rule class legend.

name: str = 'Biconditional'

The rule class name.

negated: bool | None = None

operator: Operator | None = (80, 2)

predicate: Predicate | None = None

quantifier: Quantifier | None = None

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

StopWatch names to create in timers mapping.

class BiconditionalNegated(tableau, /, **opts)

¬↔

¬(A ↔ B), w₀

⋮

A, w₀

¬B, w₀

¬A, w₀

B, 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:()>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Biconditional(negated)>}), pred=(<NodeDesignation:()>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Biconditional(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 = 1

The number of additional branches created.

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

designation: bool | None = None

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

The rule class legend.

name: str = 'BiconditionalNegated'

The rule class name.

negated: bool | None = True

operator: Operator | None = (80, 2)

predicate: Predicate | None = None

quantifier: Quantifier | None = None

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

StopWatch names to create in timers mapping.

class Existential(tableau, /, **opts)

∃

∃xFx, w₀

⋮

Fa, 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:()>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:quantifier=Existential>}), pred=(<NodeDesignation:()>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:quantifier=Existential>), ignore_ticked=True), <class 'pytableaux.proof.helpers.QuitFlag'>: None, <class 'pytableaux.proof.helpers.MaxConsts'>: 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 = None

legend: tuple[tuple[str, Any], ...] = ((Legend.quantifier, Quantifier.Existential),)

The rule class legend.

name: str = 'Existential'

The rule class name.

negated: bool | None = None

operator: Operator | None = None

predicate: Predicate | None = None

quantifier: Quantifier | None = 0

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

StopWatch names to create in timers mapping.

class ExistentialNegated(tableau, /, **opts)

¬∃

¬∃xFx, w₀

⋮

∀x¬Fx, 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:()>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:quantifier=Existential(negated)>}), pred=(<NodeDesignation:()>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:quantifier=Existential(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 = None

legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.quantifier, Quantifier.Existential))

The rule class legend.

name: str = 'ExistentialNegated'

The rule class name.

negated: bool | None = True

operator: Operator | None = None

predicate: Predicate | None = None

quantifier: Quantifier | None = 0

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

StopWatch names to create in timers mapping.

class Universal(tableau, /, **opts)

∀

∀xFx, w₀

⋮

Fa, 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:()>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:quantifier=Universal>}), pred=(<NodeDesignation:()>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:quantifier=Universal>), ignore_ticked=True), <class 'pytableaux.proof.helpers.QuitFlag'>: None, <class 'pytableaux.proof.helpers.MaxConsts'>: None, <class 'pytableaux.proof.helpers.NodeConsts'>: None, <class 'pytableaux.proof.helpers.NodeCount'>: 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 = None

legend: tuple[tuple[str, Any], ...] = ((Legend.quantifier, Quantifier.Universal),)

The rule class legend.

name: str = 'Universal'

The rule class name.

negated: bool | None = None

operator: Operator | None = None

predicate: Predicate | None = None

quantifier: Quantifier | None = 1

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

StopWatch names to create in timers mapping.

class UniversalNegated(tableau, /, **opts)

¬∀

¬∀xFx, w₀

⋮

∃x¬Fx, 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:()>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:quantifier=Universal(negated)>}), pred=(<NodeDesignation:()>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:quantifier=Universal(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 = None

legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.quantifier, Quantifier.Universal))

The rule class legend.

name: str = 'UniversalNegated'

The rule class name.

negated: bool | None = True

operator: Operator | None = None

predicate: Predicate | None = None

quantifier: Quantifier | None = 1

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

StopWatch names to create in timers mapping.

class Possibility(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:()>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Possibility>}), pred=(<NodeDesignation:()>, <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.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 = None

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

The rule class legend.

name: str = 'Possibility'

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 PossibilityNegated(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:()>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Possibility(negated)>}), pred=(<NodeDesignation:()>, <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 = None

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

The rule class legend.

name: str = 'PossibilityNegated'

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 Necessity(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:()>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Necessity>}), pred=(<NodeDesignation:()>, <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.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 = None

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

The rule class legend.

name: str = 'Necessity'

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 NecessityNegated(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:()>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Necessity(negated)>}), pred=(<NodeDesignation:()>, <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 = None

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

The rule class legend.

name: str = 'NecessityNegated'

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 IdentityIndiscernability(tableau, /, **opts)

=

Fa, w₀

a = b, w₀

⋮

Fb, w₀

From an unticked node n having an Identity sentence s at world w on an open branch b, and a predicated node n' whose sentence s' has a constant that is a parameter of s, if the replacement of that constant for the other constant of s is a sentence that does not appear on b at w, then add it.

Parameters:

tableau (Tableau) --

ticking: bool = False

Whether this is a ticking rule.

predicate: Predicate | None = <Predicate: Identity>

example_nodes()

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:()>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:predicate=Identity>}), pred=(<NodeDesignation:()>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:predicate=Identity>), ignore_ticked=True), <class 'pytableaux.proof.helpers.PredNodes'>: Config(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})

legend: tuple[tuple[str, Any], ...] = ((Legend.predicate, <Predicate: Identity>),)

The rule class legend.

name: str = 'IdentityIndiscernability'

The rule class name.

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

StopWatch names to create in timers mapping.

closure: tuple[type[ClosingRule], ...] = (<class 'pytableaux.logics.k.Rules.ContradictionClosure'>, <class 'pytableaux.logics.k.Rules.SelfIdentityClosure'>, <class 'pytableaux.logics.k.Rules.NonExistenceClosure'>)

groups: tuple[tuple[type[Rule], ...], ...] = ((<class 'pytableaux.logics.k.Rules.IdentityIndiscernability'>, <class 'pytableaux.logics.k.Rules.Assertion'>, <class 'pytableaux.logics.k.Rules.AssertionNegated'>, <class 'pytableaux.logics.k.Rules.Conjunction'>, <class 'pytableaux.logics.k.Rules.DisjunctionNegated'>, <class 'pytableaux.logics.k.Rules.MaterialConditionalNegated'>, <class 'pytableaux.logics.k.Rules.ConditionalNegated'>, <class 'pytableaux.logics.k.Rules.DoubleNegation'>, <class 'pytableaux.logics.k.Rules.PossibilityNegated'>, <class 'pytableaux.logics.k.Rules.NecessityNegated'>, <class 'pytableaux.logics.k.Rules.ExistentialNegated'>, <class 'pytableaux.logics.k.Rules.UniversalNegated'>), (<class 'pytableaux.logics.k.Rules.ConjunctionNegated'>, <class 'pytableaux.logics.k.Rules.Disjunction'>, <class 'pytableaux.logics.k.Rules.MaterialConditional'>, <class 'pytableaux.logics.k.Rules.MaterialBiconditional'>, <class 'pytableaux.logics.k.Rules.MaterialBiconditionalNegated'>, <class 'pytableaux.logics.k.Rules.Conditional'>, <class 'pytableaux.logics.k.Rules.Biconditional'>, <class 'pytableaux.logics.k.Rules.BiconditionalNegated'>), (<class 'pytableaux.logics.k.Rules.Necessity'>, <class 'pytableaux.logics.k.Rules.Possibility'>), (<class 'pytableaux.logics.k.Rules.Existential'>, <class 'pytableaux.logics.k.Rules.Universal'>))