Pointwise provable equality and the failure of composition
Abstract
In their studies of pathologies in recursion categories, Montagna (1989) and Di Paola--Montagna (1991) introduce the algebraic systems S' and S'T, respectively, and claim that they are categories. We show that the proposed composition is not independent of the choice of representatives. For every consistent recursively enumerable extension T of Peano arithmetic (PA), we exhibit two unary programs whose partial functions are provably equal in T, separately at each standard input. Composing each after a program that searches for a T-proof of contradiction and returns its code yields programs that are not equivalent in this sense. An alternative proof uses the productivity of the complement of the diagonal halting set. Montagna's S' is the case T=PA. More generally, for consistent T⊇PA, pointwise provable equality is a composition congruence exactly when T proves every true Π01 sentence, in which case it is extensional equality. This completeness condition fails for every consistent recursively enumerable T⊇PA by Gödel's second incompleteness theorem. For every extension T⊇PA, the least composition congruence containing pointwise provable equality is extensional equality if T is Σ01-sound and the universal relation otherwise.
Related
- Quasi-Static Fault-Tolerant Feedback Control of a Quadrotor under Rotor Failure with Provable Safety Guarantees
- HOLES IN PLANAR PARALLEL SETS: AN INTEGRATED BETTI-NUMBER BOUND AND ITS POINTWISE FAILURE
- The failure of stable composition for equivalence relations in simple theories
- Identifying Damage Pathways Linking Sequence Composition to Storage Failure in DNA Data Storage via High-Dimensional Mediation Analysis
- Provable circuit-level thresholds for non-abelian topological phases
BibTeX
@misc{lengyel2026pointwise,
title = {{Pointwise provable equality and the failure of composition}},
author = {Florian Lengyel},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2609.25556},
eprint = {2609.25556},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.25556},
}
RIS
TY - UNPB
TI - Pointwise provable equality and the failure of composition
AU - Florian Lengyel
PY - 2026
DA - 2026/10/01
PB - arXiv
DO - 10.48550/arxiv.2609.25556
UR - https://arxiv.org/abs/2609.25556
AB - In their studies of pathologies in recursion categories, Montagna (1989) and Di Paola--Montagna (1991) introduce the algebraic systems S' and S'_T, respectively, and claim that they are categories. We show that the proposed composition is not independent of the choice of representatives. For every consistent recursively enumerable extension T of Peano arithmetic (PA), we exhibit two unary programs whose partial functions are provably equal in T, separately at each standard input. Composing each after a program that searches for a T-proof of contradiction and returns its code yields programs that are not equivalent in this sense. An alternative proof uses the productivity of the complement of the diagonal halting set. Montagna's S' is the case T=PA. More generally, for consistent T⊇PA, pointwise provable equality is a composition congruence exactly when T proves every true Π^0_1 sentence, in which case it is extensional equality. This completeness condition fails for every consistent recursively enumerable T⊇PA by Gödel's second incompleteness theorem. For every extension T⊇PA, the least composition congruence containing pointwise provable equality is extensional equality if T is Σ^0_1-sound and the universal relation otherwise.
ER -