Gödel's first incompleteness theorem for arithmetic theories stronger than $\mathsf{R_0}$

theorem LO.FirstOrder.Arithmetic.incomplete (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗥₀ ⪯ T] [T.SoundOnHierarchy 𝚺 1] : Entailment.Incomplete T

Gödel's first incompleteness theorem

theorem LO.FirstOrder.Arithmetic.exists_true_but_unprovable_sentence (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗥₀ ⪯ T] [T.SoundOnHierarchy 𝚺 1] : ∃ (δ : ArithmeticSentence), ℕ↓[ℒₒᵣ] ⊧ δ ∧ T ⊬ δ

instance LO.FirstOrder.Arithmetic.instStrictlyWeakerThanSentenceORingArithmeticTheoryFirstOrderTrueArithOfModelsSetStrucStrOfΔ₁OfWeakerThanR0OfSoundOnHierarchySigmaPolarityOfNatNat {T : ArithmeticTheory} [ℕ↓[ℒₒᵣ] ⊧* T] [Theory.Δ₁ T] [𝗥₀ ⪯ T] [T.SoundOnHierarchy 𝚺 1] : T ⪱ 𝗧𝗔