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

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

Gödel's second incompleteness theorem

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

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

The consistency statement is independent.

instance LO.FirstOrder.Arithmetic.instStrictlyWeakerThanSentenceORingArithmeticTheoryUnionConOfConsistent (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] [Entailment.Consistent T] : T ⪱ T ∪ Theory.Con T

instance LO.FirstOrder.Arithmetic.instStrictlyWeakerThanSentenceORingArithmeticTheoryUnionInconOfSoundOnHierarchySigmaPolarityOfNatNat (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] [T.SoundOnHierarchy 𝚺 1] : T ⪱ T ∪ Theory.Incon T