refactor(Incompleteness): Provability Abstraction Pt.3 (#797)

Author: SnO2WMaN

Foundation/FirstOrder/Incompleteness/ProvabilityAbstraction/Basic.lean

@@ -10,6 +10,7 @@ public import Foundation.Meta.ClProver
 
 namespace LO
 
+open LO.Entailment
 
 namespace FirstOrder
 
@@ -22,7 +23,7 @@ namespace ProvabilityAbstraction
 structure Provability [L.ReferenceableBy L₀] (T₀ : Theory L₀) (T : Theory L) where
   prov : Semisentence L₀ 1
   /-- Derivability condition `D1` -/
-  prov_def {σ : Sentence L} : T ⊢ σ → T₀ ⊢ prov/[⌜σ⌝]
+  bew_def {σ : Sentence L} : T ⊢ σ → T₀ ⊢ prov/[⌜σ⌝]
 
 namespace Provability
 
@@ -38,15 +39,17 @@ abbrev dia (𝔅 : Provability T₀ T) (φ : Sentence L) : Sentence L₀ := ∼
 end Provability
 
 
+section
+
+namespace Provability
+
 section
 
 variable
   {L₀ L : Language} [L.ReferenceableBy L₀]
   {T₀ : Theory L₀} {T : Theory L}
 
-lemma D1 {𝔅 : Provability T₀ T} {σ : Sentence L} : T ⊢ σ → T₀ ⊢ 𝔅 σ := fun h ↦ 𝔅.prov_def h
-
-namespace Provability
+lemma D1 {𝔅 : Provability T₀ T} {σ : Sentence 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₀ ⊢ 𝔅 (σ ➝ τ) ➝ 𝔅 σ ➝ 𝔅 τ
@@ -62,70 +65,56 @@ 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₀ ⊢ 𝔅 σ ➝ 𝔅 τ
+export Mono (mono)
 
-class Equiv [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L} (𝔅 : Provability T₀ T) where
-  equiv {σ τ : Sentence L} : T ⊢ σ ⭤ τ → T₀ ⊢ 𝔅 σ ⭤ 𝔅 τ
-
-class Löb where
-  LT {σ : Sentence L} : T ⊢ 𝔅 σ ➝ σ → T ⊢ σ
-export Löb (LT)
-
-class FormalizedLöb where
-  FLT {σ : Sentence L} : T₀ ⊢ 𝔅 (𝔅 σ ➝ σ) ➝ 𝔅 σ
-export FormalizedLöb (FLT)
+class Ext [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L} (𝔅 : Provability T₀ T) where
+  ext {σ τ : Sentence L} : T ⊢ σ ⭤ τ → T₀ ⊢ 𝔅 σ ⭤ 𝔅 τ
+export Ext (ext)
 
 class Rosser [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L} (𝔅 : Provability T₀ T) where
   Ros {σ : Sentence L} : T ⊢ ∼σ → T₀ ⊢ ∼𝔅 σ
 export Rosser (Ros)
 
 
 /--
-  Abstract version of formalized `Γ`-completeness for provability `𝔅`
+  Abstract version of formalized `Γ`-completeness for provability `𝔅`.
 
-  example: `[∀ σ ∈ 𝚺₁, 𝔅.FormalizedCompleteOn σ]` for formalized `𝚺₁`-completeness
+  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
 
+instance [∀ σ, 𝔅.FormalizedCompleteOn (𝔅 σ)] : 𝔅.HBL3 := ⟨by simp⟩
+
 /--
   NOTE: Named after [Vis21].
 -/
-class Kreisel [L.ReferenceableBy L] {T₀ T : Theory L} (𝔅 : Provability T₀ T) (σ) where
-  KR : T ⊢ 𝔅 σ → T ⊢ σ
+class Kreisel [L.ReferenceableBy L] {T₀ T : Theory L} (𝔅 : Provability T₀ T) where
+  KR {σ : Sentence L} : T ⊢ 𝔅 σ → T ⊢ σ
 export Kreisel (KR)
 attribute [simp, grind .] KR
 
-class WeakKreisel [L.ReferenceableBy L] {T₀ T : Theory L} (𝔅 : Provability T₀ T) (σ) where
-  WKR : T₀ ⊢ 𝔅 σ → T ⊢ σ
-export WeakKreisel (WKR)
-attribute [simp, grind .] WKR
-
 
 class SoundOn
   [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L}
-  (𝔅 : Provability T₀ T)
-  (M : outParam Type*) [Nonempty M] [Structure L₀ M]
-  (σ)
+  (𝔅 : Provability T₀ T) (M : outParam Type*) [Nonempty M] [Structure L₀ M]
   where
-  sound_on : M ⊧ₘ 𝔅 σ → T ⊢ σ
+  sound_on {σ} : M ⊧ₘ 𝔅 σ → T ⊢ σ
 export SoundOn (sound_on)
 attribute [simp, grind .] sound_on
 
-
-instance [Nonempty M] [Structure L M] [𝔅.SoundOn M σ] [M ⊧ₘ* T₀] : 𝔅.WeakKreisel σ where
-  WKR h := SoundOn.sound_on $ models_of_provable inferInstance h;
-
-end Provability
-
+lemma syntactical_sound (M) [Nonempty M] [Structure L M] [SoundOn 𝔅 M] [M ⊧ₘ* T₀] : ∀ {σ}, T₀ ⊢ 𝔅 σ → T ⊢ σ := by
+  intro σ h;
+  apply 𝔅.sound_on;
+  apply models_of_provable (T := T₀);
+  . infer_instance;
+  . exact h;
 
 end
 
 
-open LO.Entailment
-open Provability
-
 section
 
 variable
@@ -134,34 +123,29 @@ variable
   {𝔅 : Provability T₀ T}
   {σ τ : Sentence L}
 
-lemma D2' [𝔅.HBL2] : T₀ ⊢ 𝔅 (σ ➝ τ) → T₀ ⊢ 𝔅 σ ➝ 𝔅 τ := by
-  intro h;
-  exact D2 ⨀ h;
+lemma bew_distribute_imply [𝔅.HBL2] (h : T₀ ⊢ 𝔅 (σ ➝ τ)) : T₀ ⊢ 𝔅 σ ➝ 𝔅 τ := D2 ⨀ h
 
-lemma prov_distribute_imply [𝔅.HBL2] (h : T ⊢ σ ➝ τ) : T₀ ⊢ 𝔅 σ ➝ 𝔅 τ := D2' $ D1 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 prov_distribute_iff [𝔅.HBL2] (h : T ⊢ σ ⭤ τ) : T₀ ⊢ 𝔅 σ ⭤ 𝔅 τ := by
-  apply E!_intro;
-  . exact prov_distribute_imply $ K!_left h;
-  . exact prov_distribute_imply $ K!_right h;
-
-lemma dia_distribute_imply [L₀.DecidableEq] [L.DecidableEq] [𝔅.HBL2]
-  (h : T ⊢ σ ➝ τ) : T₀ ⊢ 𝔅.dia σ ➝ 𝔅.dia τ := by
-  have : T₀ ⊢ 𝔅 (∼τ) ➝ 𝔅 (∼σ) := prov_distribute_imply $ by cl_prover [h];
-  cl_prover [this]
-
-lemma prov_distribute_and [𝔅.HBL2] [L₀.DecidableEq] : T₀ ⊢ 𝔅 (σ ⋏ τ) ➝ 𝔅 σ ⋏ 𝔅 τ := by
-  have h₁ : T₀ ⊢ 𝔅 (σ ⋏ τ) ➝ 𝔅 σ := D2' $ D1 and₁!;
-  have h₂ : T₀ ⊢ 𝔅 (σ ⋏ τ) ➝ 𝔅 τ := D2' $ 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 prov_distribute_and' [𝔅.HBL2] [L₀.DecidableEq] : T₀ ⊢ 𝔅 (σ ⋏ τ) → T₀ ⊢ 𝔅 σ ⋏ 𝔅 τ := λ h => prov_distribute_and ⨀ h
+lemma bew_distribute_and' [𝔅.HBL2] [L₀.DecidableEq] : T₀ ⊢ 𝔅 (σ ⋏ τ) → T₀ ⊢ 𝔅 σ ⋏ 𝔅 τ := λ h => bew_distribute_and ⨀ h
 
-lemma prov_collect_and [𝔅.HBL2] [L₀.DecidableEq] [L.DecidableEq] : T₀ ⊢ 𝔅 σ ⋏ 𝔅 τ ➝ 𝔅 (σ ⋏ τ) := by
-  have h₁ : T₀ ⊢ 𝔅 σ ➝ 𝔅 (τ ➝ σ ⋏ τ) := prov_distribute_imply $ by cl_prover
+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];
+  cl_prover [this]
+
 end
 
 section
@@ -171,27 +155,17 @@ variable
   {𝔅 : Provability T₀ T}
   {σ τ : Sentence L}
 
-lemma D1_shift : T ⊢ σ → T ⊢ 𝔅 σ := by
-  intro h;
-  apply Entailment.WeakerThan.pbl (𝓢 := T₀);
-  apply D1 h;
+lemma mono' [𝔅.Mono] (h : T₀ ⊢ σ ➝ τ) : T₀ ⊢ 𝔅 σ ➝ 𝔅 τ := 𝔅.mono $ WeakerThan.pbl h
+lemma ext' [𝔅.Ext] (h : T₀ ⊢ σ ⭤ τ) : T₀ ⊢ 𝔅 σ ⭤ 𝔅 τ := 𝔅.ext $ WeakerThan.pbl h
 
-lemma D2_shift [𝔅.HBL2] : T ⊢ 𝔅 (σ ➝ τ) ➝ 𝔅 σ ➝ 𝔅 τ := by
-  apply Entailment.WeakerThan.pbl (𝓢 := T₀) $ D2;
+end
 
-lemma D3_shift [𝔅.HBL3] : T ⊢ 𝔅 σ ➝ 𝔅 (𝔅 σ) := by
-  apply Entailment.WeakerThan.pbl (𝓢 := T₀) $ D3;
+end Provability
 
-lemma FLT_shift [𝔅.FormalizedLöb] : T ⊢ 𝔅 (𝔅 σ ➝ σ) ➝ 𝔅 σ := by
-  apply Entailment.WeakerThan.pbl (𝓢 := T₀) $ FLT;
 
-lemma prov_distribute_imply' [𝔅.HBL2] (h : T₀ ⊢ σ ➝ τ) : T₀ ⊢ 𝔅 σ ➝ 𝔅 τ :=
-  prov_distribute_imply $ WeakerThan.pbl h
+end
 
-lemma prov_distribute_imply'' [𝔅.HBL2] (h : T ⊢ σ ➝ τ) : T ⊢ 𝔅 σ ➝ 𝔅 τ :=
-  WeakerThan.pbl $ prov_distribute_imply h
 
-end
 
 
 class Diagonalization [L.ReferenceableBy L] (T : Theory L) where
@@ -216,25 +190,25 @@ variable [T₀ ⪯ T] [Consistent T]
 
 theorem unprovable_gödel : T ⊬ (gödel 𝔅) := by
   intro h;
-  have h₁ : T ⊢ 𝔅 (gödel 𝔅) := D1_shift h;
+  have h₁ : T ⊢ 𝔅 (gödel 𝔅) := WeakerThan.pbl $ D1 h;
   have h₂ : T ⊢ (gödel 𝔅) ⭤ ∼𝔅 (gödel 𝔅) := WeakerThan.pbl $ gödel_spec;
   have : T ⊢ ⊥ := by cl_prover [h₁, h₂, h];
   have : ¬Consistent T := not_consistent_iff_inconsistent.mpr <| inconsistent_iff_provable_bot.mpr this;
   contradiction
 
-theorem unrefutable_gödel [𝔅.Kreisel (gödel 𝔅)] : T ⊬ ∼(gödel 𝔅) := by
+theorem unrefutable_gödel [𝔅.Kreisel] : T ⊬ ∼(gödel 𝔅) := by
   intro h₂;
   have h₁ : T ⊢ (gödel 𝔅) := WeakerThan.pbl $ 𝔅.KR $ by cl_prover [gödel_spec (T₀ := T₀), h₂];
   have : T ⊢ ⊥ := (N!_iff_CO!.mp $ WeakerThan.pbl $ h₂) ⨀ h₁;
   have : ¬Consistent T := not_consistent_iff_inconsistent.mpr <| inconsistent_iff_provable_bot.mpr this
   contradiction;
 
-theorem gödel_independent [𝔅.Kreisel (gödel 𝔅)] : Independent T (gödel 𝔅) := by
+theorem gödel_independent [𝔅.Kreisel] : Independent T (gödel 𝔅) := by
   constructor
   . apply unprovable_gödel
   . apply unrefutable_gödel
 
-theorem first_incompleteness [𝔅.Kreisel (gödel 𝔅)] : Incomplete T :=
+theorem first_incompleteness [𝔅.Kreisel] : Incomplete T :=
   incomplete_def.mpr ⟨(gödel 𝔅), gödel_independent⟩
 
 end First
@@ -255,8 +229,7 @@ variable [L.DecidableEq] [T₀ ⪯ T]
 theorem formalized_unprovable_gödel  : T₀ ⊢ 𝔅.con ➝ ∼𝔅 𝐆 := by
   suffices T₀ ⊢ ∼𝔅 ⊥ ➝ ∼𝔅 𝐆 from this
   have h₁ : T₀ ⊢ 𝔅 𝐆 ➝ 𝔅 (𝔅 𝐆) := D3
-  have h₂ : T₀ ⊢ 𝔅 𝐆 ➝ 𝔅 (𝔅 𝐆 ➝ ⊥) := prov_distribute_imply $ by
-    cl_prover [gödel_spec (T₀ := T₀)]
+  have h₂ : T₀ ⊢ 𝔅 𝐆 ➝ 𝔅 (𝔅 𝐆 ➝ ⊥) := 𝔅.mono' $ by cl_prover [gödel_spec (T₀ := T₀)]
   have h₃ : T₀ ⊢ 𝔅 (𝔅 𝐆 ➝ ⊥) ➝ 𝔅 (𝔅 𝐆) ➝ 𝔅 ⊥ := D2
   cl_prover [h₁, h₂, h₃]
 
@@ -272,13 +245,13 @@ theorem con_unprovable [Consistent T] : T ⊬ 𝔅.con := by
   have : T ⊢ 𝐆 := by cl_prover [h, this]
   exact unprovable_gödel this
 
-theorem con_unrefutable [Consistent T] [𝔅.Kreisel (gödel 𝔅)] : T ⊬ ∼𝔅.con := by
+theorem con_unrefutable [Consistent T] [𝔅.Kreisel] : T ⊬ ∼𝔅.con := by
   intro h
-  have : T₀ ⊢ 𝐆 ⭤ 𝔅.con := gödel_iff_con
+  have : T ⊢ 𝐆 ⭤ 𝔅.con := WeakerThan.pbl $ gödel_iff_con;
   have : T ⊢ ∼𝐆 := by cl_prover [h, this]
   exact unrefutable_gödel this
 
-theorem con_independent [Consistent T] [𝔅.Kreisel (gödel 𝔅)] : Independent T 𝔅.con := by
+theorem con_independent [Consistent T] [𝔅.Kreisel] : Independent T 𝔅.con := by
   constructor
   . apply con_unprovable
   . apply con_unrefutable
@@ -290,6 +263,8 @@ section Löb
 
 def kreisel [Diagonalization T₀] (𝔅 : Provability T₀ T) (σ : Sentence L) : Sentence L := fixedpoint T₀ “x. !𝔅.prov x → !σ”
 
+variable {σ : Sentence L}
+
 local notation "𝐊" => kreisel 𝔅
 
 lemma kreisel_spec : T₀ ⊢ (𝐊 σ) ⭤ (𝔅 (𝐊 σ) ➝ σ) := by
@@ -306,38 +281,30 @@ variable [L.DecidableEq] [T₀ ⪯ T]
 
 theorem löb_theorem (H : T ⊢ 𝔅 σ ➝ σ) : T ⊢ σ := by
   have d₁ : T ⊢ 𝔅 (𝐊 σ) ➝ σ := C!_trans (WeakerThan.pbl kreisel_specAux₁) H;
-  have d₂ : T ⊢ 𝔅 (𝐊 σ)     := WeakerThan.pbl (𝓢 := T₀) (D1 $ WeakerThan.pbl kreisel_specAux₂ ⨀ d₁);
+  have d₂ : T ⊢ 𝔅 (𝐊 σ)     := WeakerThan.pbl $ D1 $ WeakerThan.pbl kreisel_specAux₂ ⨀ d₁;
   exact d₁ ⨀ d₂;
 
-instance : 𝔅.Löb := ⟨löb_theorem⟩
-
 theorem formalized_löb_theorem : T₀ ⊢ 𝔅 (𝔅 σ ➝ σ) ➝ 𝔅 σ := by
   have h₁ : T₀ ⊢ 𝔅 (𝐊 σ) ➝ 𝔅 σ := kreisel_specAux₁;
-  have : T₀ ⊢ (𝔅 σ ➝ σ) ➝ (𝔅 (𝐊 σ) ➝ σ) := CCC!_of_C!_left h₁;
-  have : T ⊢ (𝔅 σ ➝ σ) ➝ 𝐊 σ := WeakerThan.pbl (𝓢 := T₀) $ C!_trans this kreisel_specAux₂;
-  exact C!_trans (D2 ⨀ (D1 this)) h₁;
-
-instance : 𝔅.FormalizedLöb := ⟨formalized_löb_theorem (T := T)⟩
-
-/-
-lemma unprovable_con_via_löb [Consistent T] [L.DecidableEq] [𝔅.Löb] : T ⊬ 𝔅.con := by
-  by_contra hC;
-  have : T ⊢ ⊥ := Löb.LT $ N!_iff_CO!.mp hC;
-  have : ¬Consistent T := not_consistent_iff_inconsistent.mpr $ inconsistent_iff_provable_bot.mpr this
-  contradiction
--/
+  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 (gödel 𝔅)] : T ⊬ 𝔅.con ➝ ∼𝔅 (∼𝔅.con) := by
+lemma formalized_unprovable_not_con [Consistent T] [𝔅.Kreisel] : T ⊬ 𝔅.con ➝ ∼𝔅 (∼𝔅.con) := by
   by_contra hC;
