Three-Valued Logics: LP and K3

@cite{kleene-1952}

LP (Logic of Paradox) and K3 (Strong Kleene logic) are dual three-valued logics built on the same truth tables but with different designated values:

• K3 (Strong Kleene): designated value = {1}. Preserves truth.
• LP (Logic of Paradox): designated values = {1, ½}. Preserves non-falsity.

Both use Strong Kleene connectives (already in Core/Logic/Truth3.lean). The only difference is what counts as "satisfied": K3 requires value 1 (like classical truth), while LP accepts value ½ as well (overlap of truth and falsity, as in paraconsistent logic).

Key Results

• LP/K3 duality via negation: LP-sat(¬φ) ↔ ¬K3-sat(φ)
• LP preserves excluded middle: P ∨ ¬P is always LP-designated
• K3 has no tautologies: every formula gets value ½ in the all-indeterminate model
• Explosion fails in LP: P ∧ ¬P ⊭^LP Q
• Conjunction respects designation: LP/K3 designation distributes over Strong Kleene conjunction

Connection to TCS

@cite{cobreros-etal-2012} Theorem 3: in the restricted vocabulary, t-consequence = LP-consequence and s-consequence = K3-consequence. The correspondence is proved in Theories/Semantics/Supervaluation/TCS.lean.

def Core.Logic.ThreeValuedLogic.isLPDesignated (v : Duality.Truth3) : Prop

LP-designated: value is non-false (true or indeterminate). In LP, ½ is in the overlap of truth and falsity — both P and ¬P can hold. This makes LP paraconsistent: contradictions don't entail everything.

Equations

• Core.Logic.ThreeValuedLogic.isLPDesignated v = (v ≠ Core.Duality.Truth3.false)

def Core.Logic.ThreeValuedLogic.isK3Designated (v : Duality.Truth3) : Prop

K3-designated: value is true (= 1). The only designated value. This makes K3 paracomplete: some formulas (borderline cases) are neither true nor false.

Equations

• Core.Logic.ThreeValuedLogic.isK3Designated v = (v = Core.Duality.Truth3.true)

instance Core.Logic.ThreeValuedLogic.instDecidableIsLPDesignated (v : Duality.Truth3) : Decidable (isLPDesignated v)

Equations

• Core.Logic.ThreeValuedLogic.instDecidableIsLPDesignated v = inferInstanceAs (Decidable (v ≠ Core.Duality.Truth3.false))

instance Core.Logic.ThreeValuedLogic.instDecidableIsK3Designated (v : Duality.Truth3) : Decidable (isK3Designated v)

Equations

• Core.Logic.ThreeValuedLogic.instDecidableIsK3Designated v = inferInstanceAs (Decidable (v = Core.Duality.Truth3.true))

theorem Core.Logic.ThreeValuedLogic.lp_neg_iff_not_k3 (v : Duality.Truth3) : isLPDesignated v.neg ↔ ¬isK3Designated v

LP/K3 duality via negation. LP-designation of the negation is equivalent to K3-non-designation of the original. This is the semantic core of duality between LP and K3.

theorem Core.Logic.ThreeValuedLogic.k3_neg_iff_not_lp (v : Duality.Truth3) : isK3Designated v.neg ↔ ¬isLPDesignated v

K3-designation of the negation ↔ LP-non-designation.

theorem Core.Logic.ThreeValuedLogic.lp_meet (v w : Duality.Truth3) : isLPDesignated (v.meet w) ↔ isLPDesignated v ∧ isLPDesignated w

LP-designation distributes over Strong Kleene conjunction.

theorem Core.Logic.ThreeValuedLogic.k3_meet (v w : Duality.Truth3) : isK3Designated (v.meet w) ↔ isK3Designated v ∧ isK3Designated w

K3-designation distributes over Strong Kleene conjunction.

theorem Core.Logic.ThreeValuedLogic.k3_implies_lp (v : Duality.Truth3) : isK3Designated v → isLPDesignated v

K3-designation implies LP-designation.

theorem Core.Logic.ThreeValuedLogic.designations_agree_classical (b : Bool) : isLPDesignated (Duality.Truth3.ofBool b) ↔ isK3Designated (Duality.Truth3.ofBool b)

Both designations agree on classical (bivalent) values.

inductive Core.Logic.ThreeValuedLogic.PropFormula (Atom : Type u_1) : Type u_1

Propositional formulas over an atom type. Structurally identical to TCSFormula but parameterized by a single type.

• atom {Atom : Type u_1} : Atom → PropFormula Atom
• neg {Atom : Type u_1} : PropFormula Atom → PropFormula Atom
• conj {Atom : Type u_1} : PropFormula Atom → PropFormula Atom → PropFormula Atom

@[reducible, inline]

abbrev Core.Logic.ThreeValuedLogic.MVModel (Atom : Type u_1) : Type u_1

A many-valued model: assigns a three-valued truth value to each atom.

Equations

• Core.Logic.ThreeValuedLogic.MVModel Atom = (Atom → Core.Duality.Truth3)

