K3 - Strong Kleene Logic

Photo of Stephen Kleene

Stephen Kleene

K3 is a three-valued logic with values T, F, and N. It can be understood as FDE without the B value.


Semantics

Truth Values

Common labels for the values include:

T

1

just true

N

0.5

neither true nor false

F

0

just false

Designated Values

The set of designated values for K3 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 F
F F F F
Disjunction
∨ T N F
T T T T
N T 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 T N N
F T T T
Material Biconditional
≡ T N F
T T N F
N N N N
F F N T

Compatibility Tables

K3 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 T N N
F T T T
Biconditional
↔ T N F
T T N F
N N N N
F F N T

Predication

Like FDE, K3 predication defines a predicate's extenstion and anti-extension. The value of a predicated sentence is determined as follows:

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

Note, unlike FDE, there is an exclusivity constraint on a predicate's extension/anti-extension. This means that \(\langle a_0, ... ,a_n\rangle\) cannot be in both the extension and the anti-extension of \(P\).

Like FDE, there is no exhaustion constraint: there are permissible K3 models where some tuple \(\langle a_0, ... ,a_n\rangle\) is in neither the extension nor the anti-extension of some predicate \(P\).

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 }:

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

K3 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 A1 ... An ∴ B write:
A1 ⊕
⋮
An ⊕
B ⊖

Closure

In addition to the FDE closure rule, K3 includes a glut closure rule. This means a branch closes when a sentence and its negation both appear as designated nodes on the branch.

⊗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 ⊖
¬∧⊕FDEConjunction Negated Designated[source]
¬(A ∧ B) ⊕
⋮
¬A ⊕
¬B ⊕
¬∧⊖FDEConjunction Negated Undesignated[source]
¬(A ∧ B) ⊖
⋮
¬A ⊖
¬B ⊖
∨ Rules
∨⊕FDEDisjunction Designated[source]
A ∨ B ⊕
⋮
A ⊕
B ⊕
∨⊖FDEDisjunction Undesignated[source]
A ∨ B ⊖
⋮
A ⊖
B ⊖
¬∨⊕FDEDisjunction Negated Designated[source]
¬(A ∨ B) ⊕
⋮
¬A ⊕
¬B ⊕
¬∨⊖FDEDisjunction Negated Undesignated[source]
¬(A ∨ B) ⊖
⋮
¬A ⊖
¬B ⊖
⊃ Rules
⊃⊕FDEMaterial Conditional Designated[source]
A ⊃ B ⊕
⋮
¬A ⊕
B ⊕
⊃⊖FDEMaterial Conditional Undesignated[source]
A ⊃ B ⊖
⋮
¬A ⊖
B ⊖
¬⊃⊕FDEMaterial Conditional Negated Designated[source]
¬(A ⊃ B) ⊕
⋮
A ⊕
¬B ⊕
¬⊃⊖FDEMaterial Conditional Negated Undesignated[source]
¬(A ⊃ B) ⊖
⋮
A ⊖
¬B ⊖
≡ Rules
≡⊕FDEMaterial Biconditional Designated[source]
A ≡ B ⊕
⋮
¬A ⊕
¬B ⊕
B ⊕
A ⊕
≡⊖FDEMaterial Biconditional Undesignated[source]
A ≡ B ⊖
⋮
A ⊖
¬B ⊖
¬A ⊖
B ⊖
¬≡⊕FDEMaterial Biconditional Negated Designated[source]
¬(A ≡ B) ⊕
⋮
A ⊕
¬B ⊕
¬A ⊕
B ⊕
¬≡⊖FDEMaterial Biconditional Negated Undesignated[source]
¬(A ≡ B) ⊖
⋮
¬A ⊖
¬B ⊖
B ⊖
A ⊖

Quantifier Rules

∃ Rules
∃⊕FDEExistential Designated[source]
∃xFx ⊕
⋮
Fa ⊕
∃⊖FDEExistential Undesignated[source]
∃xFx ⊖
⋮
Fa ⊖
¬∃⊕FDEExistential Negated Designated[source]
¬∃xFx ⊕
⋮
∀x¬Fx ⊕
¬∃⊖FDEExistential Negated Undesignated[source]
¬∃xFx ⊖
⋮
∀x¬Fx ⊖
∀ Rules
∀⊕FDEUniversal Designated[source]
∀xFx ⊕
⋮
Fa ⊕
∀⊖FDEUniversal Undesignated[source]
∀xFx ⊖
⋮
Fa ⊖
¬∀⊕FDEUniversal Negated Designated[source]
¬∀xFx ⊕
⋮
∃x¬Fx ⊕
¬∀⊖FDEUniversal Negated Undesignated[source]
¬∀xFx ⊖
⋮
∃x¬Fx ⊖

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
→⊕FDEConditional Designated[source]
A → B ⊕
⋮
¬A ⊕
B ⊕
→⊖FDEConditional Undesignated[source]
A → B ⊖
⋮
¬A ⊖
B ⊖
¬→⊕FDEConditional Negated Designated[source]
¬(A → B) ⊕
⋮
A ⊕
¬B ⊕
¬→⊖FDEConditional Negated Undesignated[source]
¬(A → B) ⊖
⋮
A ⊖
¬B ⊖
↔ Rules
↔⊕FDEBiconditional Designated[source]
A ↔ B ⊕
⋮
¬A ⊕
¬B ⊕
B ⊕
A ⊕
↔⊖FDEBiconditional Undesignated[source]
A ↔ B ⊖
⋮
A ⊖
¬B ⊖
¬A ⊖
B ⊖
¬↔⊕FDEBiconditional Negated Designated[source]
¬(A ↔ B) ⊕
⋮
A ⊕
¬B ⊕
¬A ⊕
B ⊕
¬↔⊖FDEBiconditional Negated Undesignated[source]
¬(A ↔ B) ⊖
⋮
¬A ⊖
¬B ⊖
B ⊖
A ⊖

Notes

Some notable features of K3 include:

References