-  have : T ⊢ ∼𝔅.con := Löb.LT $ CN!_of_CN!_right hC;
+  have : T ⊢ ∼𝔅.con := löb_theorem $ CN!_of_CN!_right hC;
   have : T ⊬ ∼𝔅.con := con_unrefutable;
   contradiction;
 
-lemma formalized_unrefutable_gödel [Consistent T] [𝔅.Kreisel (gödel 𝔅)] : 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 $ WeakerThan.pbl <| K!_left <| ENN!_of_E!
-      <| prov_distribute_iff <| ENN!_of_E! <| WeakerThan.pbl gödel_iff_con;
+  have : T ⊢ 𝔅.con ➝ ∼𝔅 (∼𝔅.con) := C!_trans hC
+    $ WeakerThan.pbl
+    $ K!_left $ ENN!_of_E!
+    $ 𝔅.ext
+    $ ENN!_of_E!
+    $ WeakerThan.pbl gödel_iff_con;
   contradiction;
 
 end Löb

Foundation/FirstOrder/Incompleteness/ProvabilityAbstraction/Height.lean

@@ -32,13 +32,15 @@ lemma boxBot_monotone [T₀ ⪯ T] [𝔅.HBL] : n ≤ m → T ⊢ 𝔅^[n] ⊥ 
   case succ k ih =>
     simp only [← add_assoc, Function.iterate_succ_apply']
     have b₀ : T ⊢ 𝔅^[n] ⊥ ➝ 𝔅 (𝔅^[n] ⊥) := by
-      cases n
-      · simp
-      · simpa only [Function.iterate_succ_apply'] using D3_shift
-    have b₁ : T ⊢ 𝔅 (𝔅^[n] ⊥) ➝ 𝔅 (𝔅^[n + k] ⊥) := prov_distribute_imply'' ih
+      match n with
+      | 0 => simp;
+      | n + 1 =>
+        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;
     cl_prover [b₀, b₁]
 
-lemma iIncon_unprovable_of_sigma1_sound [∀ n, 𝔅.Kreisel (𝔅^[n] ⊥)] [Entailment.Consistent T] : ∀ n, T ⊬ 𝔅^[n] ⊥
+lemma iIncon_unprovable_of_sigma1_sound [𝔅.Kreisel] [Entailment.Consistent T] : ∀ n, T ⊬ 𝔅^[n] ⊥
   |     0 => Entailment.consistent_iff_unprovable_bot.mp inferInstance
   | n + 1 => fun h ↦
     have : T ⊢ 𝔅 (𝔅^[n] ⊥) := by simpa [Function.iterate_succ_apply'] using h
@@ -47,15 +49,17 @@ lemma iIncon_unprovable_of_sigma1_sound [∀ n, 𝔅.Kreisel (𝔅^[n] ⊥)] [En
 
 namespace Provability
 
+
 lemma height_eq_top_iff : 𝔅.height = ⊤ ↔ ∀ n, T ⊬ 𝔅^[n] ⊥ := ENat.find_eq_top_iff _
 
 lemma height_le_of_boxBot {n : ℕ} (h : T ⊢ 𝔅^[n] ⊥) : 𝔅.height ≤ n :=
   ENat.find_le (T ⊢ 𝔅^[·] ⊥) n h
 
-lemma height_lt_pos_of_boxBot {n : ℕ} (pos : 0 < n) [𝔅.WeakKreisel (𝔅^[n.pred] ⊥)] (h : T₀ ⊢ 𝔅^[n] ⊥) : 𝔅.height < n := by
+lemma height_lt_pos_of_boxBot (hSound : ∀ {σ}, T₀ ⊢ 𝔅 σ → T ⊢ σ)
+  {n : ℕ} (pos : 0 < n) (h : T₀ ⊢ 𝔅^[n] ⊥) : 𝔅.height < n := by
   have e : n.pred.succ = n := Eq.symm <| (Nat.sub_eq_iff_eq_add pos).mp rfl
   have : T₀ ⊢ 𝔅 (𝔅^[n.pred] ⊥) := by rwa [←Function.iterate_succ_apply' (f := 𝔅), e];
-  have : 𝔅.height ≤ n.pred := height_le_of_boxBot $ 𝔅.WKR this;
+  have : 𝔅.height ≤ n.pred := height_le_of_boxBot $ hSound this
   have : 𝔅.height < n := by
     rw [←e]
     exact lt_of_le_of_lt this <| ENat.coe_lt_coe.mpr <| by simp
@@ -70,7 +74,7 @@ lemma height_le_iff_boxBot [T₀ ⪯ T] [𝔅.HBL] {n : ℕ} :
     exact boxBot_monotone hmn ⨀ hm
   · exact height_le_of_boxBot
 
-lemma height_eq_top_of_sound_and_consistent [∀ n, 𝔅.Kreisel (𝔅^[n] ⊥)] [Entailment.Consistent T] : 𝔅.height = ⊤ :=
+lemma height_eq_top_of_sound_and_consistent [𝔅.Kreisel] [Entailment.Consistent T] : 𝔅.height = ⊤ :=
   height_eq_top_iff.mpr iIncon_unprovable_of_sigma1_sound
 
 @[grind =>]

Foundation/FirstOrder/Incompleteness/ProvabilityAbstraction/Refutability.lean

@@ -106,7 +106,7 @@ variable
 local notation "𝐉" => jeroslow 𝔚
 
 lemma jeroslow_not_safe [𝔅.FormalizedCompleteOn 𝐉] : T ⊢ 𝐉 ➝ (𝔅 𝐉 ⋏ 𝔚 𝐉) := by
-  have h₁ : T ⊢ 𝐉 ➝ 𝔅 𝐉 := 𝔅.formalized_complete_on;
+  have h₁ : T ⊢ 𝐉 ➝ 𝔅 𝐉 := Entailment.WeakerThan.pbl $ 𝔅.formalized_complete_on;
   have h₂ : T ⊢ 𝐉 ⭤ 𝔚 𝐉 := jeroslow_def';
   cl_prover [h₁, h₂];