feat: soundness and completeness of linear logic phase semantics

Cslib.lean

@@ -118,4 +118,6 @@ public import Cslib.Logics.LinearLogic.CLL.Basic
 public import Cslib.Logics.LinearLogic.CLL.CutElimination
 public import Cslib.Logics.LinearLogic.CLL.EtaExpansion
 public import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic
+public import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Completeness
+public import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Soundness
 public import Cslib.Logics.Propositional.Defs

Cslib/Logics/LinearLogic/CLL/Basic.lean

@@ -11,6 +11,8 @@ public import Cslib.Foundations.Syntax.Context
 public import Cslib.Foundations.Logic.InferenceSystem
 public import Cslib.Foundations.Logic.LogicalEquivalence
 public import Mathlib.Data.Multiset.Fold
+public import Mathlib.Data.Multiset.AddSub
+public import Mathlib.Data.Multiset.Basic
 
 @[expose] public section
 
@@ -129,6 +131,15 @@ def Proposition.negative : Proposition Atom → Bool
   | quest _ => true
   | _ => false
 
+/--
+Whether a proposition is in the multiplicative-additive fragment (MALL), i.e. it
+contains no exponentials.
+-/
+def Proposition.IsMALL : Proposition Atom → Prop
+  | .atom _ | .atomDual _ | .one | .bot | .top | .zero => True
+  | .tensor a b | .parr a b | .oplus a b | .with a b => a.IsMALL ∧ b.IsMALL
+  | .bang _ | .quest _ => False
+
 /-- Whether a `Proposition` is positive is decidable. -/
 instance Proposition.positive_decidable (a : Proposition Atom) : Decidable a.positive :=
   a.positive.decEq true
@@ -188,6 +199,10 @@ def Proposition.linImpl (a b : Proposition Atom) : Proposition Atom := a⫠ ⅋
 /-- A sequent in CLL is a multiset of propositions. -/
 abbrev Sequent Atom := Multiset (Proposition Atom)
 
+/-- A sequent is MALL if every proposition in it is MALL. -/
+def Sequent.IsMALL (Γ : Sequent Atom) : Prop :=
+  ∀ A ∈ Γ, (A : Proposition Atom).IsMALL
+
 /-- Checks that all propositions in a sequent `Γ` are question marks. -/
 def Sequent.allQuest (Γ : Sequent Atom) :=
   Γ.map (· matches ʔ_)
@@ -720,6 +735,37 @@ end Proposition
 
 end LogicalEquiv
 
+/-- Folds a sequent into a single formula by taking the par of all its members. -/
+noncomputable def foldParr {Atom : Type u} (Γ : Sequent Atom) : Proposition Atom :=
+  Γ.toList.foldr (· ⅋ ·) ⊥
+
+theorem foldParr_isMALL {Atom : Type u} (Γ : Sequent Atom)
+    (h : Sequent.IsMALL Γ) :
+    Proposition.IsMALL (foldParr Γ) := by
+  suffices ∀ l : List (Proposition Atom), (∀ A ∈ l, A.IsMALL) →
+      (List.foldr (· ⅋ ·) ⊥ l).IsMALL by
+    exact this _ (fun A hA => h A (by aesop))
+  intro l hl; induction l <;> simp [Proposition.IsMALL]; grind [Proposition.IsMALL]
+
+theorem derivable_of_list_foldr_parr {Atom : Type u}
+    (l : List (Proposition Atom)) (Δ : Sequent Atom) :
+    Derivable ((List.foldr (· ⅋ ·) ⊥ l) ::ₘ Δ) →
+    Derivable ((l : Sequent Atom) + Δ) := by
+  induction l generalizing Δ with
+  | nil => intro ⟨p⟩; exact ⟨Proof.rwConclusion (by simp) p.bot_inversion⟩
+  | cons a l ih =>
+    intro ⟨p⟩
+    have p' := Proof.rwConclusion (Multiset.cons_swap ..) (Proof.parr_inversion p)
+    rcases ih (Δ := a ::ₘ Δ) ⟨p'⟩ with ⟨q⟩
+    have hEq : (↑l + (a ::ₘ Δ)) = (↑(a :: l) + Δ) := by
+      have : a ::ₘ (↑l + Δ) = (a ::ₘ ↑l) + Δ := (Multiset.cons_add a ↑l Δ).symm
+      simp_all
+    exact ⟨q.rwConclusion hEq⟩
+
+theorem derivable_of_foldParr {Atom : Type u} (Γ : Sequent Atom) :
+    Derivable ({foldParr Γ} : Sequent Atom) → Derivable Γ := by
+  intro h; have := derivable_of_list_foldr_parr Γ.toList 0 (by aesop); aesop
+
 end CLL
 
 end Cslib

Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean

