本ページでは、権が専攻しているProof Complexityがどんな分野であるかを、数学的技術細部に立ち入らず、アイディアのみを示す形で ご説明いたします。

  まず、Proof Complexityは、数理論理学の一分野 です。そこで、数理論理学をざっくりご紹介するところから始めたいと思います。

  ここで、釈迦に説法で恐縮なのですが、学問の定義付けは、論者の哲学観が如実に反映され、十人十色になり得ます（数学には、ほぼ明確に「正しい議論」「正しくない議論」を選り分ける基準がありますが、数学の一分野の定義付けそのものについては、そのような基準は全くないように思います）。ですから、このページで述べられていることはあくまで権の私見・権のまとめ方に過ぎません。どうか、教材・文献案内でご紹介している文献なども読者ご自身でチェックの上、常に批判的に読んでいただけましたら幸いです。

  このサイトにいらした方が新たに辿り着いた学問観に触れる日を、権は楽しみにしております

  数理論理学（あるいは数学基礎論）とは、数学の一分野であって、「数学そのもの」を研究対象とする分野です。すなわち、

「数学（あるいは、敢えて広く言い換えるならば、我々の論理的思考）に何ができて何ができないのか」

を、数学的手法で 研究するのです。

  もう少し具体的に、アプローチを述べます。まず、数学では、調べる対象が与えられたとき、それの"数理モデル"を構築 します。

  中学生で学ぶ平面幾何を思い出してみます。この分野では、平面図形、具体的には、日常目にする

図形の位置・定規で引ける線・コンパスで描ける丸 など

を調べるために、これらの"数理モデル"にあたる

点・直線・円 など

の概念を規定（ユークリッドの公理系によって）し、その振る舞いを論じるわけでした。

  同様に、数理論理学では、考える対象である「数学そのもの」の"数理モデル" をまず立てます。

  どうすればよいか考えてみましょう。素朴に我々の日常的な数学的営みを観察すると、これは自然言語（e.g. 日本語、英語 etc.）で行われています。そこで、

「数学を展開するのに必要十分な表現力を持った人工言語を定式化 すれば、"数理モデル"を与えたことになるのではないか」

と考えるのは自然でしょう。

  ここで、自然言語処理や言語学に取り組まれたことのある方はすぐに

「それって現実的ではないのでは？」

と思われるかもしれません。我々の自然言語を包括的に扱える言語モデルの構築 は、人類の悲願の一つと言っても過言ではなく、それは未だ道半ばと言わざるを得ませんから。

  しかし、幸いなことに、「数学を展開できさえすればよい」ということに着目すると、実は今回のケースでは妥当な人工言語を定式化することができます（重要な観察としては、例えば数学を展開するにあたっては、時制や様相は必ずしも必要でない、ということが挙げられると思います）！

  そしてこの人工言語によって記述される

「（数学的）主張」、「（数学的）理論」、「（数学的）証明」、「（数学的）計算」etc.

といった概念も定式化でき*、これらの性質を調べるのが、数理論理学だと言えます。

*上記の概念のどれを分析するかに応じて、人工言語を取り替えることもよくあります。特に、「（数学的）計算」の定式化は、例えば後述する一階述語論理や命題論理といった人工言語からは独立に定義されることが殆ど です（しかし、「計算」を定式化するための人工言語を何らかの形で用意することは間違いありません）。

  では具体的にはどのような"数理モデル"があるのでしょうか？ここでは

一階述語論理、命題論理

の二つを挙げます。どちらも数理論理学全体で大変メジャーな人工言語です。

 ・一階述語論理は、

「証明は、一文が連なってできている。

   一文は、より小さな一文が接続詞（論理結合子）や量化（「任意の」、「存在する」などです）で結ばれてできている。

   接続詞や量化に従って一文を分解していくと、やがてそれ以上分解できない極小な文（atomic formulaと呼びます）に辿り着く。

   Atomic formulaは、いくつかの『名詞』（主語や目的語を想定しています）が『とある関係を満たす』（述語を想定しています）という形をしている」

