Supporting results for pointwise provable equality.

Index-level consequence of the arithmetization assumptions explicitly stated in v36, equations (composition-graph) and (graph-realization).

Arithmetization is a hypothesis, not a constructed instance for Mathlib's evaluator. In particular, the realization field is not discharged here. No theorem in this file identifies standard-model equivalence with PA provability.

def PointwiseComposition.FailureOfComposition.ProgramIndices.kleeneEqAt (F G : ProofSearch.Graph) (n : ℕ) : FFL.FirstOrder.ArithmeticSentence

The paper's definedness equivalence and common-value clause.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FailureOfComposition.ProgramIndices.kleeneEqAt_iff_eqAt (F G : ProofSearch.Graph) (hF : ProofSearch.Functional F) (hG : ProofSearch.Functional G) (n : ℕ) : 𝐏𝐀 ⊢ kleeneEqAt F G n ⇔ₗ ProofSearch.eqAt F G n

Functionality is what makes output-quantified graph equality the same as the manuscript's equality, including agreement on divergence.

structure PointwiseComposition.FailureOfComposition.ProgramIndices.Arithmetization : Type

The two PA-level arithmetization theorems assumed in v36, together with functionality. Supplying this structure is a substantial separate obligation.

• evaluation : ℕ → ℕ → Part ℕ

  The evaluation construction in FailureOfComposition.ProgramIndices.Arithmetization.

• graph : ℕ → ProofSearch.Graph

  The graph construction in FailureOfComposition.ProgramIndices.Arithmetization.

• compIndex : ℕ → ℕ → ℕ

  The comp Index construction in FailureOfComposition.ProgramIndices.Arithmetization.

• compIndex_primrec : Primrec₂ self.compIndex
• adequate (e x y : ℕ) : (FFL.FirstOrder.Semiformula.Evalb ![x, y]) ↑(self.graph e) ↔ y ∈ self.evaluation e x
• functional (e : ℕ) : ProofSearch.Functional (self.graph e)
• composition (e d : ℕ) : ProofSearch.Uniform 𝐏𝐀 (self.graph (self.compIndex e d)) (ProofSearch.comp (self.graph e) (self.graph d))
• realization (F : ProofSearch.Graph) : ProofSearch.Functional F → ∃ (e : ℕ), ProofSearch.Uniform 𝐏𝐀 (self.graph e) F

theorem PointwiseComposition.FailureOfComposition.ProgramIndices.uniform_to_pointwise (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] {F G : ProofSearch.Graph} (h : ProofSearch.Uniform 𝐏𝐀 F G) : ProofSearch.Pointwise T F G

theorem PointwiseComposition.FailureOfComposition.ProgramIndices.uniform_comp {F F' G G' : ProofSearch.Graph} (hF : ProofSearch.Uniform 𝐏𝐀 F F') (hG : ProofSearch.Uniform 𝐏𝐀 G G') : ProofSearch.Uniform 𝐏𝐀 (ProofSearch.comp F G) (ProofSearch.comp F' G')

def PointwiseComposition.FailureOfComposition.ProgramIndices.PointwiseIndex (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) (e d : ℕ) : Prop

The Pointwise Index construction in FailureOfComposition.ProgramIndices.

Equations

• PointwiseComposition.FailureOfComposition.ProgramIndices.PointwiseIndex A T e d = ∀ (n : ℕ), T ⊢ PointwiseComposition.FailureOfComposition.ProgramIndices.kleeneEqAt (A.graph e) (A.graph d) n

theorem PointwiseComposition.FailureOfComposition.ProgramIndices.pointwiseIndex_iff (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (e d : ℕ) : PointwiseIndex A T e d ↔ ProofSearch.Pointwise T (A.graph e) (A.graph d)

def PointwiseComposition.FailureOfComposition.ProgramIndices.indexSetoid (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] : Setoid ℕ

The index Setoid construction in FailureOfComposition.ProgramIndices.

Equations

• PointwiseComposition.FailureOfComposition.ProgramIndices.indexSetoid A T = { r := PointwiseComposition.FailureOfComposition.ProgramIndices.PointwiseIndex A T, iseqv := ⋯ }

def PointwiseComposition.FailureOfComposition.ProgramIndices.NoIndexQuotientComposition (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] : Prop

The No Index Quotient Composition construction in FailureOfComposition.ProgramIndices.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FailureOfComposition.ProgramIndices.index_noncongruence_of_graph_noncongruence (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (h : ∃ (F : ProofSearch.Graph) (I : ProofSearch.Graph) (G : ProofSearch.Graph), ProofSearch.Functional F ∧ ProofSearch.Functional I ∧ ProofSearch.Functional G ∧ ProofSearch.Pointwise T F I ∧ ¬ProofSearch.Pointwise T (ProofSearch.comp F G) (ProofSearch.comp I G)) : ∃ (f : ℕ) (i : ℕ) (g : ℕ), PointwiseIndex A T f i ∧ ¬PointwiseIndex A T (A.compIndex f g) (A.compIndex i g)

theorem PointwiseComposition.FailureOfComposition.ProgramIndices.no_index_quotient_of_graph_noncongruence (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (h : ∃ (F : ProofSearch.Graph) (I : ProofSearch.Graph) (G : ProofSearch.Graph), ProofSearch.Functional F ∧ ProofSearch.Functional I ∧ ProofSearch.Functional G ∧ ProofSearch.Pointwise T F I ∧ ¬ProofSearch.Pointwise T (ProofSearch.comp F G) (ProofSearch.comp I G)) : NoIndexQuotientComposition A T

theorem PointwiseComposition.FailureOfComposition.ProgramIndices.no_index_quotient_via_godel (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ T] [FFL.Entailment.Consistent T] [𝐏𝐀 ≼ T] : NoIndexQuotientComposition A T

theorem PointwiseComposition.FailureOfComposition.ProgramIndices.no_index_quotient_via_productiveness (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [FFL.Entailment.Consistent T] [𝐏𝐀 ≼ T] (hT : REPred (TheoremCodes T)) : NoIndexQuotientComposition A T

Independent productiveness route, with r.e. theorem codes explicit.