Documentation

LeanPool.PointwiseComposition.FailureOfComposition.ConcreteDiagonal

Supporting results for pointwise provable equality.

Productiveness for the diagonal halting formula of the actual history evaluator. The formula is built directly from evalnCertificateFormula; no representation chosen by codeOfREPred occurs in its definition.

source
def PointwiseComposition.FailureOfComposition.ConcreteEvaluator.diagonalHistoryFormula :
FFL.FirstOrder.ArithmeticSemisentence 1

The diagonal computation of the actual arithmetized history evaluator.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.diagonalHistoryFormula_sigma :
    FFL.FirstOrder.Arithmetic.Hierarchy Σ 1 diagonalHistoryFormula
    source
    theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.diagonalHistoryFormula_eval_model {M : Type u_1} [FFL.ORingStructure M] (q : M) :
    (FFL.FirstOrder.Semiformula.Evalb ![q]) diagonalHistoryFormula ↔ ∃ (s : M) (y : M), (FFL.FirstOrder.Semiformula.Evalb ![s, q, q, y]) ↑CategoricalRiceShapiro.Evaluator.evalnCertificateFormula

    The diagonal formula quantifies over all model stages and outputs.

    source
    theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.diagonalHistoryFormula_eval (n : ℕ) :
    (FFL.FirstOrder.Semiformula.Evalb ![n]) diagonalHistoryFormula ↔ ∃ (y : ℕ), (FFL.FirstOrder.Semiformula.Evalb ![n, y]) ↑(eventualGraph n)

    Specializing the program parameter is the same as its fixed-index graph.

    source
    def PointwiseComposition.FailureOfComposition.ConcreteEvaluator.provableHistoryDivergence (T : FFL.FirstOrder.ArithmeticTheory) (n : ℕ) :
    Prop

    The represented divergence sentences provable in T.

    Equations
    Instances For
      source
      theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.provableHistoryDivergence_re_of_theorem_codes (T : FFL.FirstOrder.ArithmeticTheory) (hT : REPred (TheoremCodes T)) :
      REPred (provableHistoryDivergence T)

      The theorem-code assumption directly enumerates these concrete sentences.

      source
      theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.provableHistoryDivergence_re (T : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ T] :
      REPred (provableHistoryDivergence T)

      A Delta-one theory presentation also enumerates the concrete sentences.

      source
      theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.provableHistoryDivergence_sound_eval (T : FFL.FirstOrder.ArithmeticTheory) [𝐑₀ ≼ T] [FFL.Entailment.Consistent T] (n : ℕ) :
      provableHistoryDivergence T n → ¬(FFL.FirstOrder.Semiformula.Evalb ![n]) diagonalHistoryFormula

      Consistency excludes a proved divergence when this concrete Sigma-one halting formula is true. No Sigma-one soundness assumption on T is needed.

      source
      theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.diagonalHistoryFormula_nat (n : ℕ) :
      (FFL.FirstOrder.Semiformula.Evalb ![n]) diagonalHistoryFormula ↔ diagonalHalts n

      Standard-model adequacy for the actual diagonal history formula.

      source
      theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.provableHistoryDivergence_sound (T : FFL.FirstOrder.ArithmeticTheory) [𝐑₀ ≼ T] [FFL.Entailment.Consistent T] (n : ℕ) :
      provableHistoryDivergence T n → ¬diagonalHalts n

      Consistency suffices to make the enumerable provable-divergence set a subset of the genuinely divergent diagonal computations.

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

      Productiveness supplies an unprovable divergence sentence for the actual program-index history formula, without Gödel's second incompleteness theorem.

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

      The same result from Foundation's Delta-one theory presentation.

      source
      theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.exists_true_unprovable_history_divergence_of_theorem_codes (T : FFL.FirstOrder.ArithmeticTheory) [𝐑₀ ≼ T] [FFL.Entailment.Consistent T] (hT : REPred (TheoremCodes T)) :
      ∃ (d : ℕ), ¬(FFL.FirstOrder.Semiformula.Evalb ![d]) diagonalHistoryFormula ∧ T ⊬ ∼diagonalHistoryFormula/[↑d]

      The selected divergence is true for the concrete arithmetical formula.

      source
      theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.exists_true_unprovable_history_divergence (T : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ T] [𝐑₀ ≼ T] [FFL.Entailment.Consistent T] :
      ∃ (d : ℕ), ¬(FFL.FirstOrder.Semiformula.Evalb ![d]) diagonalHistoryFormula ∧ T ⊬ ∼diagonalHistoryFormula/[↑d]

      Concrete arithmetical divergence under a Delta-one theory presentation.