rest

Author: SnO2WMaN

Foundation/FirstOrder/Incompleteness/ProvabilityAbstraction/Basic.lean

@@ -52,19 +52,19 @@ variable
 lemma D1 {𝔅 : Provability T₀ T} {σ :🡒Sent🡒nce L}🡒: T ⊢ σ → T₀ ⊢ 𝔅 σ := fun h ↦ 𝔅.bew_def h
 
 class HBL2 [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L} (𝔅 : Provability T₀ T) where
-  D2 {σ τ : Sentence L} : T₀ ⊢ 𝔅 (σ ➝ τ) ➝ 𝔅 σ ➝ 𝔅 τ
+  D2 {σ τ : Sentence L} : T₀ ⊢ 𝔅 (σ 🡒 τ) 🡒 𝔅 σ 🡒 𝔅 τ
 export HBL2 (D2)
 
 variable [L.ReferenceableBy L] {T₀🡒T : Theory L} (𝔅 : Provability T₀ T)
 
 class HBL3 where
-  D3 {σ : Sentence L} : T₀ ⊢ 𝔅 σ ➝ 𝔅 (𝔅 σ)
+  D3 {σ : Sentence L} : T₀ ⊢ 𝔅 σ 🡒 𝔅 (𝔅 σ)
 export HBL3 (D3)
 
-class HBL extends 𝔅.HBL2, 𝔅.HBL3🡒🡒
+class HBL extends 𝔅.HBL2, 𝔅.HBL3
 
 class Mono [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L} (𝔅 : Provability T₀ T) where
-  mono {σ τ : Sentence L} : T ⊢ σ ➝ τ → T₀ ⊢ 𝔅 σ ➝ 𝔅 τ
+  mono {σ τ : Sentence L} : T ⊢ σ 🡒 τ → T₀ ⊢ 𝔅 σ 🡒 𝔅 τ
 export Mono (mono)
 
 class Ext [L.ReferenceableBy L₀] 🡒T₀ : Theory L₀} {T : Theory L} (𝔅 : Provability T₀ T) where
@@ -82,7 +82,7 @@ export Rosser (Ros)
   example: `[∀ σ ∈ 𝚺₁, 𝔅.FormalizedCompleteOn σ]` for formalized `𝚺₁`-completeness.
 -/
 class FormalizedCompleteOn (𝔅 : Provability T₀ T) (σ) where
-  formalized_complete_on : T₀ ⊢ σ ➝ 𝔅 σ
+  formalized_complete_on : T₀ ⊢ σ 🡒 𝔅 σ
 export FormalizedCompleteOn (formalized_complete_on)
 attribute [simp, grind .] formalized_complete_on
 🡒
@@ -123,43 +123,43 @@ variable
   {𝔅 : Provability T₀ T}
   {σ τ : Sentence L}
 
-lemma bew_distribute_imply [𝔅.HBL2] (h : T₀ ⊢ 𝔅 (σ ➝ τ)) : T₀ ⊢ 𝔅 σ ➝ 𝔅 τ := D2 ⨀ h
+lemma bew_distribute_imply [𝔅.HBL2] (h : T₀ ⊢ 𝔅 (σ 🡒 τ)) : T₀ ⊢ 𝔅 σ 🡒 𝔅 τ := D2 ⨀ h
 
 instance [𝔅.HBL2] : 𝔅.Mono := ⟨λ h => bew_distribute_imply $ D1 h⟩
 instance [𝔅.HBL2] : 𝔅.Ext := ⟨λ h => E!_intro (mono (K!_left h)) (mono (K!_right h))⟩
 
