Pointwise provable equality fails to ensure compositional consistency in arithmetic-based programs

Pointwise provable equality and the failure of composition

Logic in Computer Science

Summary

The paper finds that when comparing computer programs based on a certain notion of equality proven inside arithmetic, two programs can seem equal piece by piece but behave differently when combined with others. This contradicts earlier claims that these programs form a mathematical structure called a category, which requires composition to be consistent. The authors show this inconsistency occurs even with basic types of partial functions and ties the problem to foundational limits in arithmetic. They also characterize exactly when this type of equality behaves well under composition, linking it to strong forms of truth provability in arithmetic.

What this means in practice

  • For program verification teams: Avoid relying on pointwise provable equality as a basis for program equivalence when verifying program composition correctness in arithmetic-based systems.
  • For formal methods engineers: Design proof systems and program equivalences that respect extensional equality to ensure compositional consistency in software verified over arithmetic theories.

A theory result. No direct application yet.

Authors

Florian Lengyel

Abstract

Montagna (1989) and Di Paola--Montagna (1991) claim that the algebraic systems $S'$ and $S'_T$, respectively, 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 program indices that are pointwise provably equal in $T$ but yield inequivalent composites when each is run after the same program. Montagna's $S'$ is the case $T=\mathrm{PA}$. 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 $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.
View PDFOpen arXiv