@@ -44,10 +44,6 @@ correspond to specific set-theoretic operations.
 
 Several lemmas about facts and orthogonality useful in the proof of soundness are proven here.
 
-## TODO
-- Soundness theorem
-- Completeness theorem
-
 ## References
 
 * [J.-Y. Girard, *Linear logic*][Girard1987]
@@ -336,7 +332,7 @@ instance : Min (Fact P) where
 def idempotentsIn [Monoid M] (X : Set M) : Set M := {m | IsIdempotentElem m ∧ m ∈ X}
 
 /-- The set I of idempotents that "belong to 1" in the phase semantics. -/
-def I : Set P := idempotentsIn (1 : Set P)
+def I : Set P := idempotentsIn (1 : Fact P)
 
 /-! ## Interpretation of the connectives -/
 
@@ -462,8 +458,14 @@ lemma par_le_par {G H K L : Fact P} (hGK : G ≤ K) (hHL : H ≤ L) : (G ⅋ H)
 
 @[simp] lemma par_assoc {G H K : Fact P} : ((G ⅋ H) ⅋ K) = (G ⅋ H ⅋ K) := by simp [par_of_tensor]
 
+instance parAssociative {M : Type*} [PhaseSpace M] :
+    Std.Associative (α := Fact M) (· ⅋ ·) := ⟨fun _ _ _ => par_assoc⟩
+
 lemma par_comm (G H : Fact P) : (G ⅋ H) = (H ⅋ G) := by simp [par_of_tensor, tensor_comm]
 
+instance parCommutative {M : Type*} [PhaseSpace M] :
+    Std.Commutative (α := Fact M) (· ⅋ ·) := ⟨par_comm⟩
+
 /--
 Linear implication between facts,
 defined as the dual of the orthogonal of the pointwise product.
@@ -538,14 +540,14 @@ The exponential `!X` (of course) of a fact,
 defined as the dual of the orthogonal of the intersection with the idempotents.
 -/
 def bang (X : Fact P) : Fact P := dualFact (X ∩ I)⫠
-@[inherit_doc] prefix:100 " ! " => bang
+@[inherit_doc] prefix:100 "!" => bang
 
 /--
 The exponential `?X` (why not) of a fact,
 defined as the dual of the intersection of the orthogonal with the idempotents.
 -/
 def quest (X : Fact P) : Fact P := dualFact (X⫠ ∩ I)
-@[inherit_doc] prefix:100 " ʔ " => quest
+@[inherit_doc] prefix:100 "ʔ" => quest
 
 /-! ### Properties of Additives -/
 
@@ -703,6 +705,29 @@ def interpProp [PhaseSpace M] (v : Atom → Fact M) : Proposition Atom → Fact
 
 @[inherit_doc] scoped notation:max "⟦" P "⟧" v:90 => interpProp v P
 
+/-- Semantic interpretation of a sequent as the par-fold of its members. -/
+def Sequent.toFact (M : Type*) [PhaseSpace M]
+    (v : Atom → Fact M) (Γ : Sequent Atom) : Fact M :=
+  (Γ.map (fun A => (interpProp v A : Fact M))).fold (· ⅋ ·) ⊥
+
+theorem Sequent.toFact_nil {M : Type*} [PhaseSpace M] (v : Atom → Fact M) :
+    Sequent.toFact M v (0 : Sequent Atom) = ⊥ := by simp [Sequent.toFact]
+
+theorem Sequent.toFact_add {M : Type*} [PhaseSpace M]
+    (v : Atom → Fact M) (Γ Δ : Sequent Atom) :
+    Sequent.toFact M v (Γ + Δ) = Sequent.toFact M v Γ ⅋ Sequent.toFact M v Δ := by
+  simp only [Sequent.toFact]
+  rw [Multiset.map_add]
+  have := Multiset.fold_add
+    (fun (x y : Fact M) => x ⅋ y) ⊥ ⊥ (Γ.map fun A => interpProp v A)
+    ( Δ.map fun A => interpProp v A)
+  rwa [bot_par] at this
+
+@[simp] theorem Sequent.toFact_cons {M : Type*} [PhaseSpace M]
+    (v : Atom → Fact M) (A : Proposition Atom) (Γ : Sequent Atom) :
+    Sequent.toFact M v (A ::ₘ Γ) = interpProp v A ⅋ Sequent.toFact M v Γ := by
+  simp [Sequent.toFact]
+
 end PhaseSpace
 
 end CLL

Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean

