Documentation

LeanPool.PointwiseComposition.FailureOfComposition.ConcreteWeakTotality

Supporting results for pointwise provable equality.

Concrete weak-totality witnesses for the manuscript's external pointwise provability relation. The guard agrees pointwise with identity, but annihilates a search program that is not provably empty. Consequently weak totality cannot be assigned to the pointwise quotient independently of a representative.

def PointwiseComposition.FailureOfComposition.ConcreteIndices.WeaklyTotalIndex (T : FFL.FirstOrder.ArithmeticTheory) (e : ℕ) :

The manuscript's weak-totality predicate on concrete program indices.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.identity_comp_pointwiseIndex (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (e : ℕ) :

PointwiseIndex T (CategoricalRiceShapiro.PartialRecursive.canonicalPartrecCompIndex Kleene.identityIndex e) e

Identity is a left identity for the external pointwise index relation.

theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.guardIndex_pointwise_identity (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (d : ℕ) (hdiv : ¬(FFL.FirstOrder.Semiformula.Evalb ![d]) ConcreteEvaluator.diagonalHistoryFormula) :

PointwiseIndex T (guardIndex d) Kleene.identityIndex

Every standard instance of the divergent guard agrees provably with identity.

theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.guard_search_pointwise_empty (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (d : ℕ) :

PointwiseIndex T (CategoricalRiceShapiro.PartialRecursive.canonicalPartrecCompIndex (guardIndex d) (searchIndex d)) ConcreteEmptyGraph.concreteEmptyIndex

The guard annihilates its associated least-success search in PA.

theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.searchIndex_not_pointwise_empty (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (d : ℕ) (hnot : T ⊬ ∼ConcreteEvaluator.diagonalHistoryFormula /[↑d]) :

¬PointwiseIndex T (searchIndex d) ConcreteEmptyGraph.concreteEmptyIndex

Proving the search empty would prove the chosen divergence sentence.

All four concrete witnesses used for composition and weak-totality failure.

theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.weaklyTotalIndex_identity (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] :

WeaklyTotalIndex T Kleene.identityIndex

Identity is weakly total without any consistency or enumerability hypothesis.

theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.not_weaklyTotalIndex_guard (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (d : ℕ) (hnot : T ⊬ ∼ConcreteEvaluator.diagonalHistoryFormula /[↑d]) :

¬WeaklyTotalIndex T (guardIndex d)

The search witness refutes weak totality of the guard.

A true unprovable divergence gives equivalent indices of different weak totality.

theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.weak_totality_counterexample_via_productiveness (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] (hT : REPred (TheoremCodes T)) :

∃ (d : ℕ), PointwiseIndex T (guardIndex d) Kleene.identityIndex ∧ ¬WeaklyTotalIndex T (guardIndex d) ∧ WeaklyTotalIndex T Kleene.identityIndex

Productiveness supplies a concrete counterexample for every consistent extension of PA with recursively enumerable theorem codes.

theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.weak_totality_counterexample_of_delta_one (T : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ T] [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] :

∃ (d : ℕ), PointwiseIndex T (guardIndex d) Kleene.identityIndex ∧ ¬WeaklyTotalIndex T (guardIndex d) ∧ WeaklyTotalIndex T Kleene.identityIndex

The decidable axiom-presentation specialization.

theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.weak_totality_counterexample_of_re_axioms (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] (hT : REPred (AxiomCodes T)) :

∃ (d : ℕ), PointwiseIndex T (guardIndex d) Kleene.identityIndex ∧ ¬WeaklyTotalIndex T (guardIndex d) ∧ WeaklyTotalIndex T Kleene.identityIndex

Recursively enumerable axiom codes suffice for weak-totality failure.

theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.weak_totality_counterexample_of_axiom_enumerator (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] (a : ℕ) (ha : ∀ (n : ℕ), AxiomCodes T n ↔ ∃ (x : ℕ), n ∈ Kleene.eval a x) :

∃ (d : ℕ), PointwiseIndex T (guardIndex d) Kleene.identityIndex ∧ ¬WeaklyTotalIndex T (guardIndex d) ∧ WeaklyTotalIndex T Kleene.identityIndex

The explicit program enumeration of axioms used in the manuscript.

theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.no_quotient_weak_totality_of_history_divergence (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (d : ℕ) (hdiv : ¬(FFL.FirstOrder.Semiformula.Evalb ![d]) ConcreteEvaluator.diagonalHistoryFormula) (hnot : T ⊬ ∼ConcreteEvaluator.diagonalHistoryFormula /[↑d]) :

¬∃ (P : Quotient (indexSetoid T) → Prop), ∀ (e : ℕ), P ⟦e⟧ ↔ WeaklyTotalIndex T e

No predicate on the pointwise quotient represents weak totality of its indices.

theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.no_quotient_weak_totality_of_re_axioms (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] (hT : REPred (AxiomCodes T)) :

¬∃ (P : Quotient (indexSetoid T) → Prop), ∀ (e : ℕ), P ⟦e⟧ ↔ WeaklyTotalIndex T e

Weak totality does not descend for any consistent recursively axiomatized extension of PA.