fix

FormalizedFormalLogic · Dec 5, 2023 · 0fab215 · 0fab215
1 parent 4aa7ab0
commit 0fab215
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 7 deletions.
diff --git a/Logic/FirstOrder/Incompleteness/FirstIncompleteness.lean b/Logic/FirstOrder/Incompleteness/FirstIncompleteness.lean
@@ -53,7 +53,7 @@ local notation "γ" => undecidable T
 
 lemma diagRefutation_spec (σ : Subsentence ℒₒᵣ 1) :
     T ⊢! ρ/[⸢σ⸣] ↔ T ⊢! ~σ/[⸢σ⸣] := by
-  simpa[diagRefutation] using pred_representation (diagRefutation_re T) (x := σ)
+  simpa[diagRefutation] using pred_representation T (diagRefutation_re T) (x := σ)
 
 lemma independent : System.Independent T γ := by
   have h : T ⊢! γ ↔ T ⊢! ~γ := by simpa using diagRefutation_spec T ρ

diff --git a/...c/FirstOrder/Incompleteness/Diagonal.lean → ...stOrder/Incompleteness/SelfReference.lean b/...c/FirstOrder/Incompleteness/Diagonal.lean → ...stOrder/Incompleteness/SelfReference.lean
@@ -7,7 +7,7 @@ namespace FirstOrder
 
 namespace Arith
 
-namespace Diagonal
+namespace SelfReference
 
 variable {T : Theory ℒₒᵣ} [EqTheory T] [PAminus T] [DecidablePred T] [SigmaOneSound T] [Theory.Computable T]
 
@@ -16,10 +16,13 @@ open Encodable Subformula
 noncomputable def fsbs : Subsentence ℒₒᵣ 3 :=
   graphTotal₂ (fun (σ π : Subsentence ℒₒᵣ 1) => σ/[(⸢π⸣ : Subterm ℒₒᵣ Empty 0)])
 
-lemma sbs_spec (σ π : Subsentence ℒₒᵣ 1) :
+lemma fsbs_spec (σ π : Subsentence ℒₒᵣ 1) :
     T ⊢! ∀' (fsbs/[#0, ⸢σ⸣, ⸢π⸣] ⟷ “#0 = !!⸢σ/[(⸢π⸣ : Subterm ℒₒᵣ Empty 0)]⸣”) :=
   representation_computable₂ T (f := fun (σ π : Subsentence ℒₒᵣ 1) => σ/[(⸢π⸣ : Subterm ℒₒᵣ Empty 0)])
-    (by sorry) σ π
+    (Primrec₂.to_comp <| (Subformula.substs₁_primrec (L := ℒₒᵣ)).comp₂
+      ((Subterm.Operator.const_primrec (L := ℒₒᵣ)).comp₂ <|
+        (Subterm.Operator.numeral_primrec (L := ℒₒᵣ)).comp₂ $ Primrec.encode.comp₂ .right) <|
+        .left) σ π
 
 noncomputable def diag (θ : Subsentence ℒₒᵣ 1) : Subsentence ℒₒᵣ 1 :=
   ∀' (fsbs/[#0, #1, #1] ⟶ θ/[#0])
@@ -31,15 +34,15 @@ lemma substs_diag (θ σ : Subsentence ℒₒᵣ 1) :
     (diag θ)/[(⸢σ⸣ : Subterm ℒₒᵣ Empty 0)] = ∀' (fsbs/[#0, ⸢σ⸣, ⸢σ⸣] ⟶ θ/[#0]) := by
   simp[diag, Rew.q_substs, ←Rew.hom_comp_app, Rew.substs_comp_substs]
 
-theorem fixpoint_spec (θ : Subsentence ℒₒᵣ 1) :
+theorem main (θ : Subsentence ℒₒᵣ 1) :
     T ⊢! fixpoint θ ⟷ θ/[⸢fixpoint θ⸣] :=
   Complete.consequence_iff_provable.mp (consequence_of _ _ (fun M _ _ _ _ _ => by
     haveI : Theory.Mod M (Theory.PAminus ℒₒᵣ) :=
       Theory.Mod.of_subtheory (T₁ := T) M (Semantics.ofSystemSubtheory _ _)
     have hfsbs : ∀ σ π : Subsentence ℒₒᵣ 1, ∀ z,
         PVal! M ![z, encode σ, encode π] fsbs ↔ z = encode (σ/[(⸢π⸣ : Subterm ℒₒᵣ Empty 0)]) := by
       simpa[models_iff, Subformula.eval_substs, Matrix.comp_vecCons', Matrix.constant_eq_singleton] using
-      fun σ π => consequence_iff'.mp (Sound.sound' (sbs_spec (T := T) σ π)) M
+      fun σ π => consequence_iff'.mp (Sound.sound' (fsbs_spec (T := T) σ π)) M
     simp[models_iff, Subformula.eval_substs, Matrix.comp_vecCons']
     suffices : PVal! M ![] (fixpoint θ) ↔ PVal! M ![encode (fixpoint θ)] θ
     · simpa[Matrix.constant_eq_singleton] using this
@@ -53,7 +56,7 @@ theorem fixpoint_spec (θ : Subsentence ℒₒᵣ 1) :
     _ ↔ PVal! M ![encode $ ∀' (fsbs/[#0, ⸢diag θ⸣, ⸢diag θ⸣] ⟶ θ/[#0])] θ         := by rw[substs_diag]
     _ ↔ PVal! M ![encode (fixpoint θ)] θ                                           := by rfl))
 
-end Diagonal
+end SelfReference
 
 
 end Arith