Documentation

LeanPool.PointwiseComposition.FailureOfComposition.GeneratedExtensionality

Supporting results for pointwise provable equality.

Extensional containment in the generated composition congruence.

source
def PointwiseComposition.FailureOfComposition.GeneratedCongruence.concreteGraph (e : ℕ) :
ProofSearch.FunctionalGraph

The concrete Graph construction in FailureOfComposition.GeneratedCongruence.

Equations
Instances For
    source
    def PointwiseComposition.FailureOfComposition.GeneratedCongruence.intersectionGraph (F G : ProofSearch.FunctionalGraph) :
    ProofSearch.FunctionalGraph

    The intersection Graph construction in FailureOfComposition.GeneratedCongruence.

    Equations
    Instances For
      source
      theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.uniform_extensional {F G : ProofSearch.Graph} (h : ProofSearch.Uniform 𝐏𝐀 F G) :
      PiOneCharacterization.Extensional F G

      PA-uniform equality in particular identifies standard graph extensions.

      source
      theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.concrete_rel_intersection (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (e : ℕ) (G : ProofSearch.FunctionalGraph) (hExt : PiOneCharacterization.Extensional ↑(concreteGraph e) ↑G) :
      Rel T (concreteGraph e) (intersectionGraph (concreteGraph e) G)

      The least-stage witnesses identify a concrete graph with its intersection with any extensionally equal graph in every generated congruence.

      source
      theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.concrete_extensional_implies_generated (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (e d : ℕ) (h : PiOneCharacterization.Extensional ↑(concreteGraph e) ↑(concreteGraph d)) :
      Rel T (concreteGraph e) (concreteGraph d)
      source
      theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.extensional_implies_generated (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (F G : ProofSearch.FunctionalGraph) (h : PiOneCharacterization.Extensional ↑F ↑G) :
      Rel T F G

      Extensional equality is contained in the congruence generated by pointwise provability for every extension of PA, without consistency or soundness.