wip: henkin

src/proof/Henkin.ard

@@ -0,0 +1,45 @@
+\import Consistent
+\import Function.Meta
+\import Logic
+\import Paths
+\import proof.NegationComplete
+\import proof.Proof
+\import proof.TermInterpretation
+\import semantics.Interpretation
+\import syntax.Context
+\import syntax.Syntax
+\import util.LogicUtil
+\open Interpretation (⊧)
+
+\lemma henkin {_ : Language} {c : Context} {T : Theory c}
+              (con : Consistent T)
+              (neg : NegationComplete T)
+  -- contains witnesses
+              (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 f)
+  | impH a f => {?}
+  | cAnd a b => <->cAnd <->* <->sigma (henkin con neg a) (henkin con neg b)
+  | forAllH f => {?}
+  | cExists f => {?}
+  \where {
+    \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) => (
+      \lam (inP prfA) (inP prfB) => con (inP (f, prfB, prfA)),
+      \lam n => \case neg f \with {
+        | byLeft h => absurd $ n $ inP $ h
+        | byRight h => inP h
+      }
+    )
+
+    \lemma <->cAnd {_ : Language} {c : Context} {T : Theory c} {f g : Formula c}
+      : Prf' T (cAnd f g) <-> (\Sigma (Prf' T f) (Prf' T g)) =>
+      (
+        \lam p => {?},
+        \lam _x => {?}
+      )
+  }

src/proof/NegationComplete.ard

@@ -0,0 +1,7 @@
+\import Logic
+\import proof.Proof
+\import syntax.Context
+\import syntax.Syntax
+
+\func NegationComplete {_ : Language} {c : Context} (T : Theory c) : \Prop
+  => \Pi (f : Formula c) -> Prf T f || Prf T (notH f)

src/proof/TermInterpretation.ard

@@ -148,7 +148,7 @@
       )
 
     \func isModelForAll {_ : Language} {c : Context} {T : Theory c} {f : Formula (suc c)}
-      : (TermInterpretation T) ⊧ forAllH f <--> ( \Pi (t : Term c) -> (TermInterpretation T) ⊧ Substitution.subst f t ) =>
+      : (TermInterpretation T) ⊧ forAllH f <-> ( \Pi (t : Term c) -> (TermInterpretation T) ⊧ Substitution.subst f t ) =>
       (\lam m t =>
            \let m' => m (in~ t)
            \in ⊧.fromSub.substitutionLemma<-

src/util/LogicUtil.ard

@@ -1,13 +1,25 @@
 \import Function.Meta
+\import Logic
 \import Meta
 \import Paths.Meta
 \import Relation.Equivalence
 
-\func \infix 5 <--> (A B : \Type) : \Type => \Sigma (A -> B) (B -> A)
-
 \func liftArrayElim {k : Nat} {A : Fin k -> \Type} {R : \Pi {j : Fin k} -> A j -> A j -> \Type} {refl : \Pi {j : Fin k} (x : A j) -> R x x}
                     {ts : DArray A}
   : Quotient.liftArray R refl (\lam i => in~ (ts i)) = {Quotient {DArray A} (\lam f g => \Pi (j : Fin ts.len) -> R (f j) (g j))} in~ ts
-  \elim k, ts
-    | 0, nil => idp
-    | suc k, a :: ts => unfold $ rewrite (liftArrayElim {k} {\lam i => A (suc i)}) idp
+\elim k, ts
+  | 0, nil => idp
+  | suc k, a :: ts => unfold $ rewrite (liftArrayElim {k} {\lam i => A (suc i)}) idp
+
+\lemma \infixl 6 <->* {P Q S : \Prop} (f : P <-> Q) (g : Q <-> S) : P <-> S => <->trans f g
+
+\lemma <->not {P Q : \Prop} (h : P <-> Q) : Not P <-> Not Q => (
+  \lam nP q => nP $ h.2 q,
+  \lam nQ p => nQ $ h.1 p
+)
+
+\lemma <->sigma {P Q R S : \Prop} (h : P <-> Q) (h' : R <-> S) : (\Sigma P R) <-> (\Sigma Q S) =>
+  (
+    \lam (p, r) => (h.1 p, h'.1 r),
+    \lam (q, s) => (h.2 q, h'.2 s)
+  )