Kleene's three-valued logic

A comparison with a NULL operand is neither true nor false but unknown, and SQL evaluates predicates in Kleene's strong three-valued logic. A row on which a predicate is unknown is not selected, and neither is it selected by the predicate's negation: unknown is a fixed point of negation, which is what no two-valued reading can imitate.

The connectives are the minimum and maximum of the order false < unknown < true, with negation exchanging the two definite values. Every law of a De Morgan algebra holds; what fails is the excluded middle, a ⊔ ¬a = true, exactly at unknown.

inductive Kleene : Type

A three-valued truth value.

• false : Kleene

  Definitely false.

• unknown : Kleene

  Neither: a comparison with a NULL operand.

• true : Kleene

  Definitely true.

@[instance_reducible]

instance instDecidableEqKleene : DecidableEq Kleene

Equations

• instDecidableEqKleene x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def instReprKleene.repr : Kleene → Nat → Std.Format

Equations

• instReprKleene.repr Kleene.false prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kleene.false")).group prec✝
• instReprKleene.repr Kleene.unknown prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kleene.unknown")).group prec✝
• instReprKleene.repr Kleene.true prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kleene.true")).group prec✝

@[instance_reducible]

instance instReprKleene : Repr Kleene

Equations

• instReprKleene = { reprPrec := instReprKleene.repr }

def Kleene.ofBool : Bool → Kleene

A two-valued truth value read as a three-valued one.

Equations

• Kleene.ofBool false = Kleene.false
• Kleene.ofBool true = Kleene.true

def Kleene.isTrue : Kleene → Bool

Whether the value is definitely true. This is the reading a selection takes: a row on which the predicate is unknown is not selected.

Equations

• Kleene.true.isTrue = true
• x✝.isTrue = false

def Kleene.not : Kleene → Kleene

Kleene negation: it exchanges the definite values and fixes unknown.

Equations

• Kleene.false.not = Kleene.true
• Kleene.unknown.not = Kleene.unknown
• Kleene.true.not = Kleene.false

def Kleene.and : Kleene → Kleene → Kleene

Kleene conjunction: the minimum in false < unknown < true.

Equations

• Kleene.false.and x✝ = Kleene.false
• x✝.and Kleene.false = Kleene.false
• Kleene.unknown.and x✝ = Kleene.unknown
• x✝.and Kleene.unknown = Kleene.unknown
• Kleene.true.and Kleene.true = Kleene.true

def Kleene.or : Kleene → Kleene → Kleene

Kleene disjunction: the maximum in false < unknown < true.

Equations

• Kleene.true.or x✝ = Kleene.true
• x✝.or Kleene.true = Kleene.true
• Kleene.unknown.or x✝ = Kleene.unknown
• x✝.or Kleene.unknown = Kleene.unknown
• Kleene.false.or Kleene.false = Kleene.false

Home · Documentation · Publications · Contributors · Source · Cite