Strong Kleene Logic

Origin. Kleene's strong three-valued logic (1938, 1952). Third value: unknown/undefined. Some operations short-circuit: F∧U=F, T∨U=T. Foundation for logic programming semantics. Connection to fixed-point semantics and partial predicates.

Models. Partial information with short-circuit. Three values: T (true), F (false), U (unknown). Strong: some operations determined by one input. F ∧ anything = F. T ∨ anything = T. Models computation with undefined subexpressions.

Formalism.

Truth values: {T, F, U} — true, false, unknown.

Strong Kleene tables:

∧	T	F	U	∨	T	F	U	¬
T	T	F	U	T	T	T	T	T	F
F	F	F	F	F	T	F	U	F	T
U	U	F	U	U	T	U	U	U	U

Key property: F ∧ U = F (false dominates) T ∨ U = T (true dominates) Short-circuit evaluation.

Implication: A → B = ¬A ∨ B T → U = U, F → U = T, U → T = T, U → F = U, U → U = U.

Designated value: T is designated (for validity). Valid: true for all valuations. A ∨ ¬A not valid (U when A = U).

Kripke-Kleene fixed point: Least fixed point of truth definition. Three-valued models for logic programs.

Symbols.

Symbol	Unicode	Name	Meaning
∧	U+2227	Logical and	Strong conjunction, minimum on F < U < T
∨	U+2228	Logical or	Strong disjunction, maximum on F < U < T
¬	U+00AC	Not sign	Negation, fixed at U
→	U+2192	Rightwards arrow	Material implication, ¬A ∨ B
⊨	U+22A8	Satisfaction	Consequence: preservation of the designated value
⊑	U+2291	Square image of or equal to	Information ordering, U ⊑ T and U ⊑ F
T	—	True	Known true; the sole designated value
F	—	False	Known false
U	—	Unknown	Undefined, unknown, or gap
K3	—	Kleene's strong three-valued logic	The matrix ({T, U, F}, {T})
D	—	Designated set	{T}

Metatheory. Kleene (1938, 1952) gave the tables and proved what singles them out: among the regular three-valued tables — those in which an undefined argument is never allowed to change an output already fixed by the defined arguments — the strong scheme is the strongest and the weak scheme the weakest, so the two Kleene logics bracket the whole regular family. K3 has no valid formulas whatever, since the valuation sending every atom to U sends every formula to U and U is undesignated. Satisfiability behaves classically instead: the connectives are monotone in the information ordering, so refining a satisfying partial valuation to a classical one preserves the value T, and a formula is K3-satisfiable iff classically satisfiable. Satisfiability is therefore NP-complete and the consequence problem coNP-complete, with classical validity reducible to it by adding p ∨ ¬p for each atom as a premise. Algebraically K3 is the three-element Kleene algebra — a De Morgan lattice satisfying A ∧ ¬A ≤ B ∨ ¬B. Every K3-valid argument is classically valid, and re-designating U as a second value on the same tables gives Priest's LP. The monotonicity underwrites the least-fixed-point constructions of Kripke (1975) for truth and Fitting (1985) for logic programs.

Applies to. Logic programming (3-valued semantics). Partial functions. Database nulls. Vagueness. Truth-value gaps. Recursion semantics. Liar paradox treatments.

Limitations. With no valid formulas there is nothing to axiomatize in Hilbert style, so K3 must be presented as a consequence relation; the deduction theorem fails outright, since A ⊨ A while A → A takes the value U when A does. Excluded middle and non-contradiction both fail as validities. K3 is not paraconsistent — explosion holds vacuously, because no valuation designates both A and ¬A — so gaps do nothing against contradiction. Truth-functionality blocks penumbral connections: if A and B are both U so is A ∧ B, even where the two are incompatible — "this patch is red" and "this patch is orange" — and the conjunction ought to come out false. Undefinedness is not expressible, since no monotone connective returns T exactly at U, and adding a definedness operator destroys the monotonicity the fixed-point constructions depend on. The tables do not determine the logic: designating U instead yields LP, and the choice is made outside the semantics.