henkin exists

TimothyEarley · Jan 11, 2025 · e46e030 · e46e030
1 parent 343b2d3
commit e46e030
Show file tree

Hide file tree

Showing 2 changed files with 112 additions and 16 deletions.
diff --git a/src/proof/Henkin.ard b/src/proof/Henkin.ard
@@ -1,39 +1,64 @@
+\import Arith.Nat
 \import Consistent
 \import Function.Meta
 \import Logic
+\import Logic.Meta
+\import Meta
 \import Relation.Equivalence
 \import proof.ContainsWitnesses
 \import proof.NegationComplete
+\import proof.PrfCorrect
 \import proof.Proof
 \import proof.TermInterpretation
 \import semantics.Interpretation
 \import syntax.Context
+\import syntax.SIze
+\import syntax.Substitution
 \import syntax.Syntax
 \import util.LogicUtil
+\import util.NatUtil
 \open Interpretation (⊧)
 
 \lemma henkin {_ : Language} {c : Context} {T : Theory c}
               (con : Consistent T)
               (neg : NegationComplete T)
               (wit : ContainsWitness T)
               (f : Formula c)
-  : Prf' T f <-> (TermInterpretation T) ⊧ f
-\elim f
-  | equal a b => <->sym TermInterpretation.isModelForEqual
-  | atomic r terms => <->sym TermInterpretation.isModelForAtomic
-  | notH f => <->notH con neg <->* <->not (henkin con neg wit f)
-  | impH a f => {?}
-  | cAnd a b => <->cAnd <->* <->sigma (henkin con neg wit a) (henkin con neg wit b)
-  | forAllH f => {?}
-  | cExists f => (
-    -- Prf to model
-    \case \elim __, wit f \with {
-      | inP p, inP (t, h) => inP (in~ t, {?})
-    },
-    -- Model to Prf
-    {?}
-  )
+  : Prf' T f <-> (TermInterpretation T) ⊧ f =>
+  henkinHelper con neg wit f (size f) NatSemiring.<=-refl
   \where {
+    \private \lemma henkinHelper {_ : Language} {c : Context} {T : Theory c}
+                                 (con : Consistent T)
+                                 (neg : NegationComplete T)
+                                 (wit : ContainsWitness T)
+                                 (f : Formula c)
+                                 (fuel : Nat) (fuelLargerThanSize : size f NatSemiring.<= fuel)
+      : Prf' T f <-> (TermInterpretation T) ⊧ f
+    \elim f, fuel
+      | equal a b, _ => <->sym TermInterpretation.isModelForEqual
+      | atomic r terms, _ => <->sym TermInterpretation.isModelForAtomic
+      | notH f, suc fuel => <->notH con neg <->* <->not (henkinHelper con neg wit f fuel (size.stepNot fuelLargerThanSize))
+      | impH a f, _ => {?}
+      | cAnd a b, fuel => <->cAnd <->* <->sigma
+                                               (henkinHelper con neg wit a fuel (size.stepAnd1 fuelLargerThanSize))
+                                               (henkinHelper con neg wit b fuel (size.stepAnd2 fuelLargerThanSize))
+      | forAllH f, _ => {?}
+      | cExists f, suc fuel =>
+        \let
+          | A => TruncP (\Sigma (t : Term c) (Prf T (Substitution.subst f t)))
+          | B => TruncP (\Sigma (t : Term c) (TermInterpretation T ⊧ Substitution.subst f t))
+          | C => TruncP (\Sigma (u : Universe {structure {TermInterpretation T}}) (Interpretation.extend (TermInterpretation T) u ⊧ f))
+          | tModel : B <-> C => <->sym $ TermInterpretation.isModelForExists {_} {c} {T} {f}
+          | goal : A <-> B => (
+            \lam (inP (t, prf)) => inP (t, (henkinHelper con neg wit (Substitution.subst f t) fuel (size.stepSubstSuc fuelLargerThanSize)).1 (inP prf)),
+            \lam (inP (t, model)) => TruncP.map ((henkinHelper con neg wit (Substitution.subst f t) fuel (size.stepSubstSuc fuelLargerThanSize)).2 model) (t, __)
+          )
+        \in
+          <->cExists wit <->* goal <->* tModel
+
+      -- the impossible cases there to aide termination
+      | f, 0 => absurd (size.not<=0 fuelLargerThanSize)
+
     \lemma <->notH {_ : Language} {c : Context} {T : Theory c} (con : Consistent T) (neg : NegationComplete T)
                    {f : Formula c}
       : Prf' T (notH f) <-> Not (Prf' T f) => (
@@ -50,4 +75,13 @@
         \lam (inP h) => (inP (cAndElim1 h idp), inP (cAndElim2 h idp)),
         \lam (inP prf1, inP prf2) => inP (and prf1 prf2 idp)
       )
