点ごとに証明できる等しさではプログラムの合成が定まらない
Pointwise provable equality and the failure of composition
この論文をやさしく読む
ひとことで言うと
プログラムが入力ごとに同じだと証明できても、その後ろに別のプログラムを合成すると同じ結果になるとは限らないことを示した。
何に役立つ？
計算可能性や証明論で、プログラムの同値関係から圏や合成演算を作る際の条件を見直すために役立つ。
この研究の面白いところ
以前に圏と主張された構成に、代表元に依存するという具体的な問題を示し、合成と両立するための条件まで特徴付けた。
どこまで分かった？
主な不可能性は無矛盾で再帰的可算なPAの拡張について述べられる。一般の拡張についての最小合同関係はΣ⁰₁健全性によって場合分けされる。
v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。
アブストラクトの日本語訳
Montagna（1989年）とDi Paola–Montagna（1991年）は、それぞれ代数系S′とS′_Tが圏であると主張した。著者らは、提案された合成が代表元の選び方によらずに定まるわけではないことを示す。Peano算術（PA）の任意の無矛盾な再帰的可算拡張Tについて、Tの中で各入力点ごとには等しいと証明できる2つのプログラム番号を示す。しかし、どちらも同じプログラムの後に実行すると、同値でない合成を生む。MontagnaのS′はT=PAの場合に当たる。この失敗は、自然数集合ωから自身への部分写像でもすでに起こる。弱い全域性と提案された値域の割当ても、代表元の選び方に依存する。 さらに一般に、無矛盾なT⊇PAでは、点ごとに証明できる等しさが合成に関する合同関係になるのは、Tが真であるすべてのΠ⁰₁文を証明するとき、かつそのときに限る。この場合、その等しさは外延的な等しさとなる。Gödelの第二不完全性定理により、この完全性条件は、無矛盾で再帰的可算な任意のT⊇PAでは成り立たない。任意の拡張T⊇PAについて、点ごとに証明できる等しさを含む最小の合成合同関係は、TがΣ⁰₁健全なら外延的な等しさであり、そうでなければ普遍関係である。
v1の要旨から自動生成。本文の精読・人による確認は未実施。
- 初稿
- 2026-09-22（UTC）
- 最新改訂
- 2026-09-22 · v1
- 査読・掲載
- 査読状況未確認
更新履歴
- v1 2026-09-22 この版を読む
取得できた版を表示。版の更新は査読済みを意味しません。過去版の本文差分は未解析です。
原文の要旨
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 $\omega$ 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 $\Pi^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 $\Sigma^0_1$-sound and the universal relation otherwise.
著者のコメント
11 pages
arXiv ID: 2609.25556 ／ 要約の誤りについて