FDE - First Degree Entailment
FDE is a 4-valued relevance logic logic with values T, F, N and B.
Semantics
Truth Values
Common labels for the values include:
T |
1 |
just true |
N |
0.25 |
neither true nor false |
B |
0.75 |
both true and false |
F |
0 |
just false |
Designated Values
The set of designated values for FDE is: { T, B }
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 | |||
| B | B | |||
| N | N | |||
| F | T | |||
| Conjunction | ||||
|---|---|---|---|---|
| ∧ | T | B | N | F |
| T | T | B | N | F |
| B | B | B | N | F |
| N | N | N | N | F |
| F | F | F | F | F |
| Disjunction | ||||
|---|---|---|---|---|
| ∨ | T | B | N | F |
| T | T | T | T | T |
| B | T | B | B | B |
| N | T | B | N | N |
| F | T | B | N | 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 | B | N | F |
| T | T | B | N | F |
| B | T | B | B | B |
| N | T | B | N | N |
| F | T | T | T | T |
| Material Biconditional | ||||
|---|---|---|---|---|
| ≡ | T | B | N | F |
| T | T | B | N | F |
| B | B | B | B | B |
| N | N | B | N | N |
| F | F | B | N | T |
Compatibility Tables
FDE does not have separate Assertion or Conditional operators, but we include tables and rules for them, for cross-compatibility.
| Assertion | ||||
|---|---|---|---|---|
| ⚬ | ||||
| T | T | |||
| B | B | |||
| N | N | |||
| F | F | |||
| Conditional | ||||
|---|---|---|---|---|
| → | T | B | N | F |
| T | T | B | N | F |
| B | T | B | B | B |
| N | T | B | N | N |
| F | T | T | T | T |
| Biconditional | ||||
|---|---|---|---|---|
| ↔ | T | B | N | F |
| T | T | B | N | F |
| B | B | B | B | B |
| N | N | B | N | N |
| F | F | B | N | T |
Predication
Predicated sentences in a model are interpreted via a predicate's extension and anti-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\) and not in the anti-extension of \(P\).
F iff \(\langle a_0, ... ,a_n\rangle\) is in the anti-extension of \(P\) and not in the extension of \(P\).
B iff \(\langle a_0, ... ,a_n\rangle\) is in both the extension and anti-extension of \(P\).
N iff \(\langle a_0, ... ,a_n\rangle\) is in neither in the extension nor the anti-extension of \(P\).
Note, for FDE, there is no exclusivity nor exhaustion constraint on a predicate's extension and anti-extension. This means that \(\langle a_0, ... ,a_n\rangle\) could be in neither the extension nor the anti-extension of a predicate, or it could be in both the extension and the anti-extension.
Quantification
Existential
The value of an existential sentence is the maximum value of the sentences that result from replacing each constant for the quantified variable. The ordering of the values from least to greatest is: F, N, B, T.
Universal
The value of an universal sentence is the minimum value of the sentences that result from replacing each constant for the quantified variable. The ordering of the values from least to greatest is: F, N, B, T.
Consequence
Logical Consequence is defined in terms of the set of designated values T, B:
Logical Consequence
C is a Logical Consequence of A iff all models where A has a desginated value are models where C also has a designated value.
Tableaux
Nodes
Nodes for many-value tableaux consiste of a sentence plus a designation marker: ⊕ for designated, and ⊖ for undesignated.
Trunk
To build the trunk for an argument, add a designated node for each premise, and an undesignated node for the conclusion.
To build the trunk for the argument A1 ... An ∴ B write:
A1 ⊕
⋮
An ⊕
B ⊖
Closure
A branch is closed iff the same sentence appears on both a designated node, and undesignated node.
This allows for both a sentence and its negation to appear as designated on an open branch (or both as undesignated).
Rules
In general, rules for connectives consist of four rules per connective: a designated rule, an undesignated rule, a negated designated rule, and a negated undesignated rule. The special case of negation has a total of two rules which apply to double negation only, one designated rule, and one undesignated rule.
Operator Rules
¬ Rules
∧ Rules
∨ Rules
⊃ Rules
≡ Rules
Quantifier Rules
∃ Rules
∀ Rules
Compatibility Rules
⚬ Rules
→ Rules
↔ Rules
Notes
Some notable features of FDE include:
No logical truths. The means that the Law of Excluded Middle A ∨ ¬A, and the Law of Non-Contradiction ¬(A ∧ ¬A) fail, as well as Conditional Identity A → A.
Failure of Modus Ponens, Modus Tollens, Disjunctive Syllogism, and other Classical validities.
DeMorgan laws are valid, as well as Conditional Contraction (A → (A → B) ⊢ A → B).
References
Beall, Jc, et al. Possibilities and Paradox: An Introduction to Modal and Many-valued Logic. United Kingdom, Oxford University Press, 2003.
Priest, Graham. An Introduction to Non-Classical Logic: From If to Is. Cambridge University Press, 2008.
For futher reading see:
Anderson, A., Belnap, N. D., et al. Entailment: The Logic of Relevance and Necessity. United Kingdom, Princeton University Press, 1975.
Belnap, N. D., McRobbie, M. A. Relevant Analytic Tableaux. Studia Logica, Vol. 38, No. 2, 1979.
Stanford Encyclopedia on Paraconsistent Logic and Relevance Logic.
- class Rules[source]
- class DesignationClosure(tableau, /, **opts)[source]
- ⊗A ⊕⋮A ⊖⊗
A branch closes when a sentence appears on a node marked designated, and the same sentence appears on a node marked undesignated.
- Parameters:
tableau (Tableau) --
- Helpers: Mapping[type[Rule.Helper], Any] = mappingproxy({<class 'pytableaux.proof.helpers.BranchTarget'>: None})
Helper classes mapped to their settings.
- defaults = mappingproxy({'is_rank_optim': False, 'nolock': False})
- class DoubleNegationDesignated(tableau, /, **opts)[source]
- ¬¬⊕¬¬A ⊕⋮A ⊕
- 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=Negation(negated)>}), pred=(<NodeDesignation:(designated=True)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.Negation), (Legend.designation, True))
The rule class legend.
- quantifier: Quantifier | None = None
- class DoubleNegationUndesignated(tableau, /, **opts)[source]
- ¬¬⊖¬¬A ⊖⋮A ⊖
- 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=Negation(negated)>}), pred=(<NodeDesignation:(designated=False)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.Negation), (Legend.designation, False))
The rule class legend.
- quantifier: Quantifier | None = None
- class AssertionDesignated(tableau, /, **opts)[source]
- ⚬⊕⚬A ⊕⋮A ⊕
- 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=Assertion>}), pred=(<NodeDesignation:(designated=True)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.operator, Operator.Assertion), (Legend.designation, True))
The rule class legend.
- quantifier: Quantifier | None = None
- class AssertionUndesignated(tableau, /, **opts)[source]
- ⚬⊖⚬A ⊖⋮A ⊖
- 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=Assertion>}), pred=(<NodeDesignation:(designated=False)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.operator, Operator.Assertion), (Legend.designation, False))
The rule class legend.
- quantifier: Quantifier | None = None
- class AssertionNegatedDesignated(tableau, /, **opts)[source]
- ¬⚬⊕¬⚬A ⊕⋮¬A ⊕
- 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=Assertion(negated)>}), pred=(<NodeDesignation:(designated=True)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.Assertion), (Legend.designation, True))
The rule class legend.
- quantifier: Quantifier | None = None
- class AssertionNegatedUndesignated(tableau, /, **opts)[source]
- ¬⚬⊖¬⚬A ⊖⋮¬A ⊖
- 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=Assertion(negated)>}), pred=(<NodeDesignation:(designated=False)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.Assertion), (Legend.designation, False))
The rule class legend.
- quantifier: Quantifier | None = None
- class ConjunctionDesignated(tableau, /, **opts)[source]
- ∧⊕A ∧ B ⊕⋮A ⊕B ⊕
- 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=Conjunction>}), pred=(<NodeDesignation:(designated=True)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.operator, Operator.Conjunction), (Legend.designation, True))
The rule class legend.
- quantifier: Quantifier | None = None
- class ConjunctionUndesignated(tableau, /, **opts)[source]
- ∧⊖A ∧ B ⊖⋮A ⊖B ⊖
- 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=Conjunction>}), pred=(<NodeDesignation:(designated=False)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.operator, Operator.Conjunction), (Legend.designation, False))
The rule class legend.
- quantifier: Quantifier | None = None
- class ConjunctionNegatedDesignated(tableau, /, **opts)[source]
- ¬∧⊕¬(A ∧ B) ⊕⋮¬A ⊕¬B ⊕
- 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=Conjunction(negated)>}), pred=(<NodeDesignation:(designated=True)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.Conjunction), (Legend.designation, True))
The rule class legend.
- quantifier: Quantifier | None = None
- class ConjunctionNegatedUndesignated(tableau, /, **opts)[source]
- ¬∧⊖¬(A ∧ B) ⊖⋮¬A ⊖¬B ⊖
- 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=Conjunction(negated)>}), pred=(<NodeDesignation:(designated=False)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.Conjunction), (Legend.designation, False))
The rule class legend.
- quantifier: Quantifier | None = None
- class DisjunctionDesignated(tableau, /, **opts)[source]
- ∨⊕A ∨ B ⊕⋮A ⊕B ⊕
- 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=Disjunction>}), pred=(<NodeDesignation:(designated=True)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.operator, Operator.Disjunction), (Legend.designation, True))
The rule class legend.
- quantifier: Quantifier | None = None
- class DisjunctionNegatedDesignated(tableau, /, **opts)[source]
- ¬∨⊕¬(A ∨ B) ⊕⋮¬A ⊕¬B ⊕
- 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=Disjunction(negated)>}), pred=(<NodeDesignation:(designated=True)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.Disjunction), (Legend.designation, True))
The rule class legend.
- quantifier: Quantifier | None = None
- class DisjunctionUndesignated(tableau, /, **opts)[source]
- ∨⊖A ∨ B ⊖⋮A ⊖B ⊖
- 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=Disjunction>}), pred=(<NodeDesignation:(designated=False)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.operator, Operator.Disjunction), (Legend.designation, False))
The rule class legend.
- quantifier: Quantifier | None = None
- class DisjunctionNegatedUndesignated(tableau, /, **opts)[source]
- ¬∨⊖¬(A ∨ B) ⊖⋮¬A ⊖¬B ⊖
- 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=Disjunction(negated)>}), pred=(<NodeDesignation:(designated=False)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.Disjunction), (Legend.designation, False))
The rule class legend.
- quantifier: Quantifier | None = None
- class MaterialConditionalDesignated(tableau, /, **opts)[source]
- ⊃⊕A ⊃ B ⊕⋮¬A ⊕B ⊕
From an unticked designated material conditional node n on a branch b, make two new branches b' and b'' from b, add a designated node with the negation of the antecedent to b', add a designated node with the consequent to b'', then tick n.
- 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=MaterialConditional>}), pred=(<NodeDesignation:(designated=True)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.operator, Operator.MaterialConditional), (Legend.designation, True))
The rule class legend.
- quantifier: Quantifier | None = None
- class MaterialConditionalNegatedDesignated(tableau, /, **opts)[source]
- ¬⊃⊕¬(A ⊃ B) ⊕⋮A ⊕¬B ⊕
From an unticked designated negated material conditional node n on a branch b, add a designated node with the antecedent, and a designated node with the negation of the consequent to b, then tick n.
- 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=MaterialConditional(negated)>}), pred=(<NodeDesignation:(designated=True)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.MaterialConditional), (Legend.designation, True))
The rule class legend.
- quantifier: Quantifier | None = None
- class MaterialConditionalUndesignated(tableau, /, **opts)[source]
- ⊃⊖A ⊃ B ⊖⋮¬A ⊖B ⊖
From an unticked undesignated material conditional node n on a branch b, add an undesignated node with the negation of the antecedent and an undesignated node with the consequent to b, then tick n.
- 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=MaterialConditional>}), pred=(<NodeDesignation:(designated=False)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.operator, Operator.MaterialConditional), (Legend.designation, False))
The rule class legend.
- quantifier: Quantifier | None = None
- class MaterialConditionalNegatedUndesignated(tableau, /, **opts)[source]
- ¬⊃⊖¬(A ⊃ B) ⊖⋮A ⊖¬B ⊖
From an unticked undesignated negated material conditional node n on a branch b, make two new branches b' and b'' from b, add an undesignated node with the antecedent to b', and add an undesignated node with the negation of the consequent to b'', then tick n.
- 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=MaterialConditional(negated)>}), pred=(<NodeDesignation:(designated=False)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.MaterialConditional), (Legend.designation, False))
The rule class legend.
- quantifier: Quantifier | None = None
- class MaterialBiconditionalDesignated(tableau, /, **opts)[source]
- ≡⊕A ≡ B ⊕⋮¬A ⊕¬B ⊕B ⊕A ⊕
From an unticked designated material biconditional node n on a branch b, make two new branches b' and b'' from b, add a designated node with the negation of the antecedent and a designated node with the negation of the consequent to b', and add a designated node with the antecedent and a designated node with the consequent to b'', then tick n.
- 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=MaterialBiconditional>}), pred=(<NodeDesignation:(designated=True)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.operator, Operator.MaterialBiconditional), (Legend.designation, True))
The rule class legend.
- quantifier: Quantifier | None = None
- class MaterialBiconditionalNegatedDesignated(tableau, /, **opts)[source]
- ¬≡⊕¬(A ≡ B) ⊕⋮A ⊕¬B ⊕¬A ⊕B ⊕
From an unticked designated negated material biconditional node n on a branch b, make two branches b' and b'' from b, add a designated node with the antecedent and a designated node with the negation of the consequent to b', and add a designated node with the negation of the antecedent and a designated node with the consequent to b'', then tick n.
- 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=MaterialBiconditional(negated)>}), pred=(<NodeDesignation:(designated=True)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.MaterialBiconditional), (Legend.designation, True))
The rule class legend.
- quantifier: Quantifier | None = None
- class MaterialBiconditionalUndesignated(tableau, /, **opts)[source]
- ≡⊖A ≡ B ⊖⋮A ⊖¬B ⊖¬A ⊖B ⊖
- 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=MaterialBiconditional>}), pred=(<NodeDesignation:(designated=False)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.operator, Operator.MaterialBiconditional), (Legend.designation, False))
The rule class legend.
- quantifier: Quantifier | None = None
- class MaterialBiconditionalNegatedUndesignated(tableau, /, **opts)[source]
- ¬≡⊖¬(A ≡ B) ⊖⋮¬A ⊖¬B ⊖B ⊖A ⊖
- 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=MaterialBiconditional(negated)>}), pred=(<NodeDesignation:(designated=False)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.MaterialBiconditional), (Legend.designation, False))
The rule class legend.
- quantifier: Quantifier | None = None
- class ConditionalDesignated(tableau, /, **opts)[source]
- →⊕A → B ⊕⋮¬A ⊕B ⊕
- 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=Conditional>}), pred=(<NodeDesignation:(designated=True)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.operator, Operator.Conditional), (Legend.designation, True))
The rule class legend.
- quantifier: Quantifier | None = None
- class ConditionalNegatedDesignated(tableau, /, **opts)[source]
- ¬→⊕¬(A → B) ⊕⋮A ⊕¬B ⊕
- 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=Conditional(negated)>}), pred=(<NodeDesignation:(designated=True)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.Conditional), (Legend.designation, True))
The rule class legend.
- quantifier: Quantifier | None = None
- class ConditionalUndesignated(tableau, /, **opts)[source]
- →⊖A → B ⊖⋮¬A ⊖B ⊖
- 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=Conditional>}), pred=(<NodeDesignation:(designated=False)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.operator, Operator.Conditional), (Legend.designation, False))
The rule class legend.
- quantifier: Quantifier | None = None
- class ConditionalNegatedUndesignated(tableau, /, **opts)[source]
- ¬→⊖¬(A → B) ⊖⋮A ⊖¬B ⊖
- 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=Conditional(negated)>}), pred=(<NodeDesignation:(designated=False)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.Conditional), (Legend.designation, False))
The rule class legend.
- quantifier: Quantifier | None = None
- class BiconditionalDesignated(tableau, /, **opts)[source]
- ↔⊕A ↔ B ⊕⋮¬A ⊕¬B ⊕B ⊕A ⊕
- 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=Biconditional>}), pred=(<NodeDesignation:(designated=True)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.operator, Operator.Biconditional), (Legend.designation, True))
The rule class legend.
- quantifier: Quantifier | None = None
- class BiconditionalNegatedDesignated(tableau, /, **opts)[source]
- ¬↔⊕¬(A ↔ B) ⊕⋮A ⊕¬B ⊕¬A ⊕B ⊕
- 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=Biconditional(negated)>}), pred=(<NodeDesignation:(designated=True)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.Biconditional), (Legend.designation, True))
The rule class legend.
- quantifier: Quantifier | None = None
- class BiconditionalUndesignated(tableau, /, **opts)[source]
- ↔⊖A ↔ B ⊖⋮A ⊖¬B ⊖¬A ⊖B ⊖
- 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=Biconditional>}), pred=(<NodeDesignation:(designated=False)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.operator, Operator.Biconditional), (Legend.designation, False))
The rule class legend.
- quantifier: Quantifier | None = None
- class BiconditionalNegatedUndesignated(tableau, /, **opts)[source]
- ¬↔⊖¬(A ↔ B) ⊖⋮¬A ⊖¬B ⊖B ⊖A ⊖
- 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=Biconditional(negated)>}), pred=(<NodeDesignation:(designated=False)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.Biconditional), (Legend.designation, False))
The rule class legend.
- quantifier: Quantifier | None = None
- class ExistentialDesignated(tableau, /, **opts)[source]
- ∃⊕∃xFx ⊕⋮Fa ⊕
From an unticked designated existential node n on a branch b quantifying over variable v into sentence s, add a designated node to b with the substitution into s of a new constant not yet appearing on b for v, then tick n.
- 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:quantifier=Existential>}), pred=(<NodeDesignation:(designated=True)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.quantifier, Quantifier.Existential), (Legend.designation, True))
The rule class legend.
- quantifier: Quantifier | None = 0
- class ExistentialNegatedDesignated(tableau, /, **opts)[source]
- ¬∃⊕¬∃xFx ⊕⋮∀x¬Fx ⊕
From an unticked designated negated existential node n on a branch b, quantifying over variable v into sentence s, add a designated node to b that universally quantifies over v into the negation of s (i.e. change ¬∃xFx to ∀x¬Fx), then tick n.
- 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:quantifier=Existential(negated)>}), pred=(<NodeDesignation:(designated=True)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.quantifier, Quantifier.Existential), (Legend.designation, True))
The rule class legend.
- quantifier: Quantifier | None = 0
- class ExistentialUndesignated(tableau, /, **opts)[source]
- ∃⊖∃xFx ⊖⋮Fa ⊖
From an undesignated existential node n on a branch b, for any constant c on b such that the result r of substituting c for the variable bound by the sentence of n does not appear on b, then add an undesignated node with r to b. If there are no constants yet on b, then instantiate with a new constant. The node n is never ticked.
- 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:quantifier=Existential>}), pred=(<NodeDesignation:(designated=False)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:quantifier=Existential>), 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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.quantifier, Quantifier.Existential), (Legend.designation, False))
The rule class legend.
- quantifier: Quantifier | None = 0
- class ExistentialNegatedUndesignated(tableau, /, **opts)[source]
- ¬∃⊖¬∃xFx ⊖⋮∀x¬Fx ⊖
- 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:quantifier=Existential(negated)>}), pred=(<NodeDesignation:(designated=False)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.quantifier, Quantifier.Existential), (Legend.designation, False))
The rule class legend.
- quantifier: Quantifier | None = 0
- class UniversalDesignated(tableau, /, **opts)[source]
- ∀⊕∀xFx ⊕⋮Fa ⊕
- 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:quantifier=Universal>}), pred=(<NodeDesignation:(designated=True)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.quantifier, Quantifier.Universal), (Legend.designation, True))
The rule class legend.
- quantifier: Quantifier | None = 1
- class UniversalNegatedDesignated(tableau, /, **opts)[source]
- ¬∀⊕¬∀xFx ⊕⋮∃x¬Fx ⊕
- 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:quantifier=Universal(negated)>}), pred=(<NodeDesignation:(designated=True)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.quantifier, Quantifier.Universal), (Legend.designation, True))
The rule class legend.
- quantifier: Quantifier | None = 1
- class UniversalUndesignated(tableau, /, **opts)[source]
- ∀⊖∀xFx ⊖⋮Fa ⊖
- 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:quantifier=Universal>}), pred=(<NodeDesignation:(designated=False)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:quantifier=Universal>), 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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.quantifier, Quantifier.Universal), (Legend.designation, False))
The rule class legend.
- quantifier: Quantifier | None = 1
- class UniversalNegatedUndesignated(tableau, /, **opts)[source]
- ¬∀⊖¬∀xFx ⊖⋮∃x¬Fx ⊖
- 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:quantifier=Universal(negated)>}), pred=(<NodeDesignation:(designated=False)>, <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}
- defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})
- legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.quantifier, Quantifier.Universal), (Legend.designation, False))
The rule class legend.
- quantifier: Quantifier | None = 1
- unquantifying_groups = ((<class 'pytableaux.logics.fde.Rules.ExistentialDesignated'>, <class 'pytableaux.logics.fde.Rules.ExistentialUndesignated'>), (<class 'pytableaux.logics.fde.Rules.UniversalDesignated'>, <class 'pytableaux.logics.fde.Rules.UniversalUndesignated'>))
- unquantifying_rules = (<class 'pytableaux.logics.fde.Rules.ExistentialDesignated'>, <class 'pytableaux.logics.fde.Rules.ExistentialUndesignated'>, <class 'pytableaux.logics.fde.Rules.UniversalDesignated'>, <class 'pytableaux.logics.fde.Rules.UniversalUndesignated'>)
- closure: tuple[type[ClosingRule], ...] = (<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.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.fde.Rules.ExistentialDesignated'>, <class 'pytableaux.logics.fde.Rules.ExistentialUndesignated'>), (<class 'pytableaux.logics.fde.Rules.UniversalDesignated'>, <class 'pytableaux.logics.fde.Rules.UniversalUndesignated'>))