Pointwise provable equality and the failure of composition
En palabras de los autores
Montagna (1989) and Di Paola--Montagna (1991) claim that the algebraic systems and , respectively, are categories. We show that the proposed composition is not independent of the choice of representatives. For every consistent recursively enumerable extension of Peano arithmetic (), we exhibit two program indices that are pointwise provably equal in but yield inequivalent composites when each is run after the same program. Montagna's is the case . The failure already occurs for partial maps from to itself. Weak totality and the proposed range assignment also depend on the choice of representatives. More generally, for consistent , pointwise provable equality is a composition congruence exactly when proves every true sentence, in which case it is extensional equality. This completeness condition fails for every consistent recursively enumerable by G\"odel's second incompleteness theorem. For every extension , the least composition congruence containing pointwise provable equality is extensional equality if is -sound and the universal relation otherwise.
Apareció: miércoles, 23 de septiembre. arXiv. Preprint, todavía sin revisión por pares.
Comentario de los autores: 11 pages