Incomplete

theorem incomplete (T : ArithmeticTheory) [T.Δ₁] [𝗥₀ ⪯ T] [T.SoundOnHierarchy 𝚺 1] :    Incomplete T := by  have con : Consistent T := inferInstance  let D : ℕ → Prop := fun φ : ℕ ↦    IsSemiformula ℒₒᵣ 1 φ ∧ Provable T (neg ℒₒᵣ <| subst ℒₒᵣ ?[numeral φ] φ)  have D_re : REPred D := by    have : 𝚺₁-Predicate fun φ : ℕ ↦        IsSemiformula ℒₒᵣ 1 φ ∧ Provable T (neg ℒₒᵣ <| subst ℒₒᵣ ?[numeral φ] φ) := by      definability    exact rePred_iff_sigma1.mpr this  have D_spec (φ : ArithmeticSemisentence 1) : D ⌜φ⌝ ↔ T ⊢ ∼φ/[⌜φ⌝] := by    simp [D, ←provable_iff_provable, Sentence.quote_def,      Rewriting.emb_subst_eq_subst_coe₁, Semiformula.quote_def]  let δ : ArithmeticSemisentence 1 := codeOfREPred D  have (n : ℕ) : D n ↔ T ⊢ δ/[↑n] := by    simpa [Semiformula.coe_subst_eq_subst_coe₁] using rePred_weak_representation D_re  let π : ArithmeticSentence := δ/[⌜δ⌝]  have : T ⊢ π ↔ T ⊢ ∼π := calc    T ⊢ π ↔ T ⊢ δ/[⌜δ⌝]  := by rfl    _     ↔ D ⌜δ⌝        := by simpa using (this ⌜δ⌝).symm    _     ↔ T ⊢ ∼δ/[⌜δ⌝] := D_spec δ    _     ↔ T ⊢ ∼π       := by rfl  refine incomplete_def.mpr ⟨π, ?_, ?_⟩  · intro h    exact not_consistent_iff_inconsistent.mpr      (inconsistent_of_provable_of_unprovable h (this.mp h)) inferInstance  · intro h    exact not_consistent_iff_inconsistent.mpr      (inconsistent_of_provable_of_unprovable (this.mpr h) h) inferInstance