make goedel1 statement a little more abstract

coq-community · Aug 27, 2023 · a9a5713 · a9a5713
1 parent 0d5ba08
commit a9a5713
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 12 deletions.
diff --git a/theories/goedel/goedel1.v b/theories/goedel/goedel1.v
@@ -17,14 +17,23 @@ From LibHyps Require Export LibHyps.
 From hydras Require Export MoreLibHyps NewNotations.
 Import NNnotations.
 
-Section Goedel's_1st_Incompleteness.
+Definition codeFormula := 
+  codeFormula LNN codeLNTFunction codeLNNRelation.
 
-Definition codeFormula := codeFormula LNN codeLNTFunction codeLNNRelation.
+(* cf Gilles' paper ? *)
+Notation reflection f := (natToTerm (codeFormula f)).
+
+Section Goedel's_1st_Incompleteness.
 
 Variable T : System.
 
 Hypothesis extendsNN : Included _ NN T.
 
+(*
+ There exists a formula repT 
+  -  with only a free variable v0
+  -  which means "v0 is a term which reflects some axiom of T"
+*)
 Variable repT : Formula.
 Variable v0 : nat.
 Hypothesis
@@ -33,13 +42,13 @@ Hypothesis
   expressT1 :
     forall f : Formula,
     mem _ T f ->
-    SysPrf T (substF LNN repT v0 (natToTerm (codeFormula f))).
+    SysPrf T (substF LNN repT v0 (reflection f)).
 Hypothesis
   expressT2 :
     forall f : Formula,
     ~ mem _ T f ->
     SysPrf T
-      (notH (substF LNN repT v0 (natToTerm (codeFormula f)))).
+      (notH (substF LNN repT v0 (reflection f))).
 
 Definition codeSysPrf :=
   codeSysPrf LNN codeLNTFunction codeLNNRelation codeArityLNTF codeArityLNNR
@@ -101,13 +110,9 @@ Proof.
          (substF LNN (notH codeSysPf) 0
             (codeNatToTerm.natToTermLNN
                (code.codeFormula LNN codeLNTFunction codeLNNRelation x)))).
-    + apply cp2.
-      apply iffE1.
-      apply sysExtend with NN.
-      * assumption.
-      * apply H1.
-    + rewrite (subFormulaNot LNN); apply nnI.
-      apply codeSysPfCorrect; assumption.
+    + apply cp2, iffE1; apply sysExtend with NN; auto. 
+    + rewrite (subFormulaNot LNN); apply nnI; 
+      now apply codeSysPfCorrect. 
 Qed.
 
 (*I don't believe I can prove
@@ -291,5 +296,5 @@ Qed.
 
 End Goedel's_1st_Incompleteness.
 
-
+About Goedel'sIncompleteness1st.
 
diff --git a/theories/ordinals/Ackermann/LNN.v b/theories/ordinals/Ackermann/LNN.v
@@ -411,3 +411,4 @@ intros a v; induction a as [| a Hreca].
 Qed.
 
 
+
Original file line number	Diff line number	Diff line change
Expand Up		@@ -411,3 +411,4 @@ intros a v; induction a as [\| a Hreca].
		Qed.