K³_WQ - Weak Kleene Logic with alternate quantification

This is a version of K³_W with a different treatment of the quantifiers in terms of generalized conjunction/disjunction. This yields some interesting rules for the quantifiers, given the behavior of those operators in K³_W.

Semantics 

Truth Values 

Common labels for the values include:

T	1	true
N	0.5	meaningless
F	0	false

Designated Values

The set of designated values for K³_WQ is the singleton: { T }

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
N	N
F	T

Conjunction
∧	T	N	F
T	T	N	F
N	N	N	N
F	F	N	F

Disjunction
∨	T	N	F
T	T	N	T
N	N	N	N
F	T	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	N	F
T	T	N	F
N	N	N	N
F	T	N	T

Material Biconditional
≡	T	N	F
T	T	N	F
N	N	N	N
F	F	N	T

Compatibility Tables

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

Assertion
	⚬
T	T
N	N
F	F

Conditional
→	T	N	F
T	T	N	F
N	N	N	N
F	T	N	T

Biconditional
↔	T	N	F
T	T	N	F
N	N	N	N
F	F	N	T

Predication 

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\).
N iff \(\langle a_0, ... ,a_n\rangle\) is in neither the extension nor the anti-extension of \(P\).

Quantification 

Existential

An existential sentence is interpreted in terms of generalized disjunction. If we order the values least to greatest as N, T, F, then we can define the value of an existential in terms of the maximum value of the set of values for the substitution of each constant in the model for the variable.

Universal

A universal sentence is interpreted in terms of generalized conjunction. If we order the values least to greatest as N, F, T, then we can define the value of a universal in terms of the minimum value of the set of values for the substitution of each constant in the model for the variable.

Consequence 

Logical Consequence is defined in terms of the set of designated values { T }:

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 

K³_WQ tableaux are built similary to FDE.

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 A₁ ... A_n ∴ B write:

A₁ ⊕

⋮

A_n ⊕

B ⊖

Closure 

⊗Glut Closure[source]: A ⊕

⋮

¬A ⊕

⊗

⊗Designation Closure[source]: A ⊕

⋮

A ⊖

⊗

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

¬¬⊕FDEDouble Negation Designated[source]: ¬¬A ⊕

⋮

A ⊕

¬¬⊖FDEDouble Negation Undesignated[source]: ¬¬A ⊖

⋮

A ⊖

∧ Rules

∧⊕FDEConjunction Designated[source]: A ∧ B ⊕

⋮

A ⊕

B ⊕

∧⊖FDEConjunction Undesignated[source]: A ∧ B ⊖

⋮

A ⊖

B ⊖

¬∧⊕K³_WConjunction Negated Designated[source]: ¬(A ∧ B) ⊕

⋮

A ⊕

¬B ⊕

¬A ⊕

B ⊕

¬A ⊕

¬B ⊕

¬∧⊖K³_WConjunction Negated Undesignated[source]: ¬(A ∧ B) ⊖

⋮

A ⊖

¬A ⊖

B ⊖

¬B ⊖

A ⊕

B ⊕

∨ Rules

∨⊕K³_WDisjunction Designated[source]: A ∨ B ⊕

⋮

A ⊕

¬B ⊕

¬A ⊕

B ⊕

A ⊕

B ⊕

∨⊖K³_WDisjunction Undesignated[source]: A ∨ B ⊖

⋮

A ⊖

¬A ⊖

B ⊖

¬B ⊖

¬A ⊕

¬B ⊕

¬∨⊕FDEDisjunction Negated Designated[source]: ¬(A ∨ B) ⊕

⋮

¬A ⊕

¬B ⊕

¬∨⊖K³_WDisjunction Negated Undesignated[source]: ¬(A ∨ B) ⊖

⋮

A ∨ B ⊕

A ⊖

¬A ⊖

B ⊖

¬B ⊖

⊃ Rules

⊃⊕K³_WMaterial Conditional Designated[source]: A ⊃ B ⊕

⋮

¬A ∨ B ⊕

⊃⊖K³_WMaterial Conditional Undesignated[source]: A ⊃ B ⊖

⋮

¬A ∨ B ⊖

¬⊃⊕K³_WMaterial Conditional Negated Designated[source]: ¬(A ⊃ B) ⊕

⋮

¬(¬A ∨ B) ⊕

¬⊃⊖K³_WMaterial Conditional Negated Undesignated[source]: ¬(A ⊃ B) ⊖

⋮

¬(¬A ∨ B) ⊖

≡ Rules

≡⊕K³_WMaterial Biconditional Designated[source]: A ≡ B ⊕

⋮

(A ⊃ B) ∧ (B ⊃ A) ⊕

≡⊖K³_WMaterial Biconditional Undesignated[source]: A ≡ B ⊖

⋮

(A ⊃ B) ∧ (B ⊃ A) ⊖

¬≡⊕K³_WMaterial Biconditional Negated Designated[source]: ¬(A ≡ B) ⊕

⋮

¬((A ⊃ B) ∧ (B ⊃ A)) ⊕

¬≡⊖K³_WMaterial Biconditional Negated Undesignated[source]: ¬(A ≡ B) ⊖