-lemma bew_distribute_and [𝔅.HBL2] [L₀.DecidableEq] : T₀ ⊢ 𝔅 (σ ⋏ τ) ➝ 𝔅 σ ⋏ 𝔅 τ := by
-  have h₁ : T₀ ⊢ 𝔅 (σ ⋏ τ) ➝ 𝔅 σ := bew_distribute_imply $ D1 and₁!;
-  have h₂ : T₀ ⊢ 𝔅 (σ ⋏ τ) ➝ 𝔅 τ := bew_distribute_imply $ D1 and₂!;
+lemma bew_distribute_and [𝔅.HBL2] [L₀.DecidableEq] : T₀ ⊢ 𝔅 (σ ⋏ τ) 🡒 𝔅 σ ⋏ 𝔅 τ := by
+  have h₁ : T₀ ⊢ 𝔅 (σ ⋏ τ) 🡒 𝔅 σ := bew_distribute_imply $ D1 and₁!;
+  have h₂ : T₀ ⊢ 𝔅 (σ ⋏ τ) 🡒 𝔅 τ := bew_distribute_imply $ D1 and₂!;
   cl_prover [h₁, h₂];
 
 lemma bew_distribute_and' [𝔅.HBL2] [L₀.DecidableEq] : T₀ ⊢ 𝔅 (σ ⋏ τ) → T₀ ⊢ 𝔅 σ ⋏ 𝔅 τ := λ h => bew_distribute_and ⨀ h
-🡒🡒
-lemma bew_collect_and [𝔅.HBL2] [L₀.DecidableEq] [L.DecidableEq] : T₀ ⊢ 𝔅 σ ⋏ 𝔅 τ ➝ 𝔅 (σ ⋏ τ) := by
-  have h₁ : T₀ ⊢ 𝔅 σ ➝ 𝔅 (τ ➝ σ ⋏ τ) := 𝔅.mono $ by cl_prover
-  have h₂ : T₀ ⊢ 𝔅 (τ ➝ σ ⋏ τ) ➝ 𝔅 τ ➝ 𝔅 (σ ⋏ τ) := D2;
-  cl_prover [h₁, h₂];🡒🡒
+
+lemma bew_collect_and [𝔅.HBL2] [L₀.DecidableEq] [L.DecidableEq] : T₀ ⊢ 𝔅 σ ⋏ 𝔅 τ 🡒 𝔅 (σ ⋏ τ) := by
+  have h₁ : T₀ ⊢ 𝔅 σ 🡒 𝔅 (τ 🡒 σ ⋏ τ) := 𝔅.mono $ by cl_prover
+  have h₂ : T₀ ⊢ 𝔅 (τ 🡒 σ ⋏ τ) 🡒 𝔅 τ 🡒 𝔅 (σ ⋏ τ) := D2;
+  cl_prover [h₁, h₂];
 
 
 lemma dia_mono [L₀.DecidableEq] [L.DecidableEq] [𝔅.Mono]
-  (h : T ⊢ σ ➝ τ) : T₀ ⊢ 𝔅.dia σ ➝ 𝔅.dia τ := by
-  have : T₀ ⊢ 𝔅 (∼τ) ➝ 𝔅 (∼σ) := 𝔅.mono $ by cl_prover [h];
+  (h : T ⊢ σ 🡒 τ) : T₀ ⊢ 𝔅.dia σ 🡒 𝔅.dia τ := by
+  have : T₀ ⊢ 𝔅 (∼τ) 🡒 𝔅 (∼σ) := 𝔅.mono $ by cl_prover [h];
   cl_prover [this]
 
-end🡒🡒
-🡒
+end
+
 section
 
 variable🡒
   [L.ReferenceableBy L] {T₀ 🡒 : Theory L} [T₀ ⪯ T]
   {𝔅 : Provability T₀ T}🡒
   {σ τ : Sentence L}
 
-lemma mono' [𝔅.Mono] (h : T₀ ⊢ σ ➝ τ) : T₀ ⊢ 𝔅 σ ➝ 𝔅 τ := 𝔅.mono $ WeakerThan.pbl h
+lemma mono' [𝔅.Mono] (h : T₀ ⊢ σ 🡒 τ) : T₀ ⊢ 𝔅 σ 🡒 𝔅 τ := 𝔅.mono $ WeakerThan.pbl h
 lemma ext' [𝔅.Ext] (h : T₀ ⊢ σ 🡘 τ) : T₀ ⊢ 𝔅 σ 🡘 𝔅 τ := 𝔅.ext $ WeakerThan.pbl h
