Supporting results for pointwise provable equality.

From a partial-recursive axiom enumerator in Mathlib's fixed program numbering to enumerability of theorem codes. The enumerator may diverge on inputs; its range, rather than totality, specifies the axioms.

theorem PointwiseComposition.FailureOfComposition.partial_program_range_re (a : ℕ) : REPred fun (n : ℕ) => ∃ (x : ℕ), n ∈ Kleene.eval a x

The range of a numbered partial-recursive program is enumerable.

theorem PointwiseComposition.FailureOfComposition.axiom_codes_re_of_program_enumerator (T : FFL.FirstOrder.ArithmeticTheory) (a : ℕ) (ha : ∀ (n : ℕ), AxiomCodes T n ↔ ∃ (x : ℕ), n ∈ Kleene.eval a x) : REPred (AxiomCodes T)

The manuscript's partial recursive axiom enumeration makes AxiomCodes r.e.

theorem PointwiseComposition.FailureOfComposition.theorem_codes_re_of_program_enumerator (T : FFL.FirstOrder.ArithmeticTheory) (a : ℕ) (ha : ∀ (n : ℕ), AxiomCodes T n ↔ ∃ (x : ℕ), n ∈ Kleene.eval a x) : REPred (TheoremCodes T)

An axiom enumerator suffices to enumerate the deductive closure.