⋮

¬((A ⊃ B) ∧ (B ⊃ A)) ⊖

Quantifier Rules

∃ Rules

∃⊕Existential Designated[source]: ∃xFx ⊕

⋮

∀x(Fx ∨ ¬Fx) ⊕

Fa ⊕

∃⊖Existential Undesignated[source]: ∃xFx ⊖

⋮

Fa ⊖

¬Fa ⊖

∀x¬Fx ⊕

¬∃⊕FDEExistential Negated Designated[source]: ¬∃xFx ⊕

⋮

∀x¬Fx ⊕

¬∃⊖Existential Negated Undesignated[source]: ¬∃xFx ⊖

⋮

¬Fa ⊖

∀ Rules

∀⊕FDEUniversal Designated[source]: ∀xFx ⊕

⋮

Fa ⊕

∀⊖FDEUniversal Undesignated[source]: ∀xFx ⊖

⋮

Fa ⊖

¬∀⊕Universal Negated Designated[source]: ¬∀xFx ⊕

⋮

∀x(Fx ∨ ¬Fx) ⊕

¬Fa ⊕

¬∀⊖Universal Negated Undesignated[source]: ¬∀xFx ⊖

⋮

Fa ⊖

¬Fa ⊖

∀xFx ⊕

Compatibility Rules

⚬ Rules

⚬⊕FDEAssertion Designated[source]: ⚬A ⊕

⋮

A ⊕

⚬⊖FDEAssertion Undesignated[source]: ⚬A ⊖

⋮

A ⊖

¬⚬⊕FDEAssertion Negated Designated[source]: ¬⚬A ⊕

⋮

¬A ⊕

¬⚬⊖FDEAssertion Negated Undesignated[source]: ¬⚬A ⊖

⋮

¬A ⊖

→ Rules

→⊕K³_WConditional Designated[source]: A → B ⊕

⋮

¬A ∨ B ⊕

→⊖K³_WConditional Undesignated[source]: A → B ⊖

⋮

¬A ∨ B ⊖

¬→⊕K³_WConditional Negated Designated[source]: ¬(A → B) ⊕

⋮

¬(¬A ∨ B) ⊕

¬→⊖K³_WConditional Negated Undesignated[source]: ¬(A → B) ⊖

⋮

¬(¬A ∨ B) ⊖

↔ Rules

↔⊕K³_WBiconditional Designated[source]: A ↔ B ⊕

⋮

(A ⊃ B) ∧ (B ⊃ A) ⊕

↔⊖K³_WBiconditional Undesignated[source]: A ↔ B ⊖

⋮

(A ⊃ B) ∧ (B ⊃ A) ⊖

¬↔⊕K³_WBiconditional Negated Designated[source]: ¬(A ↔ B) ⊕

⋮

¬((A ⊃ B) ∧ (B ⊃ A)) ⊕

¬↔⊖K³_WBiconditional Negated Undesignated[source]: ¬(A ↔ B) ⊖

⋮

¬((A ⊃ B) ∧ (B ⊃ A)) ⊖

Notes 

Standard interdefinability of the quantifiers is preserved.

References 

class Rules[source]

closure: tuple[type[ClosingRule], ...] = (<class 'pytableaux.logics.k3.Rules.GlutClosure'>, <class 'pytableaux.logics.fde.Rules.DesignationClosure'>)

class ExistentialDesignated(tableau, /, **opts)[source]

∃⊕

∃xFx ⊕

⋮

∀x(Fx ∨ ¬Fx) ⊕

Fa ⊕

From an unticked, designated existential node n on a branch b, add two designated nodes to b. One node is the result of universally quantifying over the disjunction of the inner sentence with its negation. The other node is a substitution of a constant new 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: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}

branching: int = 0: The number of additional branches created.

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

designation: bool | None = True

legend: tuple[tuple[str, Any], ...] = ((Legend.quantifier, Quantifier.Existential), (Legend.designation, True)): The rule class legend.

name: str = 'ExistentialDesignated': 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 ExistentialUndesignated(tableau, /, **opts)[source]

∃⊖

∃xFx ⊖

⋮

Fa ⊖

¬Fa ⊖

∀x¬Fx ⊕

From an unticked, undesignated existential node n on a branch b, make two branches b' and b'' from b. On b' add two undesignated nodes, one with the substituion of a constant new to b for the inner sentence, and the other with the negation of that sentence. On b'' add a designated node with universal quantifier over the negation of the inner sentence. 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: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}): 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 = False

legend: tuple[tuple[str, Any], ...] = ((Legend.quantifier, Quantifier.Existential), (Legend.designation, False)): The rule class legend.

name: str = 'ExistentialUndesignated': 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 ExistentialNegatedUndesignated(tableau, /, **opts)[source]

¬∃⊖

¬∃xFx ⊖

⋮

¬Fa ⊖

" From an unticked, undesignated, negated existential node n on a branch b, add an undesignated node to b with the negation of the inner sentence, substituting a constant new to b for the variable. 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:quantifier=Existential(negated)>}), pred=(<NodeDesignation:(designated=False)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:quantifier=Existential(negated)>), 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 = False

legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.quantifier, Quantifier.Existential), (Legend.designation, False)): The rule class legend.

name: str = 'ExistentialNegatedUndesignated': 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 UniversalNegatedDesignated(tableau, /, **opts)[source]

¬∀⊕

¬∀xFx ⊕

⋮

∀x(Fx ∨ ¬Fx) ⊕

¬Fa ⊕

From an unticked, designated, negated universal node n on a branch b, add two designated nodes to b. The first node is a universally quantified disjunction of the inner sentence and its negation. The second node is the negation of the inner sentence, substituting a constant new to b for the variable. 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=Universal(negated)>}), pred=(<NodeDesignation:(designated=True)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:quantifier=Universal(negated)>), 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 = True

legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.quantifier, Quantifier.Universal), (Legend.designation, True)): The rule class legend.

name: str = 'UniversalNegatedDesignated': 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 UniversalNegatedUndesignated(tableau, /, **opts)[source]

¬∀⊖

¬∀xFx ⊖

⋮

Fa ⊖

¬Fa ⊖

∀xFx ⊕

From an unticked, undesignated, negated universal node n on a branch b, make two branches b' and b'' from b. On b' add two undesignated nodes, one with the substitution of a constant new to b for the inner sentence of n, and the other with the negation of that sentence. On b'', add a designated node with the negatum of n. 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:quantifier=Universal(negated)>}), pred=(<NodeDesignation:(designated=False)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:quantifier=Universal(negated)>), 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 = 1: The number of additional branches created.

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

designation: bool | None = False

legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.quantifier, Quantifier.Universal), (Legend.designation, False)): The rule class legend.

name: str = 'UniversalNegatedUndesignated': 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.

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.DisjunctionNegatedDesignated'>, <class 'pytableaux.logics.fde.Rules.ExistentialNegatedDesignated'>, <class 'pytableaux.logics.fde.Rules.DoubleNegationDesignated'>, <class 'pytableaux.logics.fde.Rules.DoubleNegationUndesignated'>, <class 'pytableaux.logics.k3w.Rules.MaterialConditionalDesignated'>, <class 'pytableaux.logics.k3w.Rules.MaterialConditionalUndesignated'>, <class 'pytableaux.logics.k3w.Rules.MaterialConditionalNegatedDesignated'>, <class 'pytableaux.logics.k3w.Rules.MaterialConditionalNegatedUndesignated'>, <class 'pytableaux.logics.k3w.Rules.ConditionalDesignated'>, <class 'pytableaux.logics.k3w.Rules.ConditionalUndesignated'>, <class 'pytableaux.logics.k3w.Rules.ConditionalNegatedDesignated'>, <class 'pytableaux.logics.k3w.Rules.ConditionalNegatedUndesignated'>, <class 'pytableaux.logics.k3w.Rules.MaterialBiconditionalDesignated'>, <class 'pytableaux.logics.k3w.Rules.MaterialBiconditionalUndesignated'>, <class 'pytableaux.logics.k3w.Rules.MaterialBiconditionalNegatedDesignated'>, <class 'pytableaux.logics.k3w.Rules.MaterialBiconditionalNegatedUndesignated'>, <class 'pytableaux.logics.k3w.Rules.BiconditionalDesignated'>, <class 'pytableaux.logics.k3w.Rules.BiconditionalUndesignated'>, <class 'pytableaux.logics.k3w.Rules.BiconditionalNegatedDesignated'>, <class 'pytableaux.logics.k3w.Rules.BiconditionalNegatedUndesignated'>), (<class 'pytableaux.logics.fde.Rules.ConjunctionUndesignated'>,), (<class 'pytableaux.logics.k3w.Rules.DisjunctionDesignated'>, <class 'pytableaux.logics.k3w.Rules.DisjunctionUndesignated'>, <class 'pytableaux.logics.k3w.Rules.ConjunctionNegatedDesignated'>, <class 'pytableaux.logics.k3w.Rules.ConjunctionNegatedUndesignated'>, <class 'pytableaux.logics.k3w.Rules.DisjunctionNegatedUndesignated'>), (<class 'pytableaux.logics.k3wq.Rules.ExistentialDesignated'>, <class 'pytableaux.logics.k3wq.Rules.ExistentialNegatedUndesignated'>, <class 'pytableaux.logics.k3wq.Rules.ExistentialUndesignated'>, <class 'pytableaux.logics.k3wq.Rules.UniversalNegatedDesignated'>, <class 'pytableaux.logics.k3wq.Rules.UniversalNegatedUndesignated'>), (<class 'pytableaux.logics.fde.Rules.UniversalDesignated'>, <class 'pytableaux.logics.fde.Rules.UniversalUndesignated'>))

K3WQ - Weak Kleene Logic with alternate quantification

Operator Rules

¬ Rules

∧ Rules

∨ Rules

⊃ Rules

≡ Rules

Quantifier Rules

∃ Rules

∀ Rules

Compatibility Rules

⚬ Rules

→ Rules

↔ Rules

K³_WQ - Weak Kleene Logic with alternate quantification