Gödel's second incompleteness theorem for arithmetic theories stronger than $\mathsf{I}\Sigma_1$

theorem LO.FirstOrder.Arithmetic.consistent_unprovable (T : Theory ℒₒᵣ) [T.Δ₁] [𝗜𝚺₁ ⪯ T] [Entailment.Consistent T] : T ⊬ ↑T.consistent

Gödel's second incompleteness theorem

theorem LO.FirstOrder.Arithmetic.inconsistent_unprovable (T : Theory ℒₒᵣ) [T.Δ₁] [𝗜𝚺₁ ⪯ T] [ArithmeticTheory.SoundOnHierarchy T 𝚺 1] : T ⊬ ∼↑T.consistent

theorem LO.FirstOrder.Arithmetic.inconsistent_independent (T : Theory ℒₒᵣ) [T.Δ₁] [𝗜𝚺₁ ⪯ T] [ArithmeticTheory.SoundOnHierarchy T 𝚺 1] : Entailment.Independent T ↑T.consistent

The consistency statement is independent.

instance LO.FirstOrder.Arithmetic.instStrictlyWeakerThanSentenceORingTheoryHAddArithmeticTheoryConOfConsistent (T : Theory ℒₒᵣ) [T.Δ₁] [𝗜𝚺₁ ⪯ T] [Entailment.Consistent T] : T ⪱ T + T.Con

instance LO.FirstOrder.Arithmetic.instStrictlyWeakerThanSentenceORingTheoryHAddArithmeticTheoryInconOfSoundOnHierarchySigmaPolarityOfNatNat (T : Theory ℒₒᵣ) [T.Δ₁] [𝗜𝚺₁ ⪯ T] [ArithmeticTheory.SoundOnHierarchy T 𝚺 1] : T ⪱ T + T.Incon