Supporting results for pointwise provable equality.

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

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.consistent_unprovable (T : ArithmeticTheory) [Theory.Δ₁ T] [𝐈Σ₁ ≼ T] [Entailment.Consistent T] : T ⊬ ↑(Theory.consistent T)

Gödel's second incompleteness theorem

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.craig_consistent_unprovable_of_RE (T : ArithmeticTheory) [Theory.RE T] [𝐈Σ₁ ≼ T] [Entailment.Consistent T] : T ⊬ ↑(Theory.craig T).consistent

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

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.inconsistent_unprovable (T : ArithmeticTheory) [Theory.Δ₁ T] [𝐈Σ₁ ≼ T] [T.SoundOnHierarchy Σ 1] : T ⊬ ∼↑(Theory.consistent T)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.inconsistent_independent (T : ArithmeticTheory) [Theory.Δ₁ T] [𝐈Σ₁ ≼ T] [T.SoundOnHierarchy Σ 1] : Entailment.Independent T ↑(Theory.consistent T)

The consistency statement is independent.

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instStrictlyWeakerThanSentenceORingArithmeticTheoryUnionConOfConsistent (T : ArithmeticTheory) [Theory.Δ₁ T] [𝐈Σ₁ ≼ T] [Entailment.Consistent T] : T ≺ T ∪ Theory.Con T

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instStrictlyWeakerThanSentenceORingArithmeticTheoryUnionInconOfSoundOnHierarchySigmaPolarityOfNatNat (T : ArithmeticTheory) [Theory.Δ₁ T] [𝐈Σ₁ ≼ T] [T.SoundOnHierarchy Σ 1] : T ≺ T ∪ Theory.Incon T