LeanPool.PointwiseComposition.FailureOfComposition.ManuscriptObstruction

Supporting results for pointwise provable equality.

The four conclusions of manuscript Theorem 1, retaining uniform provable equality in its two middle clauses. The concrete productive witnesses have these uniform graph equations already in PA, before passing to the theory T.

source

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

Prop

Uniform equality of the concrete arithmetic program graphs.

Equations

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

Instances For

source

def PointwiseComposition.FailureOfComposition.ConcreteIndices.uniformKleeneSentence (F G : ProofSearch.Graph) :

FFL.FirstOrder.ArithmeticSentence

The manuscript's Kleene equality formula, universally quantified over inputs.

Equations

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

Instances For

source

@[simp]

theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.uniformKleeneSentence_eval {M : Type u_1} [FFL.ORingStructure M] (F G : ProofSearch.Graph) :

(FFL.FirstOrder.Semiformula.Evalb ![]) (uniformKleeneSentence F G) ↔ ∀ (x : M), ((∃ (y : M), (FFL.FirstOrder.Semiformula.Evalb ![x, y]) ↑F) ↔ ∃ (y : M), (FFL.FirstOrder.Semiformula.Evalb ![x, y]) ↑G) ∧ ((∃ (y : M), (FFL.FirstOrder.Semiformula.Evalb ![x, y]) ↑F) → ∃ (y : M), (FFL.FirstOrder.Semiformula.Evalb ![x, y]) ↑F ∧ (FFL.FirstOrder.Semiformula.Evalb ![x, y]) ↑G)

The implication from output-graph equality to Kleene equality is pure first-order logic. The explicit LK construction below deliberately avoids the converse direction, functionality, PA, semantic completeness, and the later uniformKleeneSentence_iff_uniformSentence.

source

theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.uniformSentence_imp_uniformKleeneSentence (F G : ProofSearch.Graph) :

∅ ⊢ ProofSearch.uniformSentence F G ⇒ₗ uniformKleeneSentence F G

Pure LK proves that an internally universal graph biconditional implies the manuscript's internally universal Kleene-equality sentence.

source

theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.uniformKleeneSentence_of_uniformSentence (T : FFL.FirstOrder.ArithmeticTheory) (F G : ProofSearch.Graph) (h : T ⊢ ProofSearch.uniformSentence F G) :

T ⊢ uniformKleeneSentence F G

The one direction needed by the obstruction transport, over any theory.

source

theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.uniformKleeneSentence_iff_uniformSentence (F G : ProofSearch.Graph) (hF : ProofSearch.Functional F) (hG : ProofSearch.Functional G) :

𝐏𝐀 ⊢ uniformKleeneSentence F G ⇔ₗ ProofSearch.uniformSentence F G

PA functionality equates the two uniform encodings, at all internal inputs.

source

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

UniformIndex T e f ↔ T ⊢ uniformKleeneSentence (ConcreteEvaluator.eventualGraph e) (ConcreteEvaluator.eventualGraph f)

UniformIndex is precisely provability of the manuscript's uniform formula.

source

theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.identity_comp_uniformIndex (e : ℕ) :

UniformIndex 𝐏𝐀 (CategoricalRiceShapiro.PartialRecursive.canonicalPartrecCompIndex Kleene.identityIndex e) e

The concrete identity law is uniformly provable already in PA.

source

theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.guard_search_uniformIndex_empty (d : ℕ) :

UniformIndex 𝐏𝐀 (CategoricalRiceShapiro.PartialRecursive.canonicalPartrecCompIndex (guardIndex d) (searchIndex d)) ConcreteEmptyGraph.concreteEmptyIndex

The guard-search composite has uniformly empty graph already in PA.

source

The four manuscript properties, with the stronger PA-uniform middle clauses.

source

Theorem 1's four properties for every consistent recursively axiomatized extension of PA. Uniform provability is retained, not replaced by its instances.

source

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

∃ (f : ℕ) (g : ℕ), PointwiseIndex T f Kleene.identityIndex ∧ UniformIndex T (CategoricalRiceShapiro.PartialRecursive.canonicalPartrecCompIndex f g) ConcreteEmptyGraph.concreteEmptyIndex ∧ UniformIndex T (CategoricalRiceShapiro.PartialRecursive.canonicalPartrecCompIndex Kleene.identityIndex g) g ∧ ¬PointwiseIndex T g ConcreteEmptyGraph.concreteEmptyIndex

The explicit partial-recursive axiom-enumerator presentation of Theorem 1.