という風に自然言語を分析して、得られる人工言語です。

  自然言語全体の"数理モデル"を立てようと思ったらこんなに"単純"にはいかないわけですが、

「数学を展開するのに必要十分な表現力を持った人工言語」

を作る分には、実はこれだけで事足りてしまうのです。実際、一階述語論理を用いると、現代数学を（例えば集合論の公理系ZFCないしその亜種を書き下すことで）問題なく記述できることが経験的にわかっています。

 ・命題論理は、一階述語論理よりも"大雑把な"自然言語の近似と見なすことができます。より具体的には、

「一文の内容には立ち入らず、文と文の論理的結合関係のみに着目する」

"数理モデル"です。つまり、上の一階述語論理のアイディアにおいて、「量化」や「Atomic formulaの構造」を捨象して得られるのが、命題論理です。

  当然、一階述語論理と比べて（少なくとも見かけの）表現力は格段に落ちますから、命題論理自体を「数学そのもの」の"数理モデル"と見なすことには無理があります。

  しかし、命題論理もまた、数理論理学を究める上で必須と言ってよい 人工言語です。

  理由の一つは、一階述語論理を分析する上での補助線としての価値 です。より複雑な言語体系である一階述語論理を調べるにあたって、まずはより単純な命題論理から知見を積み重ねる、ということですね。

  しかし、命題論理の重要性はそれだけではありません。実は命題論理は、有限的な数学的構造（例えば有限グラフだったり、それこそ「人工言語そのもの」であったり）の性質を豊かに表現できる ことがわかっています（これを理解するにあたっては、例えば接続詞「かつ」が、量化子「任意のxについて」の「x」の変域を有限集合に制限したものだとみなせる、といった観察が重要です）。従って、有限的な数学的構造を操作していく「（数学的）計算」を考察するにあたって極めて有用な道具立てとなり、それゆえに数理論理学でも最重要な概念の一つなのです。

  これで準備ができました。Proof Complexityの説明に入っていきましょう。

  まず、Proof Complexityとは、端的に言えば、

「数理論理学の中でも、数学的証明の複雑さを解析する分野」

です。

  もう少し掘り下げてみましょう。まず、Proof Complexityの研究対象は「数学的証明」の「複雑さ」です。

 「数学的証明」の"数理モデル"の与え方は上で述べました。繰り返すと、人工言語を定式化し、その後、その人工言語で記述される「数学的証明」を定式化する という流れでした。

  一般には様々な人工言語が考えられ、さらに各々の人工言語に対して多様な「数学的証明」の"数理モデル"（一つ一つの「数学的証明」の"数理モデル"のことを証明系 と呼びます）がありえて、その一つ一つに対して、対応するProof Complexityを議論しえます。

  その上でですが、現在この分野では、人工言語として専ら

一階述語論理、命題論理

が考察されています。ただし、黎明期は古典論理（ぼく達が中高で学ぶ数学で用いる"普通の論理"のことだと思ってください）が研究対象になっていましたが、昨今は非古典論理（人工言語の体系に、「必ずしも必要でない」と先述した様相の表現能力を付け加えたり、人工言語に文法と意味を与える際、「『αではない』わけではない」と「αが成り立つ」を、必ずしも等価であると考えないことにしたり・・・といった形で定義されるものたちです）のproof complexityも盛んに研究 されています。

  では証明系としては何が考えられているかというと、一階述語論理に関してはシーケント計算と呼ばれる証明系、あるいはそれと（証明を互いに"容易に"変換し合えるという意味で）等価な証明系たちを考えるのがメジャーです。これらは概して、

「数学的証明とは、

文（数学的主張）を並べた列 であって、

公理として指定されている文から始まっており、

そこまでで並べた文いくつかから、合法とされている論理法則を適用して（例えば、「AならばB」と「A」が示されたなら、「B」を結論してよい、など）新たな文を得て、列の末尾に付け加えていく

形で構成されるものである」

