From 9e09641f75857e699837a14bacc7a57ae31f14ab Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 21:40:14 +0000 Subject: [PATCH] abi: prove Kleene ternary-logic soundness (Layer 2 Semantics) Flagship semantic proof: negation involution + De Morgan laws, plus a decidable `Designated` (classical-truth) proposition with sound+complete Dec, certifier soundness, conjunction preservation, and positive + negative controls (negation is provably not the identity; U/F are provably not designated). Verified with idris2 0.7.0 (build clean, zero warnings) + adversarial false-proof rejection. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- .../abi/Betlangiser/ABI/Semantics.idr | 160 ++++++++++++++++++ src/interface/abi/betlangiser-abi.ipkg | 1 + 2 files changed, 161 insertions(+) create mode 100644 src/interface/abi/Betlangiser/ABI/Semantics.idr diff --git a/src/interface/abi/Betlangiser/ABI/Semantics.idr b/src/interface/abi/Betlangiser/ABI/Semantics.idr new file mode 100644 index 0000000..4aea86c --- /dev/null +++ b/src/interface/abi/Betlangiser/ABI/Semantics.idr @@ -0,0 +1,160 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Flagship semantic proof for Betlangiser (Idris2 ABI Layer 2). +||| +||| Betlangiser's headline is "ternary probabilistic modelling". The logical +||| substrate is three-valued (Kleene) logic over `Trit = T | U | F` (true / +||| unknown / false). This module proves that substrate is algebraically sound: +||| +||| 1. negation is an involution (`doubleNeg`: not3 (not3 x) = x); +||| 2. De Morgan holds (`deMorgan`: not3 (and3 x y) = or3 (not3 x) (not3 y)); +||| 3. `Designated` (classical truth, = T) is a decidable proposition with a +||| sound+complete `Dec`, a certifier proven sound, and `and3` preserves it; +||| 4. positive + negative controls, the negative ones machine-checking that the +||| laws are non-vacuous (negation is genuinely not the identity; U and F are +||| genuinely not designated). + +module Betlangiser.ABI.Semantics + +import Betlangiser.ABI.Types +import Decidable.Equality + +%default total + +-------------------------------------------------------------------------------- +-- The three truth values and the Kleene connectives +-------------------------------------------------------------------------------- + +public export +data Trit = T | U | F + +public export +not3 : Trit -> Trit +not3 T = F +not3 U = U +not3 F = T + +||| Kleene conjunction (the min under F < U < T). +public export +and3 : Trit -> Trit -> Trit +and3 F _ = F +and3 _ F = F +and3 T T = T +and3 T U = U +and3 U T = U +and3 U U = U + +||| Kleene disjunction (the max under F < U < T). +public export +or3 : Trit -> Trit -> Trit +or3 T _ = T +or3 _ T = T +or3 F F = F +or3 F U = U +or3 U F = U +or3 U U = U + +-------------------------------------------------------------------------------- +-- Algebraic laws (universally quantified, proven by total case analysis) +-------------------------------------------------------------------------------- + +||| Negation is an involution. +export +doubleNeg : (x : Trit) -> not3 (not3 x) = x +doubleNeg T = Refl +doubleNeg U = Refl +doubleNeg F = Refl + +||| De Morgan: negating a conjunction is the disjunction of the negations. +export +deMorgan : (x, y : Trit) -> not3 (and3 x y) = or3 (not3 x) (not3 y) +deMorgan T T = Refl +deMorgan T U = Refl +deMorgan T F = Refl +deMorgan U T = Refl +deMorgan U U = Refl +deMorgan U F = Refl +deMorgan F T = Refl +deMorgan F U = Refl +deMorgan F F = Refl + +-------------------------------------------------------------------------------- +-- Designated truth as a decidable proposition (no inhabitant for U or F) +-------------------------------------------------------------------------------- + +||| A `Designated` value is classically true — in Kleene logic, exactly `T`. +||| There is no constructor for `U` or `F`. +public export +data Designated : Trit -> Type where + DesT : Designated T + +export +Uninhabited (Designated U) where + uninhabited DesT impossible + +export +Uninhabited (Designated F) where + uninhabited DesT impossible + +public export +decDesignated : (t : Trit) -> Dec (Designated t) +decDesignated T = Yes DesT +decDesignated U = No absurd +decDesignated F = No absurd + +||| Truth-functional soundness: conjunction preserves designation. +export +andDesignated : Designated x -> Designated y -> Designated (and3 x y) +andDesignated DesT DesT = DesT + +-------------------------------------------------------------------------------- +-- Certifier into the ABI Result, proven sound +-------------------------------------------------------------------------------- + +public export +certifyDesignated : Trit -> Result +certifyDesignated t = case decDesignated t of + Yes _ => Ok + No _ => Error + +export +certifyDesignatedSound : (t : Trit) -> certifyDesignated t = Ok -> Designated t +certifyDesignatedSound t prf with (decDesignated t) + certifyDesignatedSound t prf | Yes d = d + certifyDesignatedSound t Refl | No _ impossible + +-------------------------------------------------------------------------------- +-- Positive controls +-------------------------------------------------------------------------------- + +export +tDesignated : Designated T +tDesignated = DesT + +export +andTTDesignated : Designated (and3 T T) +andTTDesignated = andDesignated DesT DesT + +export +certifyTAccepts : certifyDesignated T = Ok +certifyTAccepts = Refl + +-------------------------------------------------------------------------------- +-- Negative controls — the laws are non-vacuous +-------------------------------------------------------------------------------- + +||| Negation is genuinely not the identity (so `doubleNeg` is non-trivial). +export +negationNotIdentity : Not (not3 T = T) +negationNotIdentity Refl impossible + +||| `U` is not designated — Kleene "unknown" is not classical truth. +export +uNotDesignated : Not (Designated U) +uNotDesignated = absurd + +||| `F` is not designated. +export +fNotDesignated : Not (Designated F) +fNotDesignated = absurd diff --git a/src/interface/abi/betlangiser-abi.ipkg b/src/interface/abi/betlangiser-abi.ipkg index df6e494..08bf69d 100644 --- a/src/interface/abi/betlangiser-abi.ipkg +++ b/src/interface/abi/betlangiser-abi.ipkg @@ -7,3 +7,4 @@ modules = Betlangiser.ABI.Types , Betlangiser.ABI.Layout , Betlangiser.ABI.Foreign , Betlangiser.ABI.Proofs + , Betlangiser.ABI.Semantics