-🡒
-end🡒🡒
-🡒🡒🡒
+
+end
+
 end Provability
 
 
@@ -182,13 +182,13 @@ def gödel [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] (
   fixedpoint T₀ “x. ¬!𝔅.prov x”🡒
 
 lemma gödel_spec : T₀ ⊢ (gödel 𝔅) 🡘 ∼𝔅 (gödel 𝔅) := by simpa [gödel] using diag “x. ¬!𝔅.prov x”;
-🡒🡒
+
 section First
 
-variable [L.DecidableEq]🡒🡒
+variable [L.DecidableEq]
 variable [T₀ ⪯ T] [Consistent T]
 
-theorem unprovable_gödel : T ⊬ (gödel 𝔅) := by🡒🡒
+theorem unprovable_gödel : T ⊬ (gödel 𝔅) := by
   intro h;
   have h₁ : T ⊢ 𝔅 (gödel 𝔅) := WeakerThan.pbl $ D1 h;
   have h₂ : T ⊢ (gödel 𝔅) 🡘 ∼𝔅 (gödel 𝔅) := WeakerThan.pbl $ gödel_spec;
@@ -219,23 +219,23 @@ section Second
 variable [𝔅.HBL]
 
 omit [Diagonalization T₀] in
-lemma formalized_consistent_of_existance_unprovable [L.DecidableEq] : T₀ ⊢ ∼𝔅 σ ➝ 𝔅.con := contra! $ mdp! D2 $ D1 efq!
+lemma formalized_consistent_of_existance_unprovable [L.DecidableEq] : T₀ ⊢ ∼𝔅 σ 🡒 𝔅.con := contra! $ mdp! D2 $ D1 efq!
 
 local notation "𝐆" => gödel 𝔅
 
 variable [L.DecidableEq] [T₀ ⪯ T]
 
 /-- Formalized First Incompleteness Theorem -/
-theorem formalized_unprovable_gödel  : T₀ ⊢ 𝔅.con ➝ ∼𝔅 𝐆 := by
-  suffices T₀ ⊢ ∼𝔅 ⊥ ➝ ∼𝔅 𝐆 from this
-  have h₁ : T₀ ⊢ 𝔅 𝐆 ➝ 𝔅 (𝔅 𝐆) := D3
-  have h₂ : T₀ ⊢ 𝔅 𝐆 ➝ 𝔅 (𝔅 𝐆 ➝ ⊥) := 𝔅.mono' $ by cl_prover [gödel_spec (T₀ := T₀)]
-  have h₃ : T₀ ⊢ 𝔅 (𝔅 𝐆 ➝ ⊥) ➝ 𝔅 (𝔅 𝐆) ➝ 𝔅 ⊥ := D2
+theorem formalized_unprovable_gödel  : T₀ ⊢ 𝔅.con 🡒 ∼𝔅 𝐆 := by
+  suffices T₀ ⊢ ∼𝔅 ⊥ 🡒 ∼𝔅 𝐆 from this
+  have h₁ : T₀ ⊢ 𝔅 𝐆 🡒 𝔅 (𝔅 𝐆) := D3
+  have h₂ : T₀ ⊢ 𝔅 𝐆 🡒 𝔅 (𝔅 𝐆 🡒 ⊥) := 𝔅.mono' $ by cl_prover [gödel_spec (T₀ := T₀)]
+  have h₃ : T₀ ⊢ 𝔅 (𝔅 𝐆 🡒 ⊥) 🡒 𝔅 (𝔅 𝐆) 🡒 𝔅 ⊥ := D2
   cl_prover [h₁, h₂, h₃]
 
 theorem gödel_iff_con : T₀ ⊢ 𝐆 🡘 𝔅.con := by
-  have h₁ : T₀ ⊢ ∼𝔅 𝐆 ➝ 𝔅.con := formalized_consistent_of_existance_unprovable
-  have h₂ : T₀ ⊢ 𝔅.con ➝ ∼𝔅 𝐆 := formalized_unprovable_gödel
+  have h₁ : T₀ ⊢ ∼𝔅 𝐆 🡒 𝔅.con := formalized_consistent_of_existance_unprovable
+  have h₂ : T₀ ⊢ 𝔅.con 🡒 ∼𝔅 𝐆 := formalized_unprovable_gödel
   have h₃ : T₀ ⊢ 𝐆 🡘 ∼𝔅 𝐆 := gödel_spec
   cl_prover [h₁, h₂, h₃];
 
@@ -255,51 +255,51 @@ theorem con_independent [Consistent T] [𝔅.Kreisel] : Independent T 𝔅.con :
   constructor🡒
   . apply con_unprovab🡒e
   . apply con_unrefutab🡒e
-🡒🡒
+
 end Second
-🡒🡒🡒
+
 
 section Löb
 
 def kreisel [Diagonaliza🡒ion T₀] (𝔅 : Provability T₀ T) (σ : Sentence L) : Sentence L := fixedpoint T₀ “x. !𝔅.prov x → !σ”
-🡒
+
 variable {σ : Sentence L}
 
 local notation "𝐊" => kreisel 𝔅
 
-lemma kreisel_spec : T₀ ⊢ (𝐊 σ) 🡘 (𝔅 (𝐊 σ) ➝ σ) := by
+lemma kreisel_spec : T₀ ⊢ (𝐊 σ) 🡘 (𝔅 (𝐊 σ) 🡒 σ) := by
   simpa [kreisel, Rew.subst_comp_subst, ←TransitiveRewriting.comp_app] using diag “x. !𝔅.prov x → !σ”;
 
-private lemma kreisel_specAux₂ : T₀ ⊢ (𝔅 (𝐊 σ) ➝ σ) ➝ (𝐊 σ) := K!_right kreisel_spec
+private lemma kreisel_specAux₂ : T₀ ⊢ (𝔅 (𝐊 σ) 🡒 σ) 🡒 (𝐊 σ) := K!_right kreisel_spec
 
 variable [𝔅.HBL]
 
-private lemma kreisel_specAux₁ [L.DecidableEq] [T₀ ⪯ T] : T₀ ⊢ 𝔅 (𝐊 σ) ➝ 𝔅 σ :=
+private lemma kreisel_specAux₁ [L.DecidableEq] [T₀ ⪯ T] : T₀ ⊢ 𝔅 (𝐊 σ) 🡒 𝔅 σ :=
   Entailment.mdp₁! (C!_trans (mdp! D2 (D1 (WeakerThan.pbl <| K!_left (kreisel_spec)))) D2) D3
 
 variable [L.DecidableEq] [T₀ ⪯ T]
 
-theorem löb_theorem (H : T ⊢ 𝔅 σ ➝ σ) : T ⊢ σ := by
-  have d₁ : T ⊢ 𝔅 (𝐊 σ) ➝ σ := C!_trans (WeakerThan.pbl kreisel_specAux₁) H;
+theorem löb_theorem (H : T ⊢ 𝔅 σ 🡒 σ) : T ⊢ σ := by
+  have d₁ : T ⊢ 𝔅 (𝐊 σ) 🡒 σ := C!_trans (WeakerThan.pbl kreisel_specAux₁) H;
   have d₂ : T ⊢ 𝔅 (𝐊 σ)     := WeakerThan.pbl $ D1 $ WeakerThan.pbl kreisel_specAux₂ ⨀ d₁;
   exact d₁ ⨀ d₂;
 
-theorem formalized_löb_theorem : T₀ ⊢ 𝔅 (𝔅 σ ➝ σ) ➝ 𝔅 σ := by
-  have h₁ : T₀ ⊢ 𝔅 (𝐊 σ) ➝ 𝔅 σ := kreisel_specAux₁;
-  have h₂ : T₀ ⊢ (𝔅 σ ➝ σ) ➝ (𝔅 (𝐊 σ) ➝ σ) := CCC!_of_C!_left h₁;
-  have h₃ : T ⊢ (𝔅 σ ➝ σ) ➝ 𝐊 σ := WeakerThan.pbl $ C!_trans (CCC!_of_C!_left h₁) kreisel_specAux₂;
+theorem formalized_löb_theorem : T₀ ⊢ 𝔅 (𝔅 σ 🡒 σ) 🡒 𝔅 σ := by
+  have h₁ : T₀ ⊢ 𝔅 (𝐊 σ) 🡒 𝔅 σ := kreisel_specAux₁;
+  have h₂ : T₀ ⊢ (𝔅 σ 🡒 σ) 🡒 (𝔅 (𝐊 σ) 🡒 σ) := CCC!_of_C!_left h₁;
+  have h₃ : T ⊢ (𝔅 σ 🡒 σ) 🡒 𝐊 σ := WeakerThan.pbl $ C!_trans (CCC!_of_C!_left h₁) kreisel_specAux₂;
   exact C!_trans (D2 ⨀ (D1 h₃)) h₁;
 
-lemma formalized_unprovable_not_con [Consistent T] [𝔅.Kreisel] : T ⊬ 𝔅.con ➝ ∼𝔅 (∼𝔅.con) := by
+lemma formalized_unprovable_not_con [Consistent T] [𝔅.Kreisel] : T ⊬ 𝔅.con 🡒 ∼𝔅 (∼𝔅.con) := by
   by_contra hC;
   have : T ⊢ ∼𝔅.con := löb_theorem $ CN!_of_C🡒!_right hC;
   have : T ⊬ ∼𝔅.con := con_unrefutable;
   contradiction;
-🡒🡒
-lemma formalized_unrefutable_gödel [Consistent T] [𝔅.Kreisel] : T ⊬ 𝔅.con ➝ ∼𝔅 (∼(gödel 𝔅)) := by
+
+lemma formalized_unrefutable_gödel [Consistent T] [𝔅.Kreisel] : T ⊬ 𝔅.con 🡒 ∼𝔅 (∼(gödel 𝔅)) := by
   by_contra hC;
-  have : T ⊬ 𝔅.con ➝ ∼𝔅 (∼𝔅.con) := formalized_unprovable_not_con;
-  have : T ⊢ 𝔅.con ➝ ∼𝔅 (∼𝔅.con) := C!_trans hC🡒
+  have : T ⊬ 𝔅.con 🡒 ∼𝔅 (∼𝔅.con) := formalized_unprovable_not_con;
+  have : T ⊢ 𝔅.con 🡒 ∼𝔅 (∼𝔅.con) := C!_trans hC🡒
     $ WeakerThan.pbl
     $ K!_left $ ENN!_of_E!
     $ 𝔅.ext
@@ -311,9 +311,9 @@ end Löb
 
 
 section Rosser
-🡒🡒
+
 variable {T₀ T : Theory L} 🡒Diagonalization T₀] [T₀ ⪯ T] [Consistent T] {𝔅 : Provability T₀ T}
