問い #71

AI調査レポート AIモデル: gpt-6-astra 作成日: 2026-09-08（JST） # 爆発律を保ったまま、証明の違いを残せるか このレポートはAIによる文献調査と検討案です。元投稿の著者による主張ではなく、元の問いの解決判定でもありません。今回は下記の一次資料2件を読み、近い構成・障害・試せる具体例を整理しました。網羅的な先行研究調査ではありません。 ## 先に分けたい二つの問い 「矛盾からどの命題でも導ける」ことと、「同じ前提・結論を持つ証明がすべて同じになる」ことは別です。後者には、どの変形で証明を同一視するかという選択が入ります。不変量を探す際は、証明の等価関係を先に決める必要があります。 ## 近い文献：零証明と線形代数 Došenの *Identity of Proofs Based on Normalization and Generality* §7は、すべての式A、Bの間に「零証明」0 : A → Bを加える案を論じています。証明可能性は自明になりますが、証明同士まで全部同一視するわけではありません。同節では、連言・選言の断片を図式から行列へ表し、証明の合成を行列積、加法を行列の加法で扱う接点が示されています。 これは「何が証明できるか」から「証明の違いにどんな構造が残るか」へ視点を移す、元の問いに近い先行する構想です。ただし、任意の矛盾した公理系にそのまま使える一般解ではありません。 [文献1：Došen、v12、§7・印刷20–21頁（PDFも同じ頁番号）](https://arxiv.org/pdf/math/0208094v12#page=20) ## 同一視を強くしすぎると起きること 同論文§5では、始対象⊥を持つcartesian closed categoryに自然な二重否定除去を加えるなどの条件で、各二対象間の射が高々一つになってしまう結果を扱います。⊥から各対象への射が存在することと、その射が一意であることを区別するのが重要です。爆発律だけから、あらゆる証明の違いが失われると結論してはいけません。 [文献1：§5、特に命題2・印刷18頁](https://arxiv.org/pdf/math/0208094v12#page=18) ## 不変量候補を考える別の入口 Došen–Petrićの *Generality of Proofs and its Brauerian Representation* は、推論規則を変えずに変数をどこまで別々にできるか、という「一般性」を扱います。前提・結論中の変数の出現を結ぶ関係として記録するので、証明の長さとは違う情報を取り出せます。導入部の二つの射影 P∧P → P は、同じ型でもどちらのPを使うかを区別する入口になります。同論文では、こうした関係の圏の表現と、論理の断片での例が調べられています。 [文献2：Došen–Petrić、v7、導入部・印刷2–3頁](https://arxiv.org/pdf/math/0211090v7#page=2) ## 試せる三つの案 ### 正規化の前後で、証明図のサイズを比べる AIによる検討案。 Aの証明からA∧Aを導入し、その左成分Aを取り出す証明を作る。これを元のAの証明へ正規化し、推論の段数が変わることを確かめる。生の図のサイズが、正規化による同値類の不変量とは限らないことを確認する最小例。 文献: https://arxiv.org/pdf/math/0208094v12#page=3 ### 二つの射影P∧P→Pを、依存する前提で区別する 文献からの具体例。 左のPを取り出す証明と右のPを取り出す証明を並べる。長さが同じでも、前提のどちらの出現を使うかは異なる。変数を別々にできる範囲を記録すると、その違いを捉えられるか調べる。 文献: https://arxiv.org/pdf/math/0211090v7#page=2 ### 1×1行列で、零射と恒等射を比べる AIによる説明用の例。 行列[0]と[1]は異なり、合成は行列積で計算できる。零射があることと、すべての射が同じになることの違いを可視化するための例として使う。これだけで論理体系のモデルを構成したとは言わない。 文献: https://arxiv.org/pdf/math/0208094v12#page=21