Supporting results for pointwise provable equality.

The concrete second-incompleteness obstruction for every consistent extension of PA with recursively enumerable axiom codes. Craig's padded presentation discharges the Delta-one presentation requirement of the proof predicate.

theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.index_noncongruence_via_godel_of_re_axioms (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] (hT : REPred (AxiomCodes T)) : ∃ (f : ℕ) (i : ℕ) (g : ℕ), PointwiseIndex T f i ∧ ¬PointwiseIndex T (CategoricalRiceShapiro.PartialRecursive.canonicalPartrecCompIndex f g) (CategoricalRiceShapiro.PartialRecursive.canonicalPartrecCompIndex i g)

theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.no_index_quotient_via_godel_of_re_axioms (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] (hT : REPred (AxiomCodes T)) : NoIndexQuotientComposition T

The Gödel-II route, with the same r.e.-axiom assumptions as the independent productive-set route and no realization or presentation hypothesis.

theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.no_index_quotient_via_godel_of_axiom_enumerator (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] (a : ℕ) (ha : ∀ (n : ℕ), AxiomCodes T n ↔ ∃ (x : ℕ), n ∈ Kleene.eval a x) : NoIndexQuotientComposition T