逐点可证相等与复合的失效
Pointwise provable equality and the failure of composition
AI总结：
本文证明Montagna和Di Paola-Montagna提出的代数系统$S'$和$S'_T$并非范畴，因为其复合依赖于代表元选择；逐点可证相等仅在$T$证明所有真$\Pi^0_1$语句时才为复合同余，而该条件由哥德尔第二不完备定理对所有一致递归可枚举扩张失效。
AI中文摘要：
Montagna（1989）和Di Paola--Montagna（1991）声称代数系统$S'$和$S'_T$分别是范畴。我们证明所提出的复合不依赖于代表元的选择。对于皮亚诺算术（$\mathrm{PA}$）的每一个一致的递归可枚举扩张$T$，我们构造两个程序指标，它们在$T$中逐点可证相等，但在同一程序之后分别运行时产生不等价的复合结果。Montagna的$S'$是$T=\mathrm{PA}$的情形。该失效已经发生在从$\omega$到自身的部分映射上。弱完全性和所提出的值域指派也依赖于代表元的选择。更一般地，对于一致的$T\supseteq\mathrm{PA}$，逐点可证相等是复合同余当且仅当$T$证明每个真的$\Pi^0_1$语句，此时它就是外延相等。由哥德尔第二不完备定理，这个完全性条件对每个一致的递归可枚举的$T\supseteq\mathrm{PA}$都不成立。对于每个扩张$T\supseteq\mathrm{PA}$，包含逐点可证相等的最小复合同余是外延相等，如果$T$是$\Sigma^0_1$-可靠的，否则是全域关系。
英文摘要：
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 ($\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'$ 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 $Π^0_1$ 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 $Σ^0_1$-sound and the universal relation otherwise.
