diff --git a/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition.lean b/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition.lean
index b4c18c3c7..1e47dc45d 100644
--- a/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition.lean
+++ b/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition.lean
@@ -35,11 +35,12 @@ theorem provable_D2 {σ π} : 𝗜𝚺₁ ⊢ □(σ ➝ π) ➝ □σ ➝ □π
 
 variable (T)
 
-noncomputable abbrev _root_.LO.FirstOrder.Theory.standardProvability : Provability 𝗜𝚺₁ T := ⟨T.provable⟩
+noncomputable abbrev _root_.LO.FirstOrder.Theory.standardProvability : Provability 𝗜𝚺₁ T where
+  prov := T.provable
+  prov_def := provable_D1
 
 variable {T}
 
-instance : T.standardProvability.HBL1 := ⟨provable_D1⟩
 instance : T.standardProvability.HBL2 := ⟨provable_D2⟩
 
 lemma standardProvability_def (σ : Sentence L) : T.standardProvability σ = T.provabilityPred σ := rfl
diff --git a/Foundation/FirstOrder/Bootstrapping/ProvabilityAbstraction/Basic.lean b/Foundation/FirstOrder/Bootstrapping/ProvabilityAbstraction/Basic.lean
index 3ea65d070..3b8a1a041 100644
--- a/Foundation/FirstOrder/Bootstrapping/ProvabilityAbstraction/Basic.lean
+++ b/Foundation/FirstOrder/Bootstrapping/ProvabilityAbstraction/Basic.lean
@@ -21,7 +21,8 @@ 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/[⌜σ⌝]
 
 namespace Provability
 
@@ -43,9 +44,7 @@ variable
   {L₀ L : Language} [L.ReferenceableBy L₀]
   {T₀ : Theory L₀} {T : Theory L}
 
-class Provability.HBL1 (𝔅 : Provability T₀ T) where
-  D1 {σ : Sentence L} : T ⊢ σ → T₀ ⊢ 𝔅 σ
-export Provability.HBL1 (D1)
+lemma D1 {𝔅 : Provability T₀ T} {σ : Sentence L} : T ⊢ σ → T₀ ⊢ 𝔅 σ := fun h ↦ 𝔅.prov_def h
 
 class Provability.HBL2 [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L} (𝔅 : Provability T₀ T) where
   D2 {σ τ : Sentence L} : T₀ ⊢ 𝔅 (σ ➝ τ) ➝ 𝔅 σ ➝ 𝔅 τ
@@ -55,7 +54,7 @@ class Provability.HBL3 [L.ReferenceableBy L] {T₀ T : Theory L} (𝔅 : Provabi
   D3 {σ : Sentence L} : T₀ ⊢ 𝔅 σ ➝ 𝔅 (𝔅 σ)
 export Provability.HBL3 (D3)
 
-class Provability.HBL [L.ReferenceableBy L] {T₀ T : Theory L} (𝔅 : Provability T₀ T) extends 𝔅.HBL1, 𝔅.HBL2, 𝔅.HBL3
+class Provability.HBL [L.ReferenceableBy L] {T₀ T : Theory L} (𝔅 : Provability T₀ T) extends 𝔅.HBL2, 𝔅.HBL3
 
 class Provability.Löb [L.ReferenceableBy L] {T₀ T : Theory L} (𝔅 : Provability T₀ T) where
   LT {σ : Sentence L} : T ⊢ 𝔅 σ ➝ σ → T ⊢ σ
@@ -101,31 +100,31 @@ lemma D2' [𝔅.HBL2] : T₀ ⊢ 𝔅 (σ ➝ τ) → T₀ ⊢ 𝔅 σ ➝ 𝔅
   intro h;
   exact D2 ⨀ h;
 
-lemma prov_distribute_imply [𝔅.HBL1] [𝔅.HBL2] (h : T ⊢ σ ➝ τ) : T₀ ⊢ 𝔅 σ ➝ 𝔅 τ := D2' $ D1 h
+lemma prov_distribute_imply [𝔅.HBL2] (h : T ⊢ σ ➝ τ) : T₀ ⊢ 𝔅 σ ➝ 𝔅 τ := D2' $ D1 h
 
-lemma prov_distribute_iff [𝔅.HBL1] [𝔅.HBL2] (h : T ⊢ σ ⭤ τ) : T₀ ⊢ 𝔅 σ ⭤ 𝔅 τ := by
+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] [𝔅.HBL1] [𝔅.HBL2]
+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 [𝔅.HBL1] [𝔅.HBL2] [L₀.DecidableEq] : T₀ ⊢ 𝔅 (σ ⋏ τ) ➝ 𝔅 σ ⋏ 𝔅 τ := by
+lemma prov_distribute_and [𝔅.HBL2] [L₀.DecidableEq] : T₀ ⊢ 𝔅 (σ ⋏ τ) ➝ 𝔅 σ ⋏ 𝔅 τ := by
   have h₁ : T₀ ⊢ 𝔅 (σ ⋏ τ) ➝ 𝔅 σ := D2' $ D1 and₁!;
   have h₂ : T₀ ⊢ 𝔅 (σ ⋏ τ) ➝ 𝔅 τ := D2' $ D1 and₂!;
   cl_prover [h₁, h₂];
 
