Supporting results for pointwise provable equality.

Internal semidecision and program realization of Sigma-one arithmetic formulas. Every program is constructed from concrete Mathlib program descriptions, and every correctness assertion quantifies over PA models rather than just ℕ.

def PointwiseComposition.FailureOfComposition.SigmaOneRealization.truthProgram (c : ProgramGraph.PCode) : ProgramGraph.PCode

Accept the nonzero output of a Boolean program and return zero.

Equations

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

theorem PointwiseComposition.FailureOfComposition.SigmaOneRealization.computes_truthProgram {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (c : ProgramGraph.PCode) (x y : M) : ProgramGraph.Computes (truthProgram c) x y ↔ y = 0 ∧ ∃ (z : M), z ≠ 0 ∧ ProgramGraph.Computes c x z

theorem PointwiseComposition.FailureOfComposition.SigmaOneRealization.atom_semidecides {n k : ℕ} (r : FFL.FirstOrder.Language.ORing.Rel k) (ts : Fin k → FFL.FirstOrder.ArithmeticSemiterm Empty n) : Semidecides (FFL.FirstOrder.Semiformula.rel r ts) (truthProgram (ArithmeticCodeCompiler.compile (ArithmeticFormulaAtoms.atomCode r ts)))

theorem PointwiseComposition.FailureOfComposition.SigmaOneRealization.negAtom_semidecides {n k : ℕ} (r : FFL.FirstOrder.Language.ORing.Rel k) (ts : Fin k → FFL.FirstOrder.ArithmeticSemiterm Empty n) : Semidecides (FFL.FirstOrder.Semiformula.nrel r ts) (truthProgram (ArithmeticCodeCompiler.compile (ArithmeticFormulaAtoms.negAtomCode r ts)))

def PointwiseComposition.FailureOfComposition.SigmaOneRealization.boundedProgram {n : ℕ} (t : FFL.FirstOrder.ArithmeticSemiterm Empty n) (c : ProgramGraph.PCode) : ProgramGraph.PCode

Evaluate the bound and sequentially check the formula at each smaller candidate, retaining the encoded environment as the recursion parameter.

Equations

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

theorem PointwiseComposition.FailureOfComposition.SigmaOneRealization.bounded_semidecides {n : ℕ} (t : FFL.FirstOrder.ArithmeticSemiterm Empty n) {φ : FFL.FirstOrder.ArithmeticSemisentence (n + 1)} {c : ProgramGraph.PCode} (hφ : Semidecides φ c) : Semidecides (“(∀¹[!!(FFL.FirstOrder.Semiterm.bvar 0) < !!(FFL.FirstOrder.Rew.bShift t)] !φ)”) (boundedProgram t c)

theorem PointwiseComposition.FailureOfComposition.SigmaOneRealization.or_semidecides {n : ℕ} {φ ψ : FFL.FirstOrder.ArithmeticSemisentence n} {c d : ProgramGraph.PCode} (hφ : Semidecides φ c) (hψ : Semidecides ψ d) : Semidecides (φ ⋎ ψ) (SigmaOneSearch.unionProgram c d)

theorem PointwiseComposition.FailureOfComposition.SigmaOneRealization.exists_semidecides {n : ℕ} {φ : FFL.FirstOrder.ArithmeticSemisentence (n + 1)} {c : ProgramGraph.PCode} (hφ : Semidecides φ c) : Semidecides (∃¹ φ) (SigmaOneSearch.existsProgram c)

theorem PointwiseComposition.FailureOfComposition.SigmaOneRealization.semidecision_exists {n : ℕ} (φ : FFL.FirstOrder.ArithmeticSemisentence n) (hφ : FFL.FirstOrder.Arithmetic.Hierarchy Σ 1 φ) : ∃ (c : ProgramGraph.PCode), Semidecides φ c

Every Sigma-one arithmetic formula has a concrete zero-valued semidecision program whose correctness holds in PA models.

theorem PointwiseComposition.FailureOfComposition.SigmaOneRealization.realize_graph (F : ProofSearch.Graph) (hF : ProofSearch.Functional F) : ∃ (e : ℕ), ProofSearch.Uniform 𝐏𝐀 (ConcreteEvaluator.eventualGraph e) F

Every PA-provably functional Sigma-one graph has a program in the fixed Mathlib numbering whose graph PA proves uniformly equivalent to it.