-🡒🡒🡒
+
 local notation "𝐑"🡒=> g🡒del 𝔅
 
 theorem unrefutable_rosser [𝔅.Rosser] : T ⊬ ∼𝐑 := by
@@ -327,7 +327,7 @@ theorem rosser_independent [L.DecidableEq] [𝔅.Rosser] : Independent T 𝐑 :=
   constructor
   . apply unprovable_gödel
   . apply unrefutable_rosser
-🡒
+
 theorem rosser_first_incompleteness [L.DecidableEq] (𝔅 : Provability T₀ T) [𝔅.Rosser] : Incomplete T :=
   incomplete_def.mpr ⟨gödel 𝔅, rosser_independent⟩
 
@@ -336,7 +336,7 @@ omit [Diagonalization T₀] [Consistent T] in
 theorem kreisel_remark [𝔅.Rosser] : T ⊢ 𝔅.con := by🡒
   have : T₀ ⊢ ∼𝔅 ⊥ := Ros (N!_iff_CO!.mpr (by simp));
   exact WeakerThan.p🡒l $ this;
-🡒
+
 end Rosser
 
 end ProvabilityAbstraction

Foundation/FirstOrder/Incompleteness/ProvabilityAbstraction/Height.lean

@@ -35,9 +35,9 @@ lemma boxBot_monotone [T₀ ⪯ T] [𝔅.HBL] : n ≤ m → T ⊢ 𝔅^[n] ⊥ 
       match n with
       | 0 => simp;
       | n + 1 =>
