Documentation

LeanPool.PointwiseComposition.FailureOfComposition.ConcreteIndexObstruction

Supporting results for pointwise provable equality.

Concrete natural-number witnesses for the failure of quotient composition. The graphs are the production history evaluator, and the guard/search indices are obtained by the proved structural compiler, without an Arithmetization parameter or a graph-realization hypothesis.

source
def PointwiseComposition.FailureOfComposition.ConcreteIndices.guardIndex (d : ℕ) :
ℕ

The guard Index construction in FailureOfComposition.ConcreteIndices.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def PointwiseComposition.FailureOfComposition.ConcreteIndices.searchIndex (d : ℕ) :
    ℕ

    The search Index construction in FailureOfComposition.ConcreteIndices.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.guardIndex_realizes (d : ℕ) :
      ProofSearch.Uniform 𝐏𝐀 (ConcreteEvaluator.eventualGraph (guardIndex d)) (HistoryWitnesses.guardGraph d)
      source
      theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.searchIndex_realizes (d : ℕ) :
      ProofSearch.Uniform 𝐏𝐀 (ConcreteEvaluator.eventualGraph (searchIndex d)) (HistoryWitnesses.searchGraph d)
      source
      def PointwiseComposition.FailureOfComposition.ConcreteIndices.PointwiseIndex (T : FFL.FirstOrder.ArithmeticTheory) (e f : ℕ) :
      Prop

      The external input quantifier of Montagna's relation.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.pointwiseIndex_iff (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (e f : ℕ) :
        PointwiseIndex T e f ↔ ProofSearch.Pointwise T (ConcreteEvaluator.eventualGraph e) (ConcreteEvaluator.eventualGraph f)
        source
        def PointwiseComposition.FailureOfComposition.ConcreteIndices.indexSetoid (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] :
        Setoid ℕ

        The index Setoid construction in FailureOfComposition.ConcreteIndices.

        Equations
        Instances For
          source
          def PointwiseComposition.FailureOfComposition.ConcreteIndices.NoIndexQuotientComposition (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] :
          Prop

          The No Index Quotient Composition construction in FailureOfComposition.ConcreteIndices.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.index_noncongruence_of_history_divergence (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (d : ℕ) (hdiv : ¬(FFL.FirstOrder.Semiformula.Evalb ![d]) ConcreteEvaluator.diagonalHistoryFormula) (hnot : T ⊬ ∼ConcreteEvaluator.diagonalHistoryFormula/[↑d]) :
            PointwiseIndex T (guardIndex d) Kleene.identityIndex ∧ ¬PointwiseIndex T (CategoricalRiceShapiro.PartialRecursive.canonicalPartrecCompIndex (guardIndex d) (searchIndex d)) (CategoricalRiceShapiro.PartialRecursive.canonicalPartrecCompIndex Kleene.identityIndex (searchIndex d))
            source
            theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.no_index_quotient_of_history_divergence (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (d : ℕ) (hdiv : ¬(FFL.FirstOrder.Semiformula.Evalb ![d]) ConcreteEvaluator.diagonalHistoryFormula) (hnot : T ⊬ ∼ConcreteEvaluator.diagonalHistoryFormula/[↑d]) :
            NoIndexQuotientComposition T
            source
            theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.no_index_quotient_via_productiveness (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] (hT : REPred (TheoremCodes T)) :
            NoIndexQuotientComposition T

            Concrete obstruction, using only consistency and an r.e. theorem set.

            source
            theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.no_index_quotient_of_delta_one (T : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ T] [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] :
            NoIndexQuotientComposition T

            The decidable axiom-presentation specialization.

            source
            theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.no_index_quotient_of_re_axioms (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] (hT : REPred (AxiomCodes T)) :
            NoIndexQuotientComposition T

            Every consistent extension of PA with recursively enumerable axiom codes has this concrete program-index quotient obstruction.

            source
            theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.no_index_quotient_of_axiom_enumerator (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] (a : ℕ) (ha : ∀ (n : ℕ), AxiomCodes T n ↔ ∃ (x : ℕ), n ∈ Kleene.eval a x) :
            NoIndexQuotientComposition T

            The explicit partial-recursive axiom enumeration used in v36.

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

            The manuscript's arithmetization assumptions with its r.e. axiom presentation; no separate theorem-code enumerability hypothesis remains.