-lemma prov_distribute_and' [𝔅.HBL1] [𝔅.HBL2] [L₀.DecidableEq] : T₀ ⊢ 𝔅 (σ ⋏ τ) → T₀ ⊢ 𝔅 σ ⋏ 𝔅 τ := λ h => prov_distribute_and ⨀ h
+lemma prov_distribute_and' [𝔅.HBL2] [L₀.DecidableEq] : T₀ ⊢ 𝔅 (σ ⋏ τ) → T₀ ⊢ 𝔅 σ ⋏ 𝔅 τ := λ h => prov_distribute_and ⨀ h
 
-lemma prov_collect_and [𝔅.HBL1] [𝔅.HBL2] [L₀.DecidableEq] [L.DecidableEq] : T₀ ⊢ 𝔅 σ ⋏ 𝔅 τ ➝ 𝔅 (σ ⋏ τ) := by
+lemma prov_collect_and [𝔅.HBL2] [L₀.DecidableEq] [L.DecidableEq] : T₀ ⊢ 𝔅 σ ⋏ 𝔅 τ ➝ 𝔅 (σ ⋏ τ) := by
   have h₁ : T₀ ⊢ 𝔅 σ ➝ 𝔅 (τ ➝ σ ⋏ τ) := prov_distribute_imply $ by cl_prover
   have h₂ : T₀ ⊢ 𝔅 (τ ➝ σ ⋏ τ) ➝ 𝔅 τ ➝ 𝔅 (σ ⋏ τ) := D2;
   cl_prover [h₁, h₂];
 
-lemma sound_iff₀ [𝔅.HBL1] [𝔅.Sound₀] : T₀ ⊢ 𝔅 σ ↔ T ⊢ σ := ⟨sound₀, D1⟩
+lemma sound_iff₀ [𝔅.Sound₀] : T₀ ⊢ 𝔅 σ ↔ T ⊢ σ := ⟨sound₀, D1⟩
 
 end
 
@@ -136,7 +135,7 @@ variable
   {𝔅 : Provability T₀ T}
   {σ τ : Sentence L}
 
-lemma D1_shift [𝔅.HBL1] : T ⊢ σ → T ⊢ 𝔅 σ := by
+lemma D1_shift : T ⊢ σ → T ⊢ 𝔅 σ := by
   intro h;
   apply Entailment.WeakerThan.pbl (𝓢 := T₀);
   apply D1 h;
@@ -150,13 +149,13 @@ lemma D3_shift [𝔅.HBL3] : T ⊢ 𝔅 σ ➝ 𝔅 (𝔅 σ) := by
 lemma FLT_shift [𝔅.FormalizedLöb] : T ⊢ 𝔅 (𝔅 σ ➝ σ) ➝ 𝔅 σ := by
   apply Entailment.WeakerThan.pbl (𝓢 := T₀) $ FLT;
 
-lemma prov_distribute_imply' [𝔅.HBL1] [𝔅.HBL2] (h : T₀ ⊢ σ ➝ τ) : T₀ ⊢ 𝔅 σ ➝ 𝔅 τ :=
+lemma prov_distribute_imply' [𝔅.HBL2] (h : T₀ ⊢ σ ➝ τ) : T₀ ⊢ 𝔅 σ ➝ 𝔅 τ :=
   prov_distribute_imply $ WeakerThan.pbl h
 