@@ -0,0 +1,223 @@
+/-
+Copyright (c) 2026 Tanner Duve. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tanner Duve, Bhavik Mehta, Aleph Prover
+-/
+
+module
+
+public import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Soundness
+public import Mathlib.Algebra.Group.TypeTags.Basic
+public import Mathlib.Data.Multiset.Basic
+public import Mathlib.Algebra.Order.Group.Multiset
+import Mathlib.Data.Set.Basic
+import Mathlib.Algebra.Group.Idempotent
+import Mathlib.Algebra.Group.Pointwise.Set.Basic
+
+@[expose] public section
+
+/-!
+# Completeness for MALL via a phase model
+
+This file constructs a canonical phase model and proves completeness for the
+multiplicative-additive fragment of classical linear logic.
+
+## Main definitions
+
+* `CanonM`: the monoid of sequents
+* `PrSet`: the interpretation of propositions in the model
+* `canonVal`: the distinguished valuation
+
+## Main results
+
+* `PrSet_eq_orth`: truth sets are characterized by orthogonality
+* `interpProp_canon_carrier`: semantic interpretation agrees with `PrSet`
+* `derivable_of_foldParr`: derivability of the folded formula implies derivability of the sequent
+* `completeness`: semantic validity implies derivability for MALL sequents
+
+TODO: extend completeness from MALL to full CLL with exponentials. This
+requires a more complex phase-model construction to account for `!` and `?`.
+-/
+
+@[expose] public section
+
+namespace Cslib
+namespace CLL
+
+open scoped Pointwise
+open PhaseSpace Logic InferenceSystem
+open Fact Sequent
+
+universe u
+
+variable {Atom : Type u} {M : Type*} [PhaseSpace M]
+
+/-- The canonical monoid for the completeness construction: sequents under multiset addition. -/
+@[reducible] def CanonM (Atom : Type u) : Type u := Multiplicative (Sequent Atom)
+
+/-- The truth set of a proposition: sequent contexts that make `a` provable. -/
+def PrSet (Atom : Type u) (a : Proposition Atom) : Set (CanonM Atom) :=
+  {m | Derivable (a ::ₘ m.toAdd)}
+
+theorem PrSet_top {Atom : Type u} : PrSet Atom ⊤ = .univ := by
+  ext m
+  exact ⟨fun _ => trivial, fun _ => ⟨Proof.top⟩⟩
+
+theorem PrSet_with {Atom : Type u} (a b : Proposition Atom) :
+    PrSet Atom (a & b) = PrSet Atom a ∩ PrSet Atom b := by
+  ext m
+  simp only [PrSet, Set.mem_setOf_eq, Set.mem_inter_iff]
+  exact ⟨fun ⟨p⟩ => ⟨⟨p.with_inversion₁⟩, ⟨p.with_inversion₂⟩⟩,
+    fun ⟨⟨p⟩, ⟨q⟩⟩ => ⟨.with p q⟩⟩
+
+/-- The bottom set of the canonical phase space: provable sequents. -/
+def canonBot (Atom : Type u) : Set (CanonM Atom) :=
+  {m | Derivable m.toAdd}
+
+theorem PrSet_bot {Atom : Type u} : PrSet Atom ⊥ = canonBot Atom := by
+  ext m
+  exact ⟨fun ⟨p⟩ => ⟨p.bot_inversion⟩, fun ⟨p⟩ => ⟨p.bot⟩⟩
+
+instance canonPhaseSpace (Atom : Type u) : PhaseSpace (CanonM Atom) where
+  bot := canonBot Atom
+
+@[simp] theorem canonPhaseSpace_bot :
+    PhaseSpace.bot = canonBot Atom := rfl
+
+/-- A singleton sequent `{a}` belongs to the truth set of `a⫠` by the axiom rule. -/
+theorem singleton_mem_PrSet_dual {Atom : Type u} (a : Proposition Atom) :
+    (Multiplicative.ofAdd ({a} : Sequent Atom) : CanonM Atom) ∈ PrSet Atom a⫠ :=
+  ⟨@Proof.ax' Atom a⟩
+
+theorem PrSet_eq_orth {Atom : Type u} (a : Proposition Atom) :
+    PrSet Atom a = orthogonal (PrSet Atom (Proposition.dual a)) := by
+  ext m
+  constructor
+  · intro hm n hn
+    simp only [canonPhaseSpace_bot]
+    exact ⟨(toAdd_mul m n).symm ▸ hm.toDerivation.cut hn.toDerivation⟩
+  · intro hm
+    exact ⟨(hm _ (singleton_mem_PrSet_dual a)).toDerivation.rwConclusion
+      (by simp [toAdd_mul, add_comm])⟩
+
+theorem PrSet_dual_eq_orth {Atom : Type u} (a : Proposition Atom) :
+    PrSet Atom (Proposition.dual a) = orthogonal (PrSet Atom a) := by
+  grind [Proposition.dual_involution, PrSet_eq_orth]
+
+theorem PrSet_oplus {Atom : Type u} (a b : Proposition Atom) :
+    PrSet Atom (a ⊕ b) = orthogonal (orthogonal (PrSet Atom a ∪ PrSet Atom b)) := by
+  rw [PrSet_eq_orth]
+  congr 1
+  simp_rw [Proposition.dual, PrSet_with a⫠ b⫠, PrSet_dual_eq_orth a, PrSet_dual_eq_orth b]
+  grind
+
+theorem PrSet_parr {Atom : Type u} (a b : Proposition Atom) :
+    PrSet Atom (a ⅋ b) =
+    orthogonal (PrSet Atom (Proposition.dual a) * PrSet Atom (Proposition.dual b)) := by
+  ext m
+  constructor
+  · intro hm x hx
+    rcases Set.mem_mul.mp hx with ⟨s, hs, t, ht, rfl⟩
+    simp only [canonPhaseSpace_bot]
+    have hab := Proof.parr_inversion hm.toDerivation
+    have hb : ⇓(b ::ₘ (m.toAdd + s.toAdd)) :=
+      Proof.rwConclusion (by simp) (Proof.cut hab (hs : Derivable _).toDerivation)
+    exact ⟨Proof.rwConclusion (by simp [toAdd_mul, add_assoc])
+      (Proof.cut hb (ht : Derivable _).toDerivation)⟩
+  · intro hm
+    have hprov := hm _ (Set.mul_mem_mul (singleton_mem_PrSet_dual a) (singleton_mem_PrSet_dual b))
+    exact ⟨Proof.parr (hprov.toDerivation.rwConclusion
+      (by simp [toAdd_mul, add_comm, Multiset.singleton_add]))⟩
+
+theorem PrSet_tensor {Atom : Type u} (a b : Proposition Atom) :
+    PrSet Atom (a ⊗ b) =
+    orthogonal (orthogonal (PrSet Atom a * PrSet Atom b)) := by
+  rw [PrSet_eq_orth (a ⊗ b)]
+  congr 1
+  have := PrSet_parr (Proposition.dual a) (Proposition.dual b)
+  simp only [Proposition.dual_involution, orthogonal_def, Multiplicative.forall] at this
+  exact this
+
+/-- The canonical valuation: interprets each atom via its dual's truth set. -/
+def canonVal {Atom : Type u} (a : Atom) : Fact (CanonM Atom) :=
+  dualFact (PrSet Atom (Proposition.atomDual a))
+
+theorem interpProp_canon_carrier {Atom : Type u} (a : Proposition Atom)
+    (ha : Proposition.IsMALL a) :
+    ((@interpProp (CanonM Atom) Atom _ canonVal a) :
+        Set (CanonM Atom)) =
+      PrSet Atom a := by
+  induction a with
+  | atom a =>
+    simp [interpProp, canonVal, PrSet_eq_orth (.atom a), Proposition.dual]
+  | atomDual a =>
+    simp only [interpProp, canonVal, dualFact, coe_neg, mk_dual_coe]
+    conv_rhs => rw [PrSet_eq_orth (.atomDual a)]
+    simp only [Proposition.dual]
+    rw [PrSet_eq_orth (.atom a)]
+    simp [Proposition.dual, -orthogonal_def]
+  | one =>
+    simp only [interpProp, coe_one, canonPhaseSpace_bot, PrSet_eq_orth .one, Proposition.dual]
+    congr 1
+    exact PrSet_bot.symm
+  | zero =>
+    simp only [interpProp, coe_zero, PrSet_eq_orth .zero, Proposition.dual]
+    congr 1
+    exact PrSet_top.symm
+  | top =>
+    simp [interpProp, PrSet_top.symm]
+    rfl
+  | bot =>
+    simp only [interpProp]
+    exact PrSet_bot.symm
+  | tensor _ _ iha ihb =>
+    simp [interpProp, iha ha.1, ihb ha.2, tensor, dualFact, PrSet_tensor, -orthogonal_def]
+  | parr _ _ iha ihb =>
+    simp [interpProp, iha ha.1, ihb ha.2, parr, dualFact, PrSet_parr,
+      PrSet_dual_eq_orth, -orthogonal_def]
+  | oplus _ _ iha ihb =>
+    simp [interpProp, iha ha.1, ihb ha.2, oplus, dualFact, PrSet_oplus, -orthogonal_def]
+  | «with» _ _ iha ihb => simp [interpProp, iha ha.1, ihb ha.2, withh, PrSet_with]
+  | bang _ _ => exact False.elim ha
+  | quest _ _ => exact False.elim ha
+
+theorem interpProp_list_foldr_parr
+    (v : Atom → Fact M) (l : List (Proposition Atom)) :
+    interpProp v (List.foldr (fun A B => A ⅋ B) ⊥ l) =
+    List.foldr (fun A acc => (interpProp v A) ⅋ acc) ⊥ l := by
+  induction l <;> aesop
+
+theorem Sequent.toFact_eq_interpProp_foldParr
+    (v : Atom → Fact M) (Γ : Sequent Atom) :
+    Sequent.toFact M v Γ = interpProp v (foldParr Γ) := by
+  simp only [Sequent.toFact, foldParr]
+  rw [interpProp_list_foldr_parr v Γ.toList]
+  have hfold : ∀ l : List (Proposition Atom),
+      List.foldr (fun A acc => interpProp v A ⅋ acc) ⊥ l =
+      List.foldr (fun x y : Fact M => x ⅋ y) ⊥ (l.map (interpProp v)) := by
+    intro l
+    induction l <;> aesop
+  rw [hfold]
+  calc
+    (Γ.map (fun A => (interpProp v A))).fold (fun x y : Fact M => x ⅋ y) ⊥
+        = ((Γ.toList : Multiset (Proposition Atom)).map (fun A =>
+        (interpProp v A))).fold (fun x y : Fact M => x ⅋ y) ⊥ := by simp
+    _ = (((Γ.toList).map (fun A => interpProp v A)) :
+            Multiset (Fact M)).fold (fun x y : Fact M => x ⅋ y) ⊥ := by
+      grind [congrArg (fun s => s.fold (fun x y : Fact M => x ⅋ y) ⊥)
+        (@Multiset.map_coe _ _ (fun A => (interpProp v A)) (Γ.toList))]
+    _ = List.foldr (fun x y : Fact M => x ⅋ y) ⊥
+            ((Γ.toList).map (fun A => interpProp v A)) := by simp
+
+theorem completeness {Atom : Type u} (Γ : Sequent Atom)
+    (hMALL : IsMALL Γ) :
+    (∀ (M : Type u) [PhaseSpace M] (v : Atom → Fact M),
+        (Sequent.toFact M v Γ).IsValid) → Derivable Γ := by
+  intro h
+  have h₁ : 1 ∈ PrSet Atom (foldParr Γ) := by
+    rw [← interpProp_canon_carrier _ (foldParr_isMALL Γ hMALL)]
+    simp_all only [SetLike.mem_coe, ← Sequent.toFact_eq_interpProp_foldParr]
+  exact derivable_of_foldParr Γ (by aesop)
+
+end CLL
+end Cslib