From ad0a0bcc5813268432e98da91da7c12b566d7404 Mon Sep 17 00:00:00 2001 From: Pierre Casteran Date: Tue, 29 Aug 2023 11:12:27 +0200 Subject: [PATCH] small changes --- .gitignore | 1 + theories/goedel/codeSysPrf.v | 12 ++++++--- theories/goedel/goedel1.v | 40 ++++++++++++++++++------------ theories/ordinals/Ackermann/code.v | 2 ++ 4 files changed, 36 insertions(+), 19 deletions(-) diff --git a/.gitignore b/.gitignore index 8157301d..3eec56fa 100644 --- a/.gitignore +++ b/.gitignore @@ -38,6 +38,7 @@ alectryon-html/ .envrc /theories/ordinals/*/*.tex /theories/ordinals/*/*.pdf +/theories/goedel/*.pdf /theories/gaia/*.tex /theories/gaia/*.pdf /doc/JFLA2022/Slides/*.png diff --git a/theories/goedel/codeSysPrf.v b/theories/goedel/codeSysPrf.v index 6a6ea09a..0a7574a5 100644 --- a/theories/goedel/codeSysPrf.v +++ b/theories/goedel/codeSysPrf.v @@ -25,9 +25,8 @@ From hydras.Ackermann Require Import wellFormed. From hydras.Ackermann Require Import prLogic. From hydras Require Import Compat815. -Import LNN NN. -Import NNnotations. +(* begin hide *) Ltac SimplFreeVar := repeat match goal with @@ -96,6 +95,7 @@ Ltac SimplFreeVar := | H:(In _ (freeVarT ?X9 (var ?X9 _))) |- _ => simpl in H; decompose sum H; clear H end. +(* end hide *) Section code_SysPrf. @@ -122,12 +122,18 @@ Hypothesis Hypothesis codeFInj : forall f g : Functions L, codeF f = codeF g -> f = g. Hypothesis codeRInj : forall R S : Relations L, codeR R = codeR S -> R = S. + +Import LNN NN. +Import NNnotations. + Section LNN. Variable T : System. Hypothesis TextendsNN : Included _ NN T. + Variable U : fol.System L. -Variable fU : Formula. +Variable fU : Formula. (* LNN *) + Variable v0 : nat. Hypothesis freeVarfU : forall v : nat, In v (freeVarF LNN fU) -> v = v0. Hypothesis diff --git a/theories/goedel/goedel1.v b/theories/goedel/goedel1.v index 8a713476..416dfc82 100644 --- a/theories/goedel/goedel1.v +++ b/theories/goedel/goedel1.v @@ -5,8 +5,7 @@ From hydras.Ackermann Require Import folProp. From hydras.Ackermann Require Import folProof. From hydras.Ackermann Require Import subProp. From hydras.Ackermann Require Import ListExt. -From Goedel Require Import fixPoint. -From Goedel Require Import codeSysPrf. +From Goedel Require Import fixPoint codeSysPrf. From hydras.Ackermann Require Import wConsistent. From hydras.Ackermann Require Import NN. From hydras.Ackermann Require Import code. @@ -15,13 +14,15 @@ From hydras Require Import Compat815. From LibHyps Require Export LibHyps. From hydras Require Export MoreLibHyps NewNotations. + Import NNnotations. -Definition codeFormula := +(* TO do: remove this kind of redefinition *) +Definition codeFNN := codeFormula LNN codeLNTFunction codeLNNRelation. (* cf Gilles' paper ? *) -Notation reflection f := (natToTerm (codeFormula f)). +Notation reflection f := (natToTerm (codeFNN f)). Section Goedel's_1st_Incompleteness. @@ -33,22 +34,26 @@ 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" + + (see also codeSysPrf.v) *) Variable repT : Formula. Variable v0 : nat. Hypothesis freeVarRepT : forall v : nat, In v (freeVarF LNN repT) -> v = v0. + Hypothesis expressT1 : - forall f : Formula, - mem _ T f -> + forall f : Formula, mem _ T f -> SysPrf T (substF LNN repT v0 (reflection f)). + Hypothesis expressT2 : - forall f : Formula, - ~ mem _ T f -> - SysPrf T - (notH (substF LNN repT v0 (reflection f))). + forall f : Formula, ~ mem _ T f -> + SysPrf T (~ (substF LNN repT v0 (reflection f)))%nn. + + + Definition codeSysPrf := codeSysPrf LNN codeLNTFunction codeLNNRelation codeArityLNTF codeArityLNNR @@ -58,6 +63,9 @@ Definition codeSysPf := codeSysPf LNN codeLNTFunction codeLNNRelation codeArityLNTF codeArityLNNR codeArityLNTFIsPR codeArityLNNRIsPR repT v0. +Definition G := let (a,_) := FixPointLNN (notH codeSysPf) 0 in a. + + Definition codeSysPfCorrect := codeSysPfCorrect LNN codeLNTFunction codeLNNRelation codeArityLNTF codeArityLNNR codeArityLNTFIsPR codeArityLNTFIsCorrect1 codeArityLNNRIsPR @@ -74,7 +82,7 @@ Definition codeSysPrfCorrect3 := codeArityLNTFIsCorrect2 codeArityLNNRIsPR codeArityLNNRIsCorrect1 codeArityLNNRIsCorrect2 codeLNTFunctionInj codeLNNRelationInj T extendsNN. -Definition G := let (a,_) := FixPointLNN (notH codeSysPf) 0 in a. + Lemma freeVarG : closed G. Proof. @@ -109,7 +117,7 @@ Proof. (notH (substF LNN (notH codeSysPf) 0 (codeNatToTerm.natToTermLNN - (code.codeFormula LNN codeLNTFunction codeLNNRelation x)))). + (codeFNN x)))). + apply cp2, iffE1; apply sysExtend with NN; auto. + rewrite (subFormulaNot LNN); apply nnI; now apply codeSysPfCorrect. @@ -162,7 +170,7 @@ Proof. destruct (eq_nat_dec (checkPrf LNN codeLNTFunction codeLNNRelation codeArityLNTF codeArityLNNR - (codeFormula x) x0) 0) as [e |n ]. + (codeFNN x) x0) 0) as [e |n ]. + apply H4. rewrite (subFormulaNot LNN). unfold codeSysPrf, codeX in |- *. @@ -171,9 +179,9 @@ Proof. assert (H6: (checkPrf LNN codeLNTFunction codeLNNRelation codeArityLNTF codeArityLNNR - (codeFormula x) + (codeFNN x) (codePrf LNN codeLNTFunction codeLNNRelation A x p) = - S (cPair.codeList (map codeFormula A)))). + S (cPair.codeList (map codeFNN A)))). { apply (checkPrfCorrect1 LNN codeLNTFunction codeLNNRelation codeArityLNTF @@ -184,7 +192,7 @@ Proof. + assert (H5: (checkPrf LNN codeLNTFunction codeLNNRelation codeArityLNTF codeArityLNNR - (codeFormula x) x0 <> 0)) + (codeFNN x) x0 <> 0)) by assumption. clear n; decompose record (checkPrfCorrect2 LNN codeLNTFunction codeLNNRelation codeArityLNTF diff --git a/theories/ordinals/Ackermann/code.v b/theories/ordinals/Ackermann/code.v index 9f5255d9..6732ecdb 100644 --- a/theories/ordinals/Ackermann/code.v +++ b/theories/ordinals/Ackermann/code.v @@ -516,3 +516,5 @@ Lemma codeIffCorrect : Proof. intros; reflexivity. Qed. End Code_Term_Formula_Proof. + +About codeFormula.