Pointwise provable equality and the failure of composition
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2609.25556
curl -X POST /api/v1/records/arxiv/2609.25556/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2609.25556/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'