Documentation

LeanPool.PointwiseComposition.FailureOfComposition.PiOneExtensionality

Supporting results for pointwise provable equality.

Pi-one completeness identifies external pointwise provability with equality of functional Sigma-one graphs on the natural numbers. No enumerability assumption is used.

source
def PointwiseComposition.FailureOfComposition.PiOneCharacterization.graphInstance (F : ProofSearch.Graph) (n m : ℕ) :
FFL.FirstOrder.ArithmeticSentence

A closed convergence assertion with both arguments standard numerals.

Equations
Instances For
    source
    def PointwiseComposition.FailureOfComposition.PiOneCharacterization.divergesAt (F : ProofSearch.Graph) (n : ℕ) :
    FFL.FirstOrder.ArithmeticSentence

    Absence of an output at one fixed standard input.

    Equations
    Instances For
      source
      theorem PointwiseComposition.FailureOfComposition.PiOneCharacterization.graphInstance_sigma_one (F : ProofSearch.Graph) (n m : ℕ) :
      FFL.FirstOrder.Arithmetic.Hierarchy Σ 1 (graphInstance F n m)
      source
      theorem PointwiseComposition.FailureOfComposition.PiOneCharacterization.divergesAt_pi_one (F : ProofSearch.Graph) (n : ℕ) :
      FFL.FirstOrder.Arithmetic.Hierarchy Π 1 (divergesAt F n)
      source
      @[simp]
      theorem PointwiseComposition.FailureOfComposition.PiOneCharacterization.graphInstance_eval {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (F : ProofSearch.Graph) (n m : ℕ) :
      (FFL.FirstOrder.Semiformula.Evalb ![]) (graphInstance F n m) ↔ (FFL.FirstOrder.Semiformula.Evalb ![↑n, ↑m]) ↑F
      source
      @[simp]
      theorem PointwiseComposition.FailureOfComposition.PiOneCharacterization.divergesAt_eval {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (F : ProofSearch.Graph) (n : ℕ) :
      (FFL.FirstOrder.Semiformula.Evalb ![]) (divergesAt F n) ↔ ∀ (y : M), ¬(FFL.FirstOrder.Semiformula.Evalb ![↑n, y]) ↑F
      source
      theorem PointwiseComposition.FailureOfComposition.PiOneCharacterization.sigma_one_sound_of_pi_one_complete (T : FFL.FirstOrder.ArithmeticTheory) [FFL.Entailment.Consistent T] (hT : PiOneComplete T) (σ : FFL.FirstOrder.ArithmeticSentence) (hσ : FFL.FirstOrder.Arithmetic.Hierarchy Σ 1 σ) (hp : T ⊢ σ) :
      ℕ↓[ℒₒᵣ] ⊧ σ

      A consistent Pi-one-complete theory cannot prove a false Sigma-one sentence: it already proves that sentence's true Pi-one negation.

      source
      theorem PointwiseComposition.FailureOfComposition.PiOneCharacterization.true_graph_instance_provable (F : ProofSearch.Graph) (n m : ℕ) (h : (FFL.FirstOrder.Semiformula.Evalb ![n, m]) ↑F) :
      𝐏𝐀 ⊢ graphInstance F n m

      True ground convergence assertions are provable already in PA.

      source
      theorem PointwiseComposition.FailureOfComposition.PiOneCharacterization.ground_proof_of_pointwise (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (F G : ProofSearch.Graph) (hFG : ProofSearch.Pointwise T F G) (n m : ℕ) (hF : (FFL.FirstOrder.Semiformula.Evalb ![n, m]) ↑F) :
      T ⊢ graphInstance G n m

      Pointwise provability transports a true ground graph instance to a proof in the theory.

      source
      theorem PointwiseComposition.FailureOfComposition.PiOneCharacterization.pointwise_implies_extensional (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] (hT : PiOneComplete T) (F G : ProofSearch.Graph) (hFG : ProofSearch.Pointwise T F G) :
      Extensional F G

      Pi-one completeness and consistency make pointwise provability sound for the represented graphs, including their individual convergence assertions.

      source
      theorem PointwiseComposition.FailureOfComposition.PiOneCharacterization.extensional_implies_pointwise (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (hT : PiOneComplete T) (F G : ProofSearch.Graph) (hF : ProofSearch.Functional F) (hG : ProofSearch.Functional G) (hFG : Extensional F G) :
      ProofSearch.Pointwise T F G

      Equality of functional standard graphs gives pointwise provability: common values use PA computation proofs; joint divergence uses Pi-one completeness. This direction does not require consistency.

      source
      theorem PointwiseComposition.FailureOfComposition.PiOneCharacterization.pointwise_iff_extensional (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] (hT : PiOneComplete T) (F G : ProofSearch.Graph) (hF : ProofSearch.Functional F) (hG : ProofSearch.Functional G) :
      ProofSearch.Pointwise T F G ↔ Extensional F G
      source
      theorem PointwiseComposition.FailureOfComposition.PiOneCharacterization.piOneComplete_implies_agreesWithExtensional (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] (hT : PiOneComplete T) :
      AgreesWithExtensional T