+
+    \lemma <->cExists {_ : Language} {c : Context} {T : Theory c} {f : Formula (suc c)} (wit : ContainsWitness T)
+      : Prf' T (cExists f) <-> ∃ (t : Term c) (Prf T (Substitution.subst f t)) => (
+      \case \elim __, wit f \with {
+        | inP p, inP (t, h) => inP (t, Prf.modusPonens _ p h)
+      },
+      \case \elim __ \with {
+        | inP (t, p) => inP $ cExistsIntro t p idp
+      })
   }
diff --git a/src/syntax/SIze.ard b/src/syntax/SIze.ard
@@ -0,0 +1,62 @@
+\import Algebra.Meta
+\import Arith.Nat
+\import Function.Meta
+\import Logic
+\import Meta
+\import Paths
+\import Paths.Meta
+\import syntax.Context
+\import syntax.Substitution
+\import syntax.Syntax
+-- helper for recursion, where normal structural recursion does not work
+
+\func size {_ : Language} {c : Context} (f : Formula c) : Nat \elim f
+  | equal a b => 1
+  | atomic r terms => 1
+  | notH f => suc (size f)
+  | impH a f => NatSemiring.∨ (size a) (size f)
+  | cAnd a f => NatSemiring.∨ (size a) (size f)
+  | forAllH f => suc (size f)
+  | cExists f => suc (size f)
+
+  \where {
+    \func not<=0 {_ : Language} {c : Context} {f : Formula c}
+                 (h : size f NatSemiring.<= 0) : Empty
+    \elim f
+      | equal a b => h NatSemiring.zero<suc
+      | atomic r terms => h NatSemiring.zero<suc
+      | notH f => h $ NatSemiring.zero<suc
+      | impH a f => not<=0 {_} {c} {a} (NatSemiring.join-left NatSemiring.<=∘ h)
+      | cAnd a f => not<=0 {_} {c} {a} (NatSemiring.join-left NatSemiring.<=∘ h)
+      | forAllH f => h $ NatSemiring.zero<suc
+      | cExists f => h $ NatSemiring.zero<suc
+
+    \func stepNot {_ : Language} {c : Context} {f : Formula c}
+                  {fuel : Nat} (h : size (notH f) NatSemiring.<= suc fuel) : size f NatSemiring.<= fuel =>
+      \lam x => h (NatSemiring.suc<suc x)
+
+    \func stepAnd1 {_ : Language} {c : Context} {f g : Formula c}
+                   {fuel : Nat} (h : size (cAnd f g) NatSemiring.<= fuel) : size f NatSemiring.<= fuel =>
+      NatSemiring.join-left NatSemiring.<=∘ h
+
+    \func stepAnd2 {_ : Language} {c : Context} {f g : Formula c}
+                   {fuel : Nat} (h : size (cAnd f g) NatSemiring.<= fuel) : size g NatSemiring.<= fuel =>
+      NatSemiring.join-right NatSemiring.<=∘ h
+
+    \func stepSubstSuc {_ : Language} {c c' : Context} {f : Formula (suc c)} {s : Substitution (suc c) c'}
+                       {fuel : Nat}
+                       (h : suc (size f) NatSemiring.<= suc fuel) : size (Substitution.substitute f s) NatSemiring.<= fuel =>
+      rewriteI substPreservesSize (\lam x => h (NatSemiring.suc<suc x))
+
+    -- this is the important property we want
+    \func substPreservesSize {_ : Language} {c c' : Context} {f : Formula c} {s : Substitution c c'}
+      : size f = size (Substitution.substitute f s)
+    \elim f
+      | equal a b => idp
+      | atomic r terms => idp
+      | notH f => pmap suc substPreservesSize
+      | impH f g => pmap2 (NatSemiring.∨) substPreservesSize substPreservesSize
+      | cAnd f g => pmap2 (NatSemiring.∨) substPreservesSize substPreservesSize
+      | forAllH f => pmap suc substPreservesSize
+      | cExists f => pmap suc substPreservesSize
+  }