Supporting results for pointwise provable equality.

Evaluation properties of primitive-recursion codes

codePrecStep dg is the step relation of codePrec. It has n + 3 arguments: the history index, the history code, the recursion argument, and the n outer arguments. It never reads argument 2, the recursion argument: precStepArgs supplies Code.proj 0, codeBeta (Code.proj 1) (Code.proj 0), and the outer projections, none of which is Code.proj 2.

eval_codePrecStep_bound_irrel_iff records that, so a caller may change the recursion argument without disturbing the step relation. The proof is structural: InputsAgree is a conservative dependency relation on the nine Code constructors, and eval_iff_of_inputsAgree turns it into an equivalence of evaluations.

The proof of eval_codePrecStep_bound_irrel_iff does not evaluate codeBeta or any other derived constructor in the model. It inspects those codes only as syntax trees and assumes no arithmetic theory: ORingStructure M alone. The existence theorem below instead uses arithmetic evaluation and beta extension under 𝐏𝐀.

A conservative dependency relation

Evaluation respects the dependency relation

Closure of the dependency relation under the derived constructors

Each lemma below inspects a code as a syntax tree only. No arithmetic meaning is attached to any of them, and codeBeta in particular is delta-reduced but never evaluated.

The recursion argument is unused by the step relation

Bound irrelevance for the base conjunct of the recursion predicate

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codePrecStep_bound_irrel_iff {M : Type u_1} [FFL.ORingStructure M] {n : ℕ} (dg : Nat.ArithPart₁.Code (n + 2)) (p j hc c c' : M) (v : Fin n → M) : (FFL.FirstOrder.Semiformula.Evalb (p :> j :> hc :> c :> v)) (FFL.FirstOrder.Arithmetic.code (codePrecStep dg)) ↔ (FFL.FirstOrder.Semiformula.Evalb (p :> j :> hc :> c' :> v)) (FFL.FirstOrder.Arithmetic.code (codePrecStep dg))

The step relation of codePrec does not read the recursion argument.

The arguments of codePrecStep dg are the history index, the history code, the recursion argument, and the outer arguments. Argument 2, the recursion argument, is supplied to nothing: precStepArgs hands dg only Code.proj 0, codeBeta (Code.proj 1) (Code.proj 0), and the outer projections. A caller may therefore change it freely.

No arithmetic theory is assumed, and no code is evaluated in the model.

Sigma-one definability of one argument slot of a literal code graph

Reading one history entry through different argument codes

Reading a correct history

Correct histories agree below the recursion argument

The successor step of primitive recursion

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codePrec_succ {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] {k : ℕ} (df : Nat.ArithPart₁.Code k) (dg : Nat.ArithPart₁.Code (k + 2)) (a z : M) (v : Fin k → M) (h : (FFL.FirstOrder.Semiformula.Evalb (z :> (a + 1) :> v)) (FFL.FirstOrder.Arithmetic.code (codePrec df dg))) : ∃ (w : M), (FFL.FirstOrder.Semiformula.Evalb (w :> a :> v)) (FFL.FirstOrder.Arithmetic.code (codePrec df dg)) ∧ (FFL.FirstOrder.Semiformula.Evalb (z :> a :> w :> v)) (FFL.FirstOrder.Arithmetic.code dg)

Evaluating codePrec df dg at a + 1 gives the value at a together with one application of the step code.

The two evaluations read different correct histories, so the proof aligns their entries by Sigma-one induction before reading the predecessor value.

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codePrec_zero {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {k : ℕ} (df : Nat.ArithPart₁.Code k) (dg : Nat.ArithPart₁.Code (k + 2)) (z : M) (v : Fin k → M) (h : (FFL.FirstOrder.Semiformula.Evalb (z :> 0 :> v)) (FFL.FirstOrder.Arithmetic.code (codePrec df dg))) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code df)

Evaluating codePrec df dg at zero gives the same value for the base code.

This is the forward direction only: a successful evaluation of the recursion at zero yields a successful evaluation of df with the same output. Nothing here asserts the converse.

Totality of the step relation

Introducing the bounded quantifier without a positive terminal step

Totality of the correctness predicate at an arbitrary history

Moving a history entry between the two-argument beta code and the

assignments of codePrecPredicate

Sigma-one definability of a literal code graph in two argument slots

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.definable_code_graph_arguments {M : Type u_1} [FFL.ORingStructure M] {k n : ℕ} (A : Nat.ArithPart₁.Code k) (arguments : Fin (k + 1) → FFL.FirstOrder.Semiterm ℒₒᵣ M n) : { Γ := Σ, rank := 1 }.Definable fun (w : Fin n → M) => (FFL.FirstOrder.Semiformula.Evalb (FFL.FirstOrder.Semiterm.val w id ∘ arguments)) (FFL.FirstOrder.Arithmetic.code A)

Substituting terms with model parameters into a code graph preserves Sigma-one definability.

Building a correct history

Generic existence for the recursion constructor

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codePrec_exists_of_total {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] {k : ℕ} (df : Nat.ArithPart₁.Code k) (dg : Nat.ArithPart₁.Code (k + 2)) (a : M) (v : Fin k → M) (hdf : ∃ (z : M), (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code df)) (hdg : ∀ i ≤ a, ∀ (z : M), ∃ (w : M), (FFL.FirstOrder.Semiformula.Evalb (w :> i :> z :> v)) (FFL.FirstOrder.Arithmetic.code dg)) : ∃ (z : M), (FFL.FirstOrder.Semiformula.Evalb (z :> a :> v)) (FFL.FirstOrder.Arithmetic.code (codePrec df dg))

codePrec df dg has a value at every recursion argument at which the base code has one and the step code is total at every index up to that argument.

The step premise is uniform in the predecessor value and is required only up to the recursion argument itself. The index a is included because the eager bounded search of codeBall evaluates the step there as well; nothing beyond a is used.

Halving

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codeDiv2_exists_of_value {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] {k : ℕ} (A : Nat.ArithPart₁.Code k) (a : M) (v : Fin k → M) (hA : (FFL.FirstOrder.Semiformula.Evalb (a :> v)) (FFL.FirstOrder.Arithmetic.code A)) : ∃ (z : M), (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeDiv2 A))

codeDiv2 A has a value at any value of A.

codeDiv2Unary is codePrec with a zero base and an eager conditional on the parity of the recursion index as step, so eval_codePrec_exists_of_total applies: the step has a value at every index and every predecessor value. Only existence is asserted; the witness is not identified with any quotient of a.