Trivalent propositional logic

Propositional syntax (Trivalent.Formula) evaluated into Trivalent by the strong Kleene tables (Formula.eval), with realization at a Trivalent.Designation threshold (Formula.Realize, notation M ⊨[d] φ) and consequence instantiating Core.Logic.Consequence.MixedConsequence. The k3 diagonal is strong Kleene logic and the lp diagonal Priest's Logic of Paradox — same tables, different designated values ([CERvR12]).

The API mirrors Mathlib.ModelTheory (Realize, per-constructor @[simp] lemmas, ⊨ notation); consequence follows linglib's list-based MixedConsequence rather than Set-based theories, matching the [CERvR12] framework its consumers use.

Main results

• Formula.realize_neg — the K3/LP duality: negation swaps the standards.
• k3_no_tautologies, lp_all_satisfiable — the all-indet model gives K3 no tautologies and LP no unsatisfiable formulas ([CERvR12], Theorem 2).
• lp_no_explosion — LP is paraconsistent: {φ ∧ ¬φ} ⊭ ψ.

References

[Kle52] [CERvR12]

inductive Trivalent.Formula (Atom : Type u_1) : Type u_1

Propositional formulas over an atom type (Semantics.Supervaluation.TCSFormula instantiates it).

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

@[reducible, inline]

abbrev Trivalent.Model (Atom : Type u_1) : Type u_1

A trivalent model: a truth value for each atom.

Equations

• Trivalent.Model Atom = (Atom → Trivalent)

def Trivalent.Formula.eval {Atom : Type u_1} (M : Model Atom) : Formula Atom → Trivalent

Evaluation by the strong Kleene tables — the semantic core shared by K3 and LP, which differ only in designation.

Equations

• Trivalent.Formula.eval M (Trivalent.Formula.atom a) = M a
• Trivalent.Formula.eval M φ.neg = (Trivalent.Formula.eval M φ).neg
• Trivalent.Formula.eval M (φ.conj ψ) = min (Trivalent.Formula.eval M φ) (Trivalent.Formula.eval M ψ)

@[simp]

theorem Trivalent.Formula.eval_atom {Atom : Type u_1} (M : Model Atom) (a : Atom) : eval M (atom a) = M a

@[simp]

theorem Trivalent.Formula.eval_neg {Atom : Type u_1} (M : Model Atom) (φ : Formula Atom) : eval M φ.neg = (eval M φ).neg

@[simp]

theorem Trivalent.Formula.eval_conj {Atom : Type u_1} (M : Model Atom) (φ ψ : Formula Atom) : eval M (φ.conj ψ) = min (eval M φ) (eval M ψ)

def Trivalent.Formula.Realize {Atom : Type u_1} (M : Model Atom) (d : Designation) (φ : Formula Atom) : Prop

Realization at a designation standard: the evaluation clears the threshold. Realize M .k3 is strong Kleene satisfaction, Realize M .lp Priest's LP.

Equations

• Trivalent.Formula.Realize M d φ = Trivalent.designated d (Trivalent.Formula.eval M φ)

def Trivalent.Formula.«term_⊨[_]_» : Lean.TrailingParserDescr

Realization at a designation standard: the evaluation clears the threshold. Realize M .k3 is strong Kleene satisfaction, Realize M .lp Priest's LP.

Equations

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

@[simp]

theorem Trivalent.Formula.realize_atom {Atom : Type u_1} (M : Model Atom) (d : Designation) (a : Atom) : Realize M d (atom a) ↔ designated d (M a)

@[simp]

theorem Trivalent.Formula.realize_neg {Atom : Type u_1} (M : Model Atom) (d : Designation) (φ : Formula Atom) : Realize M d φ.neg ↔ ¬Realize M d.dual φ

The K3/LP duality at formula level: negation swaps the standards.

@[simp]

theorem Trivalent.Formula.realize_conj {Atom : Type u_1} (M : Model Atom) (d : Designation) (φ ψ : Formula Atom) : Realize M d (φ.conj ψ) ↔ Realize M d φ ∧ Realize M d ψ

Realization distributes over conjunction at either standard.

@[reducible, inline]

abbrev Trivalent.Consequence {Atom : Type u_1} (m n : Designation) (Γ : List (Formula Atom)) (φ : Formula Atom) : Prop

Mixed consequence over designation standards: premises at m, conclusion at n.

Equations

• Trivalent.Consequence m n Γ φ = Core.Logic.Consequence.MixedConsequence Trivalent.Formula.Realize m n Γ φ

Meta-theorems

theorem Trivalent.eval_allIndet {Atom : Type u_1} (φ : Formula Atom) : Formula.eval (fun (x : Atom) => indet) φ = indet

In the all-indeterminate model every formula evaluates to indet.

theorem Trivalent.k3_no_tautologies {Atom : Type u_1} [Nonempty Atom] (φ : Formula Atom) : ¬∀ (M : Model Atom), Formula.Realize M Designation.k3 φ

K3 has no tautologies: nothing is designated in the all-indeterminate model ([CERvR12], Theorem 2).

theorem Trivalent.lp_all_satisfiable {Atom : Type u_1} (φ : Formula Atom) : Formula.Realize (fun (x : Atom) => indet) Designation.lp φ

Every formula is LP-satisfiable: the all-indeterminate model designates everything ([CERvR12], Theorem 2).

theorem Trivalent.lp_no_explosion : ∃ (φ : Formula Bool) (ψ : Formula Bool), ¬Consequence Designation.lp Designation.lp [φ.conj φ.neg] ψ

Explosion fails in LP: {a ∧ ¬a} ⊭ b, with countermodel M a = indet, M b = false.