Documentation

LeanPool.PointwiseComposition.FailureOfComposition.GeneratedCollapse

Supporting results for pointwise provable equality.

The two algebraic halves of the generated-congruence dichotomy. Sigma-one soundness makes the closure extensionally sound; a false proved Sigma-one sentence collapses it once extensional containment has been established.

source
def PointwiseComposition.FailureOfComposition.GeneratedCongruence.deltaGraph (σ : Σ₁.Sentence) :
ProofSearch.Graph

The delta Graph construction in FailureOfComposition.GeneratedCongruence.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.deltaGraph_eval {M : Type u_1} [FFL.ORingStructure M] (σ : Σ₁.Sentence) (v : Fin 2 → M) :
    (FFL.FirstOrder.Semiformula.Evalb v) ↑(deltaGraph σ) ↔ (FFL.FirstOrder.Semiformula.Evalb ![]) ↑σ ∧ v 1 = v 0
    source
    theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.deltaGraph_functional (σ : Σ₁.Sentence) :
    ProofSearch.Functional (deltaGraph σ)
    source
    theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.deltaGraph_pointwise_identity (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (σ : Σ₁.Sentence) (hp : T ⊢ ↑σ) :
    ProofSearch.Pointwise T (deltaGraph σ) ProofSearch.identity
    source
    theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.deltaGraph_extensional_empty (σ : Σ₁.Sentence) (hn : ¬ℕ↓[ℒₒᵣ] ⊧ ↑σ) :
    PiOneCharacterization.Extensional (deltaGraph σ) ProofSearch.empty
    source
    theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.comp_right_identity (F : ProofSearch.Graph) :
    ProofSearch.Uniform 𝐏𝐀 (ProofSearch.comp F ProofSearch.identity) F
    source
    theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.comp_right_empty (F : ProofSearch.Graph) :
    ProofSearch.Uniform 𝐏𝐀 (ProofSearch.comp F ProofSearch.empty) ProofSearch.empty
    source
    def PointwiseComposition.FailureOfComposition.GeneratedCongruence.identityGraph :
    ProofSearch.FunctionalGraph

    The identity and empty graphs as PA-functional graph objects.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def PointwiseComposition.FailureOfComposition.GeneratedCongruence.emptyGraph :
      ProofSearch.FunctionalGraph

      The empty Graph construction in FailureOfComposition.GeneratedCongruence.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def PointwiseComposition.FailureOfComposition.GeneratedCongruence.deltaFunctionalGraph (σ : Σ₁.Sentence) :
        ProofSearch.FunctionalGraph

        The delta Functional Graph construction in FailureOfComposition.GeneratedCongruence.

        Equations
        Instances For
          source
          theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.collapse_of_identity_rel_empty (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (h : Rel T identityGraph emptyGraph) (F G : ProofSearch.FunctionalGraph) :
          Rel T F G

          Identifying the identity with the empty graph collapses every program.

          source
          theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.identity_rel_empty_of_false_proved_sigma_one (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (hExt : ∀ (F G : ProofSearch.FunctionalGraph), PiOneCharacterization.Extensional ↑F ↑G → Rel T F G) (σ : Σ₁.Sentence) (hp : T ⊢ ↑σ) (hn : ¬ℕ↓[ℒₒᵣ] ⊧ ↑σ) :
          Rel T identityGraph emptyGraph

          A false proved Sigma-one sentence identifies the identity and empty graphs once standard extensional equality is contained in the generated relation.

          source
          theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.collapse_of_not_sigmaOneSound (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (hExt : ∀ (F G : ProofSearch.FunctionalGraph), PiOneCharacterization.Extensional ↑F ↑G → Rel T F G) (hT : ¬SigmaOneSound T) (F G : ProofSearch.FunctionalGraph) :
          Rel T F G

          Without Sigma-one soundness the generated relation is universal. The extensional-containment hypothesis is discharged by the computation witnesses.

          source
          theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.generated_implies_extensional_of_sigmaOneSound (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (hT : SigmaOneSound T) {F G : ProofSearch.FunctionalGraph} (h : Rel T F G) :
          PiOneCharacterization.Extensional ↑F ↑G

          Sigma-one soundness makes the generated congruence extensionally sound.

          source
          theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.rel_iff_extensional_of_sigmaOneSound (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (hExt : ∀ (F G : ProofSearch.FunctionalGraph), PiOneCharacterization.Extensional ↑F ↑G → Rel T F G) (hT : SigmaOneSound T) (F G : ProofSearch.FunctionalGraph) :
          Rel T F G ↔ PiOneCharacterization.Extensional ↑F ↑G

          Extensional containment and Sigma-one soundness identify the generated relation with standard graph equality.