Supporting results for pointwise provable equality.

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

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.incomplete (T : ArithmeticTheory) [Theory.Δ₁ T] [𝐑₀ ≼ T] [T.SoundOnHierarchy Σ 1] : Entailment.Incomplete T

Gödel's first incompleteness theorem

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

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryTheoryR0CraigOfRE {T : ArithmeticTheory} [Theory.RE T] [𝐑₀ ≼ T] : 𝐑₀ ≼ Theory.craig T

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instSoundOnHierarchyCraigSigmaPolarityOfNatNatOfRE {T : ArithmeticTheory} [Theory.RE T] [T.SoundOnHierarchy Σ 1] : ArithmeticTheory.SoundOnHierarchy (Theory.craig T) Σ 1

theorem PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.exists_true_but_unprovable_sentence_of_RE_of_sigma1sound (T : ArithmeticTheory) [Theory.RE T] [𝐑₀ ≼ T] [T.SoundOnHierarchy Σ 1] : ∃ (δ : ArithmeticSentence), ℕ↓[ℒₒᵣ] ⊧ δ ∧ T ⊬ δ

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instStrictlyWeakerThanSentenceORingArithmeticTheoryFirstOrderTrueArithOfModelsSetStrucStrOfΔ₁OfWeakerThanR0OfSoundOnHierarchySigmaPolarityOfNatNat {T : ArithmeticTheory} [ℕ↓[ℒₒᵣ] ⊧* T] [Theory.Δ₁ T] [𝐑₀ ≼ T] [T.SoundOnHierarchy Σ 1] : T ≺ 𝐓𝐀