Supporting results for pointwise provable equality.
Arithmetic graph equations for actual primitive-recursion program indices. The equations hold over arbitrary PA models, including nonstandard inputs.
theorem
PointwiseComposition.FailureOfComposition.ConcreteEvaluator.evaln_tag_six_zero_iff
{M : Type u_1}
[FFL.ORingStructure M]
[M↓[ℒₒᵣ] ⊧* 𝐏𝐀]
[M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧]
(q : ℕ)
(hq : CategoricalRiceShapiro.ArithmeticCode.partrecCodeTag q = 6)
(s z y : M)
(hs : 0 < s)
:
At a positive stage, zero-argument primitive recursion is the base program, with the caller's argument bound imposed by the concrete evaluator.
theorem
PointwiseComposition.FailureOfComposition.ConcreteEvaluator.evaln_tag_six_succ_iff
{M : Type u_1}
[FFL.ORingStructure M]
[M↓[ℒₒᵣ] ⊧* 𝐏𝐀]
[M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧]
(q : ℕ)
(hq : CategoricalRiceShapiro.ArithmeticCode.partrecCodeTag q = 6)
(k z a y : M)
:
(FFL.FirstOrder.Semiformula.Evalb ![k + 1, ↑q, ⟪z, a + 1⟫, y])
↑CategoricalRiceShapiro.Evaluator.evalnCertificateFormula ↔ ⟪z, a + 1⟫ < k + 1 ∧ ∃ (x : M),
(FFL.FirstOrder.Semiformula.Evalb ![k, ↑q, ⟪z, a⟫, x]) ↑CategoricalRiceShapiro.Evaluator.evalnCertificateFormula ∧ (FFL.FirstOrder.Semiformula.Evalb
![k + 1, ↑(CategoricalRiceShapiro.ArithmeticCode.partrecCodePayload₂ q), ⟪z, ⟪a, x⟫⟫, y])
↑CategoricalRiceShapiro.Evaluator.evalnCertificateFormula
A successor recursion computation at stage k + 1 consists of the
predecessor computation at stage k and the step computation at stage k + 1.
theorem
PointwiseComposition.FailureOfComposition.ConcreteEvaluator.eventualGraph_prec_zero_eval
{M : Type u_1}
[FFL.ORingStructure M]
[M↓[ℒₒᵣ] ⊧* 𝐏𝐀]
[M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧]
(fCode gCode : ℕ)
(z y : M)
:
(FFL.FirstOrder.Semiformula.Evalb ![⟪z, 0⟫, y])
↑(eventualGraph (CategoricalRiceShapiro.PartialRecursive.canonicalPartrecPrecIndex fCode gCode)) ↔ (FFL.FirstOrder.Semiformula.Evalb ![z, y]) ↑(eventualGraph fCode)
Primitive recursion at zero realizes the base graph in every PA model.
theorem
PointwiseComposition.FailureOfComposition.ConcreteEvaluator.eventualGraph_prec_succ_eval
{M : Type u_1}
[FFL.ORingStructure M]
[M↓[ℒₒᵣ] ⊧* 𝐏𝐀]
[M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧]
(fCode gCode : ℕ)
(z a y : M)
:
(FFL.FirstOrder.Semiformula.Evalb ![⟪z, a + 1⟫, y])
↑(eventualGraph (CategoricalRiceShapiro.PartialRecursive.canonicalPartrecPrecIndex fCode gCode)) ↔ ∃ (x : M),
(FFL.FirstOrder.Semiformula.Evalb ![⟪z, a⟫, x])
↑(eventualGraph (CategoricalRiceShapiro.PartialRecursive.canonicalPartrecPrecIndex fCode gCode)) ∧ (FFL.FirstOrder.Semiformula.Evalb ![⟪z, ⟪a, x⟫⟫, y]) ↑(eventualGraph gCode)
Primitive recursion at a successor realizes the predecessor-then-step graph in every PA model. The recursion argument may be nonstandard.