def Core.Logic.ThreeValuedLogic.mvEval {Atom : Type u_1} (M : MVModel Atom) : PropFormula Atom → Duality.Truth3

Three-valued formula evaluation using Strong Kleene connectives. This is the semantic core shared by LP and K3 — the only difference is which values count as designated.

Equations

• Core.Logic.ThreeValuedLogic.mvEval M (Core.Logic.ThreeValuedLogic.PropFormula.atom a) = M a
• Core.Logic.ThreeValuedLogic.mvEval M φ.neg = (Core.Logic.ThreeValuedLogic.mvEval M φ).neg
• Core.Logic.ThreeValuedLogic.mvEval M (φ.conj ψ) = (Core.Logic.ThreeValuedLogic.mvEval M φ).meet (Core.Logic.ThreeValuedLogic.mvEval M ψ)

def Core.Logic.ThreeValuedLogic.lpSat {Atom : Type u_1} (M : MVModel Atom) (φ : PropFormula Atom) : Prop

LP-satisfaction: a formula is LP-satisfied iff its three-valued evaluation is designated (non-false).

Equations

• Core.Logic.ThreeValuedLogic.lpSat M φ = Core.Logic.ThreeValuedLogic.isLPDesignated (Core.Logic.ThreeValuedLogic.mvEval M φ)

def Core.Logic.ThreeValuedLogic.k3Sat {Atom : Type u_1} (M : MVModel Atom) (φ : PropFormula Atom) : Prop

K3-satisfaction: a formula is K3-satisfied iff its three-valued evaluation is true.

Equations

• Core.Logic.ThreeValuedLogic.k3Sat M φ = Core.Logic.ThreeValuedLogic.isK3Designated (Core.Logic.ThreeValuedLogic.mvEval M φ)

theorem Core.Logic.ThreeValuedLogic.lpSat_neg_iff {Atom : Type u_1} (M : MVModel Atom) (φ : PropFormula Atom) : lpSat M φ.neg ↔ ¬k3Sat M φ

LP/K3 duality lifts to formulas: LP-sat(¬φ) ↔ ¬K3-sat(φ).

theorem Core.Logic.ThreeValuedLogic.k3Sat_neg_iff {Atom : Type u_1} (M : MVModel Atom) (φ : PropFormula Atom) : k3Sat M φ.neg ↔ ¬lpSat M φ

K3-sat(¬φ) ↔ ¬LP-sat(φ).

theorem Core.Logic.ThreeValuedLogic.lpSat_conj {Atom : Type u_1} (M : MVModel Atom) (φ ψ : PropFormula Atom) : lpSat M (φ.conj ψ) ↔ lpSat M φ ∧ lpSat M ψ

LP-sat distributes over conjunction.

theorem Core.Logic.ThreeValuedLogic.k3Sat_conj {Atom : Type u_1} (M : MVModel Atom) (φ ψ : PropFormula Atom) : k3Sat M (φ.conj ψ) ↔ k3Sat M φ ∧ k3Sat M ψ

K3-sat distributes over conjunction.

def Core.Logic.ThreeValuedLogic.LPConsequence {Atom : Type u_1} (Γ : List (PropFormula Atom)) (φ : PropFormula Atom) : Prop

LP-consequence: preservation of LP-designation (nonzero value) from premises to conclusion.

Equations

• One or more equations did not get rendered due to their size.

def Core.Logic.ThreeValuedLogic.K3Consequence {Atom : Type u_1} (Γ : List (PropFormula Atom)) (φ : PropFormula Atom) : Prop

K3-consequence: preservation of value 1 from premises to conclusion.

Equations

• One or more equations did not get rendered due to their size.

theorem Core.Logic.ThreeValuedLogic.mvEval_allIndet {Atom : Type u_1} (φ : PropFormula Atom) : mvEval (fun (x : Atom) => Duality.Truth3.indet) φ = Duality.Truth3.indet

No K3 tautologies. In the all-indeterminate model, every formula evaluates to indet, so no formula is K3-valid.

Theorem 2 of @cite{cobreros-etal-2012}: no formula in the restricted vocabulary is s-valid.

theorem Core.Logic.ThreeValuedLogic.k3_no_tautologies {Atom : Type u_1} [Nonempty Atom] (φ : PropFormula Atom) : ¬∀ (M : MVModel Atom), k3Sat M φ

theorem Core.Logic.ThreeValuedLogic.lp_all_satisfiable {Atom : Type u_1} (φ : PropFormula Atom) : lpSat (fun (x : Atom) => Duality.Truth3.indet) φ

Every formula is LP-satisfiable. The all-indeterminate model LP-satisfies everything (since indet ≠ false).

Theorem 2 of @cite{cobreros-etal-2012}: every formula in the restricted vocabulary is t-satisfiable.

theorem Core.Logic.ThreeValuedLogic.lp_no_explosion : ∃ (φ : PropFormula Bool), ∃ (ψ : PropFormula Bool), ¬LPConsequence [φ.conj φ.neg] ψ

Explosion fails in LP. There exist atoms a, b such that {a ∧ ¬a} ⊭^LP b. Countermodel: M(a) = ½, M(b) = 0.