Documentation

LeanPool.PointwiseComposition.FailureOfComposition.ConcretePiOneCharacterization

Supporting results for pointwise provable equality.

The manuscript's four-way characterization for the actual natural-number program indices and history graphs. The ambient theory may be non-enumerable.

source
def PointwiseComposition.FailureOfComposition.ConcreteIndices.RightCompatible (T : FFL.FirstOrder.ArithmeticTheory) :
Prop

The Right Compatible construction in FailureOfComposition.ConcreteIndices.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def PointwiseComposition.FailureOfComposition.ConcreteIndices.CompositionCongruence (T : FFL.FirstOrder.ArithmeticTheory) :
    Prop

    The Composition Congruence construction in FailureOfComposition.ConcreteIndices.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def PointwiseComposition.FailureOfComposition.ConcreteIndices.AgreesWithExtensional (T : FFL.FirstOrder.ArithmeticTheory) :
      Prop

      The Agrees With Extensional construction in FailureOfComposition.ConcreteIndices.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.pointwiseIndex_comp_left (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (f g h : ℕ) (hgh : PointwiseIndex T g h) :
        PointwiseIndex T (CategoricalRiceShapiro.PartialRecursive.canonicalPartrecCompIndex f g) (CategoricalRiceShapiro.PartialRecursive.canonicalPartrecCompIndex f h)

        Left composition preserves pointwise provability for every PA extension.

        source
        theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.rightCompatible_implies_piOneComplete (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (h : RightCompatible T) :
        PiOneCharacterization.PiOneComplete T
        source
        theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.rightCompatible_iff_piOneComplete (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] :
        RightCompatible T ↔ PiOneCharacterization.PiOneComplete T
        source
        theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.compositionCongruence_iff_piOneComplete (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] :
        CompositionCongruence T ↔ PiOneCharacterization.PiOneComplete T
        source
        theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.agreesWithExtensional_iff_piOneComplete (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] :
        AgreesWithExtensional T ↔ PiOneCharacterization.PiOneComplete T
        source
        theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.pointwiseIndex_iff_evaluation_eq (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] (hT : PiOneCharacterization.PiOneComplete T) (e d : ℕ) :
        PointwiseIndex T e d ↔ Kleene.eval e = Kleene.eval d

        Pointwise provability is exactly equality of the computed partial functions when T is consistent and proves every true Pi-one sentence.

        source
        theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.pi_one_characterization (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] :
        (RightCompatible T ↔ CompositionCongruence T) ∧ (CompositionCongruence T ↔ PiOneCharacterization.PiOneComplete T) ∧ (PiOneCharacterization.PiOneComplete T ↔ AgreesWithExtensional T)

        The four statements of the characterization, without a realization or recursive-enumerability hypothesis.

        source
        theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.no_index_quotient_iff_not_piOneComplete (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] :
        NoIndexQuotientComposition T ↔ ¬PiOneCharacterization.PiOneComplete T

        Induced quotient composition fails exactly when Pi-one completeness fails.