Supporting results for pointwise provable equality.

The manuscript's range obstruction via Gödel's second incompleteness theorem. A program that outputs zero on codes of proofs of contradiction agrees pointwise with the empty program. Its range at zero encodes the existence of a contradiction proof. Craig's presentation removes the Delta-one axiom-presentation hypothesis.

noncomputable def PointwiseComposition.FailureOfComposition.ConcreteIndices.proofBotPredicate (T : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ T] : Σ₁.Semisentence 1

The positive proof-of-contradiction predicate of the chosen presentation.

Equations

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

theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.proofBotPredicate_numeral_refutation (T : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ T] [FFL.Entailment.Consistent T] (n : ℕ) : 𝐏𝐀 ⊢ ∼↑(proofBotPredicate T)/[↑n]

Consistency refutes each fixed proof code in PA, including the Sigma-one form.

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

Universal absence of contradiction proofs would establish the theory's own consistency, which Gödel's second incompleteness theorem excludes.

theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.range_counterexample_via_godel (T : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ T] [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] : PointwiseIndex T (probeIndex (proofBotPredicate T)) ConcreteEmptyGraph.concreteEmptyIndex ∧ ¬PointwiseIndex T (rangeIndex (probeIndex (proofBotPredicate T))) (rangeIndex ConcreteEmptyGraph.concreteEmptyIndex)

The manuscript's zero-output proof probe is pointwise empty, but its range program is not pointwise equal to the empty program's range.

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

A quotient range operation would contradict the concrete Gödel-II witnesses.

theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.range_counterexample_of_equivalent_presentation (S T : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ S] [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] (hST : S ≼ T) (hTS : T ≼ S) : ∃ (u : ℕ), PointwiseIndex T u ConcreteEmptyGraph.concreteEmptyIndex ∧ ¬PointwiseIndex T (rangeIndex u) (rangeIndex ConcreteEmptyGraph.concreteEmptyIndex)

Deductive equivalence transports the same natural-number witnesses. The chosen range indices depend on their programs, not on the theory presentation.

theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.range_counterexample_of_re_axioms (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] (hT : REPred (AxiomCodes T)) : ∃ (u : ℕ), PointwiseIndex T u ConcreteEmptyGraph.concreteEmptyIndex ∧ ¬PointwiseIndex T (rangeIndex u) (rangeIndex ConcreteEmptyGraph.concreteEmptyIndex)

For every consistent recursively axiomatized extension of PA, range assignment fails to preserve the external pointwise relation.

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

The range assignment does not descend to the quotient in the manuscript's full recursively enumerable axiom setting.

theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.range_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) : ∃ (u : ℕ), PointwiseIndex T u ConcreteEmptyGraph.concreteEmptyIndex ∧ ¬PointwiseIndex T (rangeIndex u) (rangeIndex ConcreteEmptyGraph.concreteEmptyIndex)

The explicit axiom-program enumeration used in the manuscript suffices.

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

No quotient range operation exists for an explicitly enumerated axiom set.

theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.pa_range_counterexample : ∃ (u : ℕ), PointwiseIndex 𝐏𝐀 u ConcreteEmptyGraph.concreteEmptyIndex ∧ ¬PointwiseIndex 𝐏𝐀 (rangeIndex u) (rangeIndex ConcreteEmptyGraph.concreteEmptyIndex)

The proof-of-contradiction probe supplies the obstruction already over PA.

theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.pa_no_index_quotient_range : NoIndexQuotientRange 𝐏𝐀

The range assignment does not descend to the external pointwise quotient of PA.