-        have : T ⊢ 𝔅 ((𝔅)^[n] 🡒) ➝ 𝔅 (𝔅 ((𝔅)^[n] ⊥)) := Entailment.WeakerThan.pbl $ 𝔅.D3;
+        have : T ⊢ 𝔅 ((𝔅)^[n] 🡒) 🡒 𝔅 (𝔅 ((𝔅)^[n] ⊥)) := Entailment.WeakerThan.pbl $ 𝔅.D3;
         simpa only [Function.iterate_succ_apply'] using this
-    have b₁ : T ⊢ 𝔅 (𝔅^[n] ⊥) ➝ 𝔅 (𝔅^[n + k] ⊥) := Entailment.WeakerThan.pbl $ 𝔅.mono ih;
+    have b₁ : T ⊢ 𝔅 (𝔅^[n] ⊥) 🡒 𝔅 (𝔅^[n + k] ⊥) := Entailment.WeakerThan.pbl $ 𝔅.mono ih;
     cl_prover [b₀, b₁]
 
 lemma iIncon_unprovable_of_sigma1_sound [𝔅.Kreisel] [Entailment.Consistent T] : ∀ n, T ⊬ 𝔅^[n] ⊥

Foundation/FirstOrder/Incompleteness/StandardProvability.lean

@@ -67,9 +67,9 @@ theorem provable_D3 [𝗣𝗔⁻ ⪯ T] {σ : Sentence ℒₒᵣ} :
 
 open LO.Entailment LO.Entailment.FiniteContext
 
-lemma provable_D2_context [𝗜𝚺₁ ⪯ U] {Γ σ π} (hσπ : Γ ⊢[U] □(σ ➝ π)) (hσ : Γ ⊢[U] □σ) :
+lemma provable_D2_context [𝗜𝚺₁ ⪯ U] {Γ σ π} (hσπ : Γ ⊢[U] □(σ 🡒 π)) (hσ : Γ ⊢[U] □σ) :
     Γ ⊢[U] □π := FiniteContext.of'! (weakening inferInstance provable_D2) ⨀! hσπ ⨀! hσ
-🡒
+
 lemma provable_D3_context [𝗣𝗔⁻ ⪯ T] [𝗜𝚺₁ ⪯ U] {Γ σ} (hσπ : Γ ⊢[U] □σ) :
   Γ ⊢[U] □□σ := FiniteContext.of'! (weakening inferInstance provable_D3) ⨀! hσπ
 
@@ -89,10 +89,10 @@ instance [T.SoundOnHierarchy 𝚺 1] : T.standardProvability.Kreisel := ⟨fun h
 open LO.Entailment in
 /--
   If `π` is equivalent to some 𝚺₁ sentence `σ`,
-  then `π ➝ □π` is provable in `T` (note: not `𝗜𝚺₁`, compare `provable_sigma_one_complete`)
+  then `π 🡒 □π` is provable in `T` (note: not `𝗜𝚺₁`, compare `provable_sigma_one_complete`)
 -/
 lemma prov🡒ble_sigma_one_complete_of_E {σ π} [𝗜𝚺₁ ⪯ T]
-  (hσ : Hierarchy 𝚺 1 σ) (hσπ : 𝗜𝚺₁ ⊢ σ 🡘 π) : 𝗜𝚺₁ ⊢ π ➝ □π := by
+  (hσ : Hierarchy 𝚺 1 σ) (hσπ : 𝗜𝚺₁ ⊢ σ 🡘 π) : 𝗜𝚺₁ ⊢ π 🡒 □π := by
   apply C!_replace ?_ ?_ $ provable_sigma_one_complete (T := T) $ hσ;
   . cl_prover [hσπ];🡒
   . apply T.standardProvability.mono';