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

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

Gödel's first incompleteness theorem

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

instance FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryTheoryR0Craig {T : ArithmeticTheory} [Theory.RE T] [𝗥₀ ⪯ T] : 𝗥₀ ⪯ Theory.craig T

instance FFL.FirstOrder.Arithmetic.instSoundOnHierarchyCraigSigmaPolarityOfNatNat {T : ArithmeticTheory} [Theory.RE T] [T.SoundOnHierarchy 𝚺 1] : ArithmeticTheory.SoundOnHierarchy (Theory.craig T) 𝚺 1

theorem FFL.FirstOrder.Arithmetic.incomplete_of_RE (T : ArithmeticTheory) [Theory.RE T] [𝗥₀ ⪯ T] [T.SoundOnHierarchy 𝚺 1] : Entailment.Incomplete T

Gödel's first incompleteness theorem for r.e. theories

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

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