-lemma prov_distribute_imply'' [𝔅.HBL1] [𝔅.HBL2] (h : T ⊢ σ ➝ τ) : T ⊢ 𝔅 σ ➝ 𝔅 τ :=
+lemma prov_distribute_imply'' [𝔅.HBL2] (h : T ⊢ σ ➝ τ) : T ⊢ 𝔅 σ ➝ 𝔅 τ :=
   WeakerThan.pbl $ prov_distribute_imply h
 
-lemma sound_iff [𝔅.HBL1] [𝔅.Sound] : T ⊢ 𝔅 σ ↔ T ⊢ σ := ⟨sound, fun h ↦ WeakerThan.pbl (D1 h)⟩
+lemma sound_iff [𝔅.Sound] : T ⊢ 𝔅 σ ↔ T ⊢ σ := ⟨sound, fun h ↦ WeakerThan.pbl (D1 h)⟩
 
 end
 
@@ -184,7 +183,7 @@ section First
 variable [L.DecidableEq]
 variable [T₀ ⪯ T] [Consistent T]
 
-theorem unprovable_gödel [𝔅.HBL1] : T ⊬ (gödel 𝔅) := by
+theorem unprovable_gödel : T ⊬ (gödel 𝔅) := by
   intro h;
   have h₁ : T ⊢ 𝔅 (gödel 𝔅) := D1_shift h;
   have h₂ : T ⊢ (gödel 𝔅) ⭤ ∼𝔅 (gödel 𝔅) := WeakerThan.pbl $ gödel_spec;
@@ -200,12 +199,12 @@ theorem unrefutable_gödel [GödelSound 𝔅] : T ⊬ ∼(gödel 𝔅) := by
   have : ¬Consistent T := not_consistent_iff_inconsistent.mpr <| inconsistent_iff_provable_bot.mpr this
   contradiction;
 
-theorem gödel_independent [𝔅.HBL1] [GödelSound 𝔅] : Independent T (gödel 𝔅) := by
+theorem gödel_independent [GödelSound 𝔅] : Independent T (gödel 𝔅) := by
   constructor
   . apply unprovable_gödel
   . apply unrefutable_gödel
 
-theorem first_incompleteness [𝔅.HBL1] [GödelSound 𝔅] : Incomplete T :=
+theorem first_incompleteness [GödelSound 𝔅] : Incomplete T :=
   incomplete_def.mpr ⟨(gödel 𝔅), gödel_independent⟩
 
 end First
@@ -327,12 +326,12 @@ theorem unrefutable_rosser [𝔅.Rosser] : T ⊬ ∼𝐑 := by
     (N!_iff_CO!.mp hnρ) ⨀ hρ;
   contradiction
 
-theorem rosser_independent [L.DecidableEq] [𝔅.HBL1] [𝔅.Rosser] : Independent T 𝐑 := by
+theorem rosser_independent [L.DecidableEq] [𝔅.Rosser] : Independent T 𝐑 := by
   constructor
   . apply unprovable_gödel
   . apply unrefutable_rosser
 
-theorem rosser_first_incompleteness [L.DecidableEq] (𝔅 : Provability T₀ T) [𝔅.HBL1] [𝔅.Rosser] : Incomplete T :=
+theorem rosser_first_incompleteness [L.DecidableEq] (𝔅 : Provability T₀ T) [𝔅.Rosser] : Incomplete T :=
   incomplete_def.mpr ⟨gödel 𝔅, rosser_independent⟩
 
 omit [Diagonalization T₀] [Consistent T] in
