Documentation

LeanPool.PointwiseComposition.FailureOfComposition.ConcreteGeneratedCongruence

Supporting results for pointwise provable equality.

Generated-congruence classification for the concrete evaluator indices.

source
def PointwiseComposition.FailureOfComposition.ConcreteIndices.GeneratedRel (T : FFL.FirstOrder.ArithmeticTheory) :
ℕ → ℕ → Prop

The intersection of all composition congruences containing pointwise provability for the actual natural-number program indices.

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

    The generated Setoid construction in FailureOfComposition.ConcreteIndices.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.extensional_implies_generated (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (e d : ℕ) (h : Kleene.eval e = Kleene.eval d) :
      GeneratedRel T e d

      Equal partial functions are always identified by the generated congruence.

      source
      theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.generated_iff_extensional_of_sound (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (hT : GeneratedCongruence.SigmaOneSound T) (e d : ℕ) :
      GeneratedRel T e d ↔ Kleene.eval e = Kleene.eval d
      source
      theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.generated_universal_of_not_sound (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (hT : ¬GeneratedCongruence.SigmaOneSound T) (e d : ℕ) :
      GeneratedRel T e d
      source
      theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.generated_congruence_classification (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] :
      (GeneratedCongruence.SigmaOneSound T → ∀ (e d : ℕ), GeneratedRel T e d ↔ Kleene.eval e = Kleene.eval d) ∧ (¬GeneratedCongruence.SigmaOneSound T → ∀ (e d : ℕ), GeneratedRel T e d)

      The generated-congruence theorem for every extension of PA. There is no consistency, enumerability, or supplied realization hypothesis.

      source
      theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.generated_iff_extensional_or_unsound (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (e d : ℕ) :
      GeneratedRel T e d ↔ Kleene.eval e = Kleene.eval d ∨ ¬GeneratedCongruence.SigmaOneSound T
      source
      theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.pa_generated_iff_extensional (e d : ℕ) :
      GeneratedRel 𝐏𝐀 e d ↔ Kleene.eval e = Kleene.eval d

      In particular, closing PA-pointwise equality under composition gives exactly extensional equality.

      source
      @[reducible, inline]
      abbrev PointwiseComposition.FailureOfComposition.ConcreteIndices.GeneratedQuotient (T : FFL.FirstOrder.ArithmeticTheory) :
      Type

      The Generated Quotient construction in FailureOfComposition.ConcreteIndices.

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

        The generated Quotient Mk construction in FailureOfComposition.ConcreteIndices.

        Equations
        Instances For
          source
          theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.generated_quotient_mul_mk (T : FFL.FirstOrder.ArithmeticTheory) (e d : ℕ) :
          generatedQuotientMk T e * generatedQuotientMk T d = generatedQuotientMk T (CategoricalRiceShapiro.PartialRecursive.canonicalPartrecCompIndex e d)
          source
          noncomputable def PointwiseComposition.FailureOfComposition.ConcreteIndices.generatedQuotientMulEquiv (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] :
          GeneratedQuotient T ≃* GeneratedCongruence.QuotientGraph T

          The concrete index quotient and functional-graph quotient are isomorphic as monoids, with their induced composition operations.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.generated_quotient_subsingleton_iff_not_sound (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] :
            Subsingleton (GeneratedQuotient T) ↔ ¬GeneratedCongruence.SigmaOneSound T