という分析に基づいて、数学的証明を定式化しています（この列の最後の文が、その証明の「結論」というわけですね）。数学的証明の"数理モデル"として大変自然であり、我々の日常的な数学的営みの解析につながっていくと考えられます。

  一方で、命題論理に関しては、証明系として（命題論理版の）シーケント計算ももちろん考えられます（し、やはり自然な証明系なので、実際とても重要です）が、実はこれ以外にも様々な証明系が考察されています。

  というのも、命題論理のproof complexityにおいては、次の問題が非常に重要だからです：

「どんな（命題論理で記述される）正しい主張も"短く"証明できる（夢のような）証明系は存在するか？」

「ありとあらゆる証明系たち」をいっぺんに考える問いの形をしていますね。「正しい」、「短い」、（この文脈での）「証明系」といった概念の正確な意味はここでは触れませんが、この問いは、適切な定式化のもとで、計算複雑性理論（計算問題の"難しさ"を分類する分野です）における「NP 対 coNP問題」と等価 なことが知られています。

  これは、有名な未解決問題「P 対 NP問題」と極めて深い関係にある（例えば、仮に上の問いの答えが「存在しない」であれば、「P≠NP」が結論されます）重要な問いであり、同時に難題です（未解決です）。そこで、

「とりあえず具体的に定式化できる証明系を列挙して、それらが（先述した）"夢のような"証明系になっているかどうかを判定していこう」

という試みがずっとなされてきました。こういったわけで、命題論理のproof complexityの世界では、多様な証明系が考察されてきたのです。

  さて、では「数学的証明」の「複雑さ」とはどのような量でしょうか？これは、実際には様々な量が考察の対象となっています。

  まず重要なのは、「長さ」です。これは、数学的証明を紙に書くときに必要になる記号の総数（あるいは紙の枚数 ）の"数理モデル"です。シーケント計算のみならず、命題論理のproof complexityで扱うような一般の「証明系」に対しても定義され、proof complexityにおいて中心的な役割を担います（例えば上で正確な意味を述べなかった"短い"という条件も、この「長さ」の概念を用いて定式化します）。

  他にも、考察する証明系に依存して、「複雑さ」の指標となる興味深い量が現れてきます。ここでは、シーケント計算に関連する量を二つだけ挙げます：

・「ステップ数」：これは、我々が日常的に数学的証明を実行する際、必要になる推論の回数（証明に含まれる文の個数 といっても構いません）の"数理モデル"です。

・「記憶領域」：普段、我々が数学的証明を実行する際、そこまでに証明してきた事柄の全てを憶えている必要はありませんよね。例えば、重要な定理を示すために補題を3つ証明したなら、その補題の証明自体はもう忘れてしまって、当該の３つの補題だけ憶えておくだけで、目的となる定理の証明の残りを片付けることができる・・・そういう状況は多々あるわけです。あるいは、黒板に 証明を書きつけていく際に、スペースの関係で、後で使う補題だけを残して他を消して、消したところに新たに 証明を書き加えていく、そういったプロセスを想像していただいても構いません。ここで述べた「記憶領域」とは、こうした状況で、証明を遂行しきるために必要な記憶の量（黒板の広さ）の"数理モデル"です。

  などがメジャーです。

  こうした「複雑さ」の指標となる量を、与えられた数学的主張や理論ごとに不等式評価していく（例えば、「理論Tから定理αを証明するには、最低でも長さがC以上必要である」といった類の主張を得ていく）のが、Proof Complexityという分野です。

  本ページでは、数理論理学 & Proof Complexityの歴史的背景、他分野との関わりについて、敢えて述べていません。議論の分岐を減らして話を見通しよくするためです。

  しかし、学問を理解する上で、上記の二点はもちろん極めて重要 であると考えます。これらについて学ばれたい方は、教材-一般教養-の「数学関連」の項目をぜひご一読ください；

数理論理学の興りとなった「数学の危機」、

不完全性定理の発見、

さらにそれを積極的に利用することで明らかとなる（理論の拡大とそれに伴う）証明の長さの短縮、

そこから始まる一階述語論理のproof complexityの探求、

計算複雑性理論を探る中で示された「命題論理のproof complexity」と「P対NP問題」との密接な関係

・・・ドラマの連続です！