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 ... AnB 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