Constructive Mathematics Is Not Metamathematics を読むだけ
原文:
ChatGPT 4o で翻訳しました。
ホモトピー型理論（Homotopy Type Theory, HoTT）の書籍が出版されたことで、数学の基盤としての型理論への関心が再び高まり、高次元型の計算的意味をコンピュータ科学者が探求するきっかけとなりました。以前の投稿でも述べたように、ホモトピー理論においてHoTTが非常に有効である理由は、それが構成的（constructive）であることにあります。少なくとも、すべての型が決定可能であると仮定していない点が挙げられます。Hedberg の定理によれば、決定可能な同値性を持つ型は集合（ホモトピー 0型）であるため、排中律を全面的に採用すると、高次元構造が直ちに排除されてしまいます。
私の考えでは、排中律の普遍的有効性の否定は構成性（constructivity）の本質的な特徴ではなく、むしろその特徴の一つに過ぎません。それは「煙」であって、「機関車」ではないのです。しかし、それでは、なぜ構成性は排中律をはじめとする多くの古典的な推論パターン（例えば、背理法や命題の真偽による場合分け推論）を否定するのでしょうか。この全容はまだ完全には解明されていませんが、必要条件の一つとして、構成的理論は「証明関連性」（proof relevance）を持つべきだと考えられます。つまり、証明は他の数学的対象と同様に数学的なオブジェクトであり、それが構成的数学の発展において果たす役割は、古典的数学における役割とは異なるものだということです。
証明関連性（proof relevance）の最も明白な現れは、HoTT（ホモトピー型理論）の特徴そのものにあります。それは、同値性の証明が空間内のパスに対応するという点です。パスは、その始点と終点が等しいことの証拠と考えることができます。この等式の概念が優れていることは、型理論の構成物が持つホモトピー不変性からも明らかです。つまり、すべての要素がパスを尊重し（型のグルーポイド構造を尊重するという意味で）、一貫性を保っています。より一般的に、HoTTにおける定理は、命題の証明の空間を特徴づける傾向があり、単に対応する型が存在する（inhabited）ことを述べるにとどまりません。例えば、一価性公理（univalence axiom）自体は、ある宇宙内での型の同値性の証明と、それらの型間の同値性の間に同値関係があることを示します。この種の推論には慣れが必要かもしれませんが、その美しさは私の考えでは否定できないものです。古典的な思考様式は、証明の構造を切り捨てる「切断」（truncation）を明示的に用いることで再現することができます。場合によっては、これが定理を述べる最善または唯一の方法になることもありますが、通常は単に型が存在することや、二つの型が相互に存在し合うこと以上のことを述べる傾向があります。この点で、構成的視点は古典数学を縮減させるどころか、むしろ豊かにしています。この事実を、20世紀最大の数学者の一人であるダフィット・ヒルベルトさえも見落としていたようです。
ホモトピー型理論（HoTT）における証明関連性の概念は、証明の本質に関する非常に一般的な誤解を再燃させたようです。多くの人々は、証明とは公理的理論（たとえば集合論）の中での導出であると考えるように訓練されてきました。この見方は教科書でしばしば推奨され、非形式的な証明もこの形式で完全に書き下すことができるという主張によって支持されています（実際にはそのような手間を省略することがほとんどであったとしても）。そこから「証明は数学的オブジェクトである」という結論に至るのは容易です。これは古典的な集合論でも同様であり、導出を帰納的に定義された集合の要素（例えば有名な自然数の集合）や、より自然な抽象構文表現（1960年にマッカーシーがこの目的のために導入したS式形式など）として扱うことが可能だからです。このような視点から、多くの人がHoTTの特徴として「証明を数学的オブジェクトとみなす」点が強調されることに戸惑い、それがどのように独自性を持つのか疑問を抱くようです。
重要な点は、「証明」と「形式的証明」は同じものではないと認識することです。さらに混乱を避けるために補足すると、ここで「形式的」という言葉で意味するのは「厳密な」という意味ではなく、公理的集合論のような「形式体系で表現された」という意味です。形式的証明とは、公理と形式理論の規則によって生成される、計算可能列挙可能な集合の要素です。一方、証明とは、命題の真実性を示す議論そのものです。形式的証明は常に証明である（少なくとも、基礎となる形式理論が矛盾しないという仮定の下では）一方で、証明が必ずしも形式的証明である必要はなく、形式的証明として表現される必要もありません。この違いの主な例が、ゲーデルの定理です。この定理は、公理的算術における形式的に証明可能な命題の計算可能列挙可能な集合が決定可能ではないことを証明します。その核心となるステップは、自己言及的な命題を考案することです。この命題は、(a) 形式的には証明不可能であるが、(b) その命題が真であることを示す証明を持ちます。この議論の要点は、一度証明の規則を固定すると、その固定された体系内では証明不可能であるが真である事柄を必然的に見逃すという点にあります。
ここからが混乱を招く部分です。HoTTは形式体系として定義されているのに、なぜ同じ議論が適用されないのでしょうか？実際には、ほぼそのまま適用されます！しかし、これはHoTTにおける「証明関連性」には影響を与えません。なぜなら、関連する証明とは、HoTTを形式体系として定義する形式的証明（導出）ではないからです。むしろ、証明は型理論の内部でオブジェクトとして定式化されており、証明の形態がそれだけに限定されるという先入観はありません。例えば、外部から見るとHoTTで定義可能な関数は可算無限個しか存在しないことは簡単に理解できます（HoTTが形式体系によって定義されているためです）。しかし、理論の内部では、無限型上の任意の関数空間には非可算無限個の要素が存在します。この二つの見解には矛盾がありません。なぜなら、含意の証明（内部的な関数）は、形式的導出のコードと同一視されず、したがって可算的ではないからです。
以前このブログでも指摘されたように、ここにはチャーチの法則（Church’s Law）との密接な類似性があります。内部的にチャーチの法則を受け入れることは、関数を定義するために使用するプログラミング言語を事前に固定することに相当します。これにより、例えば、特定のプログラムがその言語では表現不可能であることを示すことができます。しかし、HoTTはチャーチの法則を採用していません。そのため、この種の議論は、例えば「チューリングマシンの停止問題を決定するチューリングマシンは存在しない」と示すことに相当しますが、一方で、そのような決定を行う構成的関数（例えば、オラクルを備えた関数）が存在し得ることを認めています。
形式的証明の理論、一般に証明論（proof theory）と呼ばれる分野は、Kleene によって「メタ数学」と名付けられました。型理論が発展するまでは、証明の研究はメタ数学に限定されていました。しかし、HoTTに体現される構成的数学の新しい世界では、証明（形式的証明に限らず）が数学において重要な位置を占めるようになりました。そして、それによってこれまで曖昧であったり、さらには見落とされていた概念を明確かつ簡潔に表現する新たな可能性が生まれています。
コメント
ああ、ロバート、もちろんあなたもご存じで、実際にそのつもりで言ったのだと思いますが、形式体系の目的の一部は、証明の集合が決定可能であるという点にあります。形式的証明（Formal-Proof）の文法や正当性を判断するのに、機械以上に賢くある必要はありません。むしろ、これは結論を導く操作によるこの集合の本質的な像、つまり、一般には帰納的に列挙可能だが決定可能ではない証明可能な命題の集合を指します。
数学的言語の構成的解釈を理解するためには、そこで関わる証明の概念が形式的推論体系における形式的証明ではないことを認識することが不可欠です。しかし、「ゲーデルの証明は、公理的算術における形式的証明の計算可能列挙集合が決定不可能であることを証明している」と言うのは誤りです。どの形式理論における形式的証明の集合も、決定可能であることは自明です。ゲーデルの不完全性定理が示しているのは、算術的真理の集合が「生成的（productive）」であるということです。
むしろ、証明は型理論の内部でオブジェクトとして定式化されており、証明の形態がそれだけに限定されるという先入観はありません。
確認ですが、ここで言いたいのは、形式的証明が内部的な証明オブジェクトの唯一の形態であるとあらかじめ限定しているわけではない、ということで正しいですか？
「ゲーデルの定理は、公理的算術における形式的証明の計算可能列挙集合が決定不可能であることを証明している」と述べていますが、これは正確ではありません。ゲーデルの第一不完全性定理は算術の無矛盾性を証明するものではないため、算術が矛盾している可能性を排除しません。この場合、形式的証明の集合は自明に決定可能です。
さらに、もし形式体系が矛盾しているなら、すべての命題が証明可能になるのは当然のことですが、その場合にあなたがゲーデルの命題を意図する意味（タルスキ的な意味？）で「真」とみなすかどうかはわかりません。おそらく、そうはならないでしょう。（一方で、体系が無矛盾であると仮定するならば、それまで証明不可能だった新しい真理を発見できるのは驚くことではないかもしれません。）
reply: ちょっと興味があるのですが、どの形式体系が矛盾しているかをどのように決定するのですか？
reply: まあ、一般的には決定することはできません。直観主義的なアプローチでは、計算を基本的な概念として出発点から積み上げていく方法が取られています。私自身は今でもこの方法を信じていますが、HoTTは現時点で計算的な正当性を欠いています。
reply: まあ、この質問は本当はフレデリックに向けたものです。そして私の主張は、算術が「自明に決定可能」である可能性を強調するのは少し不誠実だという点です。なぜなら、1) 誰も算術が矛盾しているとは信じておらず、算術のモデルを知っていると考える人がほとんどであり、2) ゲンツェンは算術の無矛盾性を有限木における特定の順序の整礎性に還元しており、これも同様に信じるに足るものであり、3) ある体系が矛盾していて「自明に決定可能」であるとしても、単にすべての命題に対して「定理」と応答するだけの機械は、そのような決定可能性の証拠にはなりません。ある形式体系で「偽」が導出されることこそが、その証拠となるからです。
reply: 私は、不完全性定理の最も基本的な形、つまり「健全性」を仮定するものを念頭に置いていました（算術の公理は真である。なぜなら、それを一般的に認められた数学的推論を用いて証明できるからです）。これは、できるだけ簡単に私の主張を伝えるためです。この仮定を形式的一貫性に弱めることもできますが、それは私の主な論点から外れます。私の論点は単に、形式的証明の概念と証明の概念を区別することであり、特に、どのような形式的証明の概念も証明の概念を完全に捉えることはできないということです。
これは「古い話」だとは認識していますが、この問題は繰り返し浮上しており、最近ではHoTTの中心概念である「証明関連性を持つ数学」に関連する話題でもありました。そのため、現状を説明しようと試みてみた次第です。
この混乱があるために、HoTTの本では、理論内の「関連する」オブジェクトを指す際に「証明（proof）」という言葉ではなく、「証人（witness）」や「証拠（evidence）」といった言葉を使おうとしているのだと思います。
いいなと思ったら応援しよう！