diff --git a/Foundation/FirstOrder/Bootstrapping/ProvabilityAbstraction/Refutability.lean b/Foundation/FirstOrder/Bootstrapping/ProvabilityAbstraction/Refutability.lean
new file mode 100644
index 000000000..4c64debff
--- /dev/null
+++ b/Foundation/FirstOrder/Bootstrapping/ProvabilityAbstraction/Refutability.lean
@@ -0,0 +1,167 @@
+import Foundation.FirstOrder.Bootstrapping.RosserProvability
+
+namespace LO.FirstOrder
+
+namespace Derivation
+
+variable {𝓢 : SyntacticFormulas L} {φ : SyntacticSemiformula L 1}
+
+def specialize'! (t : SyntacticTerm L) (b : 𝓢 ⊢! ∀' φ) : 𝓢 ⊢! φ/[t] := by simpa using specialize (Γ := []) t b;
+
+def specialize' (t : SyntacticTerm L) (b : 𝓢 ⊢ ∀' φ) : 𝓢 ⊢ φ/[t] := ⟨specialize'! t b.get⟩
+
+end Derivation
+
+
+namespace Theory
+
+variable {T : Theory L} {φ : Semisentence L 1}
+
+def specialize! (t) (b : T ⊢! ∀' φ) : T ⊢! (φ/[t]) := by
+  apply ofSyntacticProof;
+  sorry;
+
+def specialize (t) (b : T ⊢ ∀' φ) : T ⊢ (φ/[t]) := by
+  have := Derivation.specialize' t $ provable_def.mp b;
+  apply provable_def.mpr;
+  sorry;
+
+end Theory
+
+
+namespace ProvabilityAbstraction
+
+open LO.Entailment FirstOrder Diagonalization Provability
+
+variable {L₀ L : Language}
+
+structure Refutability [L.ReferenceableBy L₀] (T₀ : Theory L₀) (T : Theory L) where
+  refu : Semisentence L₀ 1
+  refu_def {σ : Sentence L} : T ⊢ ∼σ → T₀ ⊢ refu/[⌜σ⌝]
+
+namespace Refutability
+
+variable [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L}
+
+@[coe] def rf (𝔚 : Refutability T₀ T) (σ : Sentence L) : Sentence L₀ := 𝔚.refu/[⌜σ⌝]
+instance : CoeFun (Refutability T₀ T) (fun _ ↦ Sentence L → Sentence L₀) := ⟨rf⟩
+
+end Refutability
+
+
+section
+
+variable
+  {L₀ L : Language} [L.ReferenceableBy L₀]
+  {T₀ : Theory L₀} {T : Theory L}
+
+lemma R1 {𝔚 : Refutability T₀ T} {σ : Sentence L} : T ⊢ ∼σ → T₀ ⊢ 𝔚 σ := fun h ↦ 𝔚.refu_def h
+
+lemma R1' {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L}
+  {𝔚 : Refutability T₀ T} {σ : Sentence L} [T₀ ⪯ T] : T ⊢ ∼σ → T ⊢ 𝔚 σ := fun h ↦
+  WeakerThan.pbl $ R1 h
+
+end
+
+
+section
+
+variable
+  [L.ReferenceableBy L] {T₀ T : Theory L}
+  [Diagonalization T₀]
+  {𝔚 : Refutability T₀ T}
+
+/-- This sentence is refutable. -/
+def jeroslow (𝔚 : Refutability T₀ T) [Diagonalization T₀] : Sentence L := fixedpoint T₀ 𝔚.refu
+
+lemma jeroslow_def : T₀ ⊢ jeroslow 𝔚 ⭤ 𝔚 (jeroslow 𝔚) := Diagonalization.diag _
+
+lemma jeroslow_def' [T₀ ⪯ T] : T ⊢ jeroslow 𝔚 ⭤ 𝔚 (jeroslow 𝔚) := WeakerThan.pbl $ jeroslow_def
+
+
+/-- Abstraction of formalized `𝚺₁`-completeness -/
+class Provability.FormalizedCompleteOn (𝔅 : Provability T₀ T) (σ : Sentence L) where
+  formalized_complete_on : T ⊢ σ ➝ 𝔅 σ
+alias Provability.formalized_complete_on := Provability.FormalizedCompleteOn.formalized_complete_on
+
+class Provability.SoundOn (𝔅 : Provability T₀ T) (σ : Sentence L) where
+  sound_on : T ⊢ 𝔅 σ → T ⊢ σ
+alias Provability.sound_on := Provability.SoundOn.sound_on
+
+class Refutability.SoundOn (𝔚 : Refutability T₀ T) (σ : Sentence L) where
+  sound_on : T ⊢ 𝔚 σ → T ⊢ ∼σ
+alias Refutability.sound_on := Refutability.SoundOn.sound_on
+
+end
+
+
+section
+
+variable
+  [L.ReferenceableBy L] {T₀ T : Theory L}
+  [Diagonalization T₀]
+  {𝔚 : Refutability T₀ T}
+
+lemma unprovable_jeroslow [T₀ ⪯ T] [Consistent T] [Refutability.SoundOn 𝔚 (jeroslow 𝔚)] : T ⊬ jeroslow 𝔚 := by
+  by_contra hC;
+  apply Entailment.Consistent.not_bot (𝓢 := T);
+  . infer_instance;
+  . have : T ⊢ ∼(jeroslow 𝔚) := Refutability.sound_on $ (Entailment.iff_of_E! $ jeroslow_def') |>.mp hC;
+    exact (N!_iff_CO!.mp this) ⨀ hC;
+
+end
+
+
+section
+
+variable
+  [L.ReferenceableBy L] {T₀ T : Theory L}
+  [Diagonalization T₀]
+  {𝔅 : Provability T₀ T} {𝔚 : Refutability T₀ T}
+
+/-- Formalized Law of Noncontradiction holds on `x` -/
+def safe (𝔅 : Provability T₀ T) (𝔚 : Refutability T₀ T) : Semisentence L 1 := “x. ¬(!𝔅.prov x ∧ !𝔚.refu x)”
+
+/-- Formalized Law of Noncontradiction -/
+def flon (𝔅 : Provability T₀ T) (𝔚 : Refutability T₀ T) : Sentence L := “∀ x, !(safe 𝔅 𝔚) x”
+
+end
+
+
+section
+
+variable
+  [L.DecidableEq] [L.ReferenceableBy L] {T₀ T : Theory L}
+  [Diagonalization T₀] [T₀ ⪯ T]
+  {𝔅 : Provability T₀ T} {𝔚 : Refutability T₀ T}
+
+local notation "𝐉" => jeroslow 𝔚
+
+lemma jeroslow_not_safe [𝔅.FormalizedCompleteOn 𝐉] : T ⊢ 𝐉 ➝ (𝔅 𝐉 ⋏ 𝔚 𝐉) := by
+  have h₁ : T ⊢ 𝐉 ➝ 𝔅 𝐉 := Provability.formalized_complete_on;
+  have h₂ : T ⊢ 𝐉 ⭤ 𝔚 𝐉 := jeroslow_def';
+  cl_prover [h₁, h₂];
+
+/--
+  Formalized law of noncontradiction cannot be proved.
+  Alternative form of Gödel's second incompleteness theorem.
+-/
+lemma unprovable_flon [consis : Consistent T] [𝔅.FormalizedCompleteOn 𝐉] : T ⊬ flon 𝔅 𝔚 := by
+  contrapose! consis;
+  replace consis : T ⊢ ∀' safe 𝔅 𝔚 := by simpa [flon] using consis;
+  have h₁ : T ⊢ ∼(𝔅 𝐉 ⋏ 𝔚 𝐉) := by simpa [safe] using FirstOrder.Theory.specialize _ $ consis;
+  have h₂ : T ⊢ 𝐉 ➝ 𝔅 𝐉 := Provability.formalized_complete_on;
+  have h₃ : T ⊢ 𝐉 ⭤ 𝔚 𝐉 := jeroslow_def';
+  have h₄ : T ⊢ ∼(𝔅 𝐉 ⋏ 𝔚 𝐉) ➝ ∼𝐉 := contra! $ by cl_prover [h₂, h₃];
+  have h₅ : T ⊢ ∼𝐉 := h₄ ⨀ h₁;
+  have h₆ : T ⊢ 𝔚 𝐉 := R1' h₅;
+  have h₇ : T ⊢ 𝔚 𝐉 ➝ 𝐉 := by cl_prover [h₃];
+  have h₈ : T ⊢ 𝐉 := h₇ ⨀ h₆;
+  exact not_consistent_iff_inconsistent.mpr <| inconsistent_iff_provable_bot.mpr $ (N!_iff_CO!.mp h₅) ⨀ h₈;
+
+end
+
+
+end ProvabilityAbstraction
+
+end LO.FirstOrder
diff --git a/Foundation/FirstOrder/Bootstrapping/RosserProvability.lean b/Foundation/FirstOrder/Bootstrapping/RosserProvability.lean
index db33daf90..0202a4756 100644
--- a/Foundation/FirstOrder/Bootstrapping/RosserProvability.lean
+++ b/Foundation/FirstOrder/Bootstrapping/RosserProvability.lean
@@ -128,10 +128,9 @@ variable (T)
 
 noncomputable abbrev _root_.LO.FirstOrder.Theory.rosserProvability : Provability 𝗜𝚺₁ T where
   prov := T.rosserProvable
+  prov_def := rosserProvable_D1
 
-instance [Entailment.Consistent T] : T.rosserProvability.HBL1 := ⟨rosserProvable_D1⟩
-
-instance [Entailment.Consistent T] : T.rosserProvability.Rosser := ⟨rosserProvable_rosser⟩
+instance : T.rosserProvability.Rosser := ⟨rosserProvable_rosser⟩
 
 lemma rosserProvability_def (σ : Sentence L) : T.rosserProvability σ = T.rosserPred σ := rfl
 
diff --git a/Foundation/FirstOrder/Incompleteness/Jeroslow.lean b/Foundation/FirstOrder/Incompleteness/Jeroslow.lean
new file mode 100644
index 000000000..697d96613
--- /dev/null
+++ b/Foundation/FirstOrder/Incompleteness/Jeroslow.lean
@@ -0,0 +1,76 @@
+import Foundation.FirstOrder.Bootstrapping.RosserProvability
+import Foundation.FirstOrder.Bootstrapping.ProvabilityAbstraction.Refutability
+
+namespace LO.FirstOrder
+
+open FirstOrder Arithmetic
+open PeanoMinus ISigma0 ISigma1 Bootstrapping Derivation ProvabilityAbstraction
+
+namespace Theory
+
+variable {V : Type*} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁]
+variable {L : Language} [L.Encodable] [L.LORDefinable]
+
+variable {T U : Theory L} [T.Δ₁] [U.Δ₁]
+
+def Refutable (T : Theory L) [T.Δ₁] (φ : V) : Prop := T.Provable (neg L φ)
+
+lemma Refutable.quote_iff {σ : Sentence L} : T.Refutable (V := V) ⌜σ⌝ ↔ T.Provable (V := V) ⌜∼σ⌝ := by
+  simp [Refutable, Sentence.quote_def, Semiformula.quote_def]
+
+noncomputable def refutable (T : Theory L) [T.Δ₁] : 𝚺₁.Semisentence 1 := .mkSigma
+  “φ. ∀ nφ, !(negGraph L) nφ φ → !T.provable nφ” $ by
+    sorry;
+    /-
+    -- apply Hierarchy.all_iff.mpr;
+    apply Hierarchy.imp_iff.mpr;
+    constructor;
+    . apply Hierarchy.strict_mono (Γ := 𝚺) (s := 1) <;> simp;
+    . apply Hierarchy.strict_mono (Γ := 𝚺) (s := 1) <;> simp;
+    -/
+
+lemma refutable_defined :𝚺₁-Predicate[V] T.Refutable via T.refutable := .mk fun v ↦ by
+  simp [Theory.refutable, Theory.Refutable];
+
+noncomputable def standardRefutability (T : ArithmeticTheory) [T.Δ₁] : Refutability 𝗜𝚺₁ T where
+  refu := T.refutable.val
+  refu_def {σ} h := by
+    sorry;
+
+end Theory
+
+
+open ProvabilityAbstraction
+
+namespace Arithmetic
+
+variable {V : Type} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁]
+variable {T U : ArithmeticTheory} [T.Δ₁]  -- [𝗜𝚺₁ ⪯ T] [𝗜𝚺₁ ⪯ U]
+
+@[simp]
+lemma jeroslow_sigmaOne : Hierarchy 𝚺 1 (jeroslow (Theory.standardRefutability T)) := by
+  dsimp [jeroslow, Diagonalization, Diagonalization.fixedpoint, fixedpoint];
+  sorry;
+
+instance : T.standardRefutability.SoundOn (jeroslow T.standardRefutability) := by
+  constructor;
+  intro h;
+  simp [Theory.standardRefutability, Refutability.rf] at h;
+  sorry;
+
+instance [𝗜𝚺₁ ⪯ T] : T.standardProvability.FormalizedCompleteOn (jeroslow T.standardRefutability) := by
+  constructor;
+  apply Entailment.WeakerThan.pbl (𝓢 := 𝗜𝚺₁);
+  apply provable_sigma_one_complete;
+  simp;
+
+theorem unprovable_jeroslow [𝗜𝚺₁ ⪯ T] [T.SoundOnHierarchy 𝚺 1]
+  : T ⊬ jeroslow (T.standardRefutability) := ProvabilityAbstraction.unprovable_jeroslow
+
+theorem unprovable_formalized_law_of_noncontradiction
+  [𝗜𝚺₁ ⪯ T] [T.SoundOnHierarchy 𝚺 1]
+  : T ⊬ flon (T.standardProvability) (T.standardRefutability) := ProvabilityAbstraction.unprovable_flon
+
+end Arithmetic
+
+end LO.FirstOrder
diff --git a/Foundation/ProvabilityLogic/GL/Unprovability.lean b/Foundation/ProvabilityLogic/GL/Unprovability.lean
index 6d6a884cd..f3a1c3cf8 100644
--- a/Foundation/ProvabilityLogic/GL/Unprovability.lean
+++ b/Foundation/ProvabilityLogic/GL/Unprovability.lean
@@ -17,7 +17,7 @@ variable {L : Language} [L.ReferenceableBy L] [DecidableEq (Sentence L)]
 
 def Provability.indep (𝔅 : Provability T₀ T) (σ : Sentence L) : Sentence L := ∼(𝔅 σ) ⋏ ∼(𝔅 (∼σ))
 
-lemma indep_distribute [𝔅.HBL1] [𝔅.HBL2] (h : T ⊢ σ ⭤ π) : T ⊢ 𝔅.indep σ ➝ 𝔅.indep π := by
+lemma indep_distribute [𝔅.HBL2] (h : T ⊢ σ ⭤ π) : T ⊢ 𝔅.indep σ ➝ 𝔅.indep π := by
   apply CKK!_of_C!_of_C!;
   . apply contra!;
     apply WeakerThan.pbl (𝓢 := T₀);
@@ -28,14 +28,14 @@ lemma indep_distribute [𝔅.HBL1] [𝔅.HBL2] (h : T ⊢ σ ⭤ π) : T ⊢ 
     apply prov_distribute_imply;
     cl_prover [h];
 
-lemma indep_iff_distribute_inside [𝔅.HBL1] [𝔅.HBL2] (h : T ⊢ σ ⭤ π) :
+lemma indep_iff_distribute_inside [𝔅.HBL2] (h : T ⊢ σ ⭤ π) :
     T ⊢ 𝔅.indep σ ⭤ 𝔅.indep π := by
   apply K!_intro
   . exact indep_distribute $ h;
   . apply indep_distribute;
     cl_prover [h];
 
-lemma indep_iff_distribute [𝔅.HBL1] [𝔅.HBL2] (h : T ⊢ σ ⭤ π) :
+lemma indep_iff_distribute [𝔅.HBL2] (h : T ⊢ σ ⭤ π) :
     T ⊢ 𝔅.indep σ ↔ T ⊢ 𝔅.indep π := by
   constructor;
   . intro H; exact K!_left (indep_iff_distribute_inside h) ⨀ H;
diff --git a/Foundation/ProvabilityLogic/Grz/Completeness.lean b/Foundation/ProvabilityLogic/Grz/Completeness.lean
index c69d6b8a2..66ba1d608 100644
--- a/Foundation/ProvabilityLogic/Grz/Completeness.lean
+++ b/Foundation/ProvabilityLogic/Grz/Completeness.lean
@@ -36,7 +36,7 @@ variable {L : Language} [L.ReferenceableBy L] [L.DecidableEq]
 
 namespace Realization
 
-variable {𝔅 : Provability T₀ T} [𝔅.HBL1] {f : Realization 𝔅} {A B : Modal.Formula _}
+variable {𝔅 : Provability T₀ T} {f : Realization 𝔅} {A B : Modal.Formula _}
 
 def strongInterpret (f : Realization 𝔅) : Formula ℕ → Sentence L
   | .atom a => f a
diff --git a/Foundation/ProvabilityLogic/N/Soundness.lean b/Foundation/ProvabilityLogic/N/Soundness.lean
index 43e0fad2f..1297ca742 100644
--- a/Foundation/ProvabilityLogic/N/Soundness.lean
+++ b/Foundation/ProvabilityLogic/N/Soundness.lean
@@ -15,7 +15,7 @@ open FirstOrder.ProvabilityAbstraction
 variable {L : FirstOrder.Language} [L.ReferenceableBy L]
          [L.DecidableEq]
          {T U : FirstOrder.Theory L} [T ⪯ U]
-         {𝔅 : Provability T U} [𝔅.HBL1]
+         {𝔅 : Provability T U}
 
 lemma N.arithmetical_soundness (h : Modal.N ⊢ A) {f : Realization 𝔅} : U ⊢ f A := by
   induction h using Hilbert.Normal.rec! with