Documentation

LeanPool.PointwiseComposition.FailureOfComposition.ProductiveDivergence

Supporting results for pointwise provable equality.

The productiveness proof of a true unprovable divergence sentence. This module does not import or invoke second incompleteness.

source
theorem PointwiseComposition.FailureOfComposition.diagonalHalts_re :
REPred diagonalHalts
source
noncomputable def PointwiseComposition.FailureOfComposition.diagonalHaltingFormula :
FFL.FirstOrder.ArithmeticSemisentence 1

The diagonal Halting Formula construction in FailureOfComposition.

Equations
Instances For
    source
    theorem PointwiseComposition.FailureOfComposition.diagonalHaltingFormula_sigma :
    FFL.FirstOrder.Arithmetic.Hierarchy Σ 1 diagonalHaltingFormula
    source
    theorem PointwiseComposition.FailureOfComposition.diagonalHaltingFormula_nat (n : ℕ) :
    (FFL.FirstOrder.Semiformula.Evalb ![n]) diagonalHaltingFormula ↔ diagonalHalts n
    source
    def PointwiseComposition.FailureOfComposition.provableDivergence (T : FFL.FirstOrder.ArithmeticTheory) (n : ℕ) :
    Prop

    The provable Divergence construction in FailureOfComposition.

    Equations
    Instances For
      source
      def PointwiseComposition.FailureOfComposition.TheoremCodes (T : FFL.FirstOrder.ArithmeticTheory) (n : ℕ) :
      Prop

      The numerical set of all theorem codes, using Foundation's sentence coding.

      Equations
      Instances For
        source
        theorem PointwiseComposition.FailureOfComposition.provableDivergence_re_of_theorem_codes (T : FFL.FirstOrder.ArithmeticTheory) (hT : REPred (TheoremCodes T)) :
        REPred (provableDivergence T)

        Enumerability of the theorem-code set suffices; no Delta-one presentation of T is used in this theorem.

        source
        theorem PointwiseComposition.FailureOfComposition.provableDivergence_re (T : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ T] :
        REPred (provableDivergence T)
        source
        theorem PointwiseComposition.FailureOfComposition.provableDivergence_sound (T : FFL.FirstOrder.ArithmeticTheory) [𝐑₀ ≼ T] [FFL.Entailment.Consistent T] (n : ℕ) :
        provableDivergence T n → ¬diagonalHalts n

        Consistency suffices; Sigma-one soundness is not assumed.

        source
        theorem PointwiseComposition.FailureOfComposition.exists_true_unprovable_divergence (T : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ T] [𝐑₀ ≼ T] [FFL.Entailment.Consistent T] :
        ∃ (d : ℕ), ¬diagonalHalts d ∧ T ⊬ ∼diagonalHaltingFormula/[↑d]

        A concrete diagonal computation diverges, but its represented divergence is not provable in the consistent Delta-one-presented theory.

        source
        theorem PointwiseComposition.FailureOfComposition.exists_true_unprovable_divergence_of_theorem_codes (T : FFL.FirstOrder.ArithmeticTheory) [𝐑₀ ≼ T] [FFL.Entailment.Consistent T] (hT : REPred (TheoremCodes T)) :
        ∃ (d : ℕ), ¬diagonalHalts d ∧ T ⊬ ∼diagonalHaltingFormula/[↑d]