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^{\prime }$ and $S_T^{\prime }$, 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 ($\mathrm{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^{\prime }$ is the case $T=\mathrm{PA}$. More generally, for consistent $T\supseteq \mathrm{PA}$, pointwise provable equality is a composition congruence exactly when $T$ proves every true ${\Pi }_1^0$ sentence, in which case it is extensional equality. This completeness condition fails for every consistent recursively enumerable $T\supseteq \mathrm{PA}$ by Gödel's second incompleteness theorem. For every extension $T\supseteq \mathrm{PA}$, the least composition congruence containing pointwise provable equality is extensional equality if $T$ is ${\Sigma }_1^0$-sound and the universal relation otherwise.

11 pages. Exposition condensed and discussion of related work revised; mathematical statements and proofs unchanged. Clarified the roles of consistency and ${\Sigma }_1^0$-soundness and the distinction between pointwise provable equality and its generated composition congruence. Results and proofs unchanged. Lean formalization and verification records: https://github.com/flengyel/FailureOfComposition