Documentation

LeanPool.PointwiseComposition.FailureOfComposition.ConcreteEmptyGraph

Supporting results for pointwise provable equality.

A concrete nowhere-defined program in the accepted Mathlib numbering. The program searches for a zero of successor; its index is 11. Its graph is proved empty inside every model of PA, including nonstandard models.

source
def PointwiseComposition.FailureOfComposition.ConcreteEmptyGraph.concreteEmptyIndex :
ℕ

Search for a zero of successor, starting from the supplied search position.

Equations
Instances For
    source
    @[simp]
    theorem PointwiseComposition.FailureOfComposition.ConcreteEmptyGraph.concreteEmptyIndex_eq :
    concreteEmptyIndex = 11
    source
    def PointwiseComposition.FailureOfComposition.ConcreteEmptyGraph.noComputationFormula (q : ℕ) :
    FFL.FirstOrder.ArithmeticSemisentence 1

    Absence of successful computations at a stage, expressed in PA's language.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem PointwiseComposition.FailureOfComposition.ConcreteEmptyGraph.concreteEmpty_no_computation {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (s u y : M) :
      ¬(FFL.FirstOrder.Semiformula.Evalb ![s, ↑concreteEmptyIndex, u, y]) ↑CategoricalRiceShapiro.Evaluator.evalnCertificateFormula

      No stage, input, or output in a PA model is a successful computation of rfind' succ; the induction is PA induction on the model's stage parameter.

      source
      theorem PointwiseComposition.FailureOfComposition.ConcreteEmptyGraph.concreteEmpty_unbounded_computation_iff {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (u y : M) :
      (∃ (s : M), (FFL.FirstOrder.Semiformula.Evalb ![s, ↑concreteEmptyIndex, u, y]) ↑CategoricalRiceShapiro.Evaluator.evalnCertificateFormula) ↔ False

      The unbounded computation graph of the concrete empty program is empty.