この記事は Mathematical Logic Advent Calendar 2023 - Adventar と Math Advent Calendar 2023 - Adventar の16日目の記事である．より正確にはMathematical Logic Advent Calendar 2023 - Adventarの主催に書くことを強要された記事である．
adventar.org
←昨日 Robustly Isomorphic Models | Mathlog
→明日 空白
adventar.org
←昨日 エブリシング・エブリウェア・オール・アット・ワンス・関数 - 電波通信
→明日 asterisque さん
以前，NHK がヒルベルトプログラム周りを紹介する番組を放送したものの，その内容の大半が誤っていたという大きな事故があった．多くの目に余る間違いに加え，その影響力の大きさを鑑みて，わたしは間違っていた内容を批判・訂正するための記事を書いた．
sokrates7chaos.hatenablog.com
この記事は上記の記事で紹介しきれなかったヒルベルトプログラムの話，特に「有限算術」という概念について説明するための記事である．現代の数理論理学（というか証明論）の源流の一つの話である．歴史の専門家ではない人間が書いているので気楽に読んでね．
はじめに
この記事を読むにあたってご承知おきいただきたいことをいくつか述べる．
まず，わたし自身はヒルベルトの思想の専門家ではないので，もしかすると，誤っている部分や語弊のある部分があるかもしれないことをご承知いただきたい．ある程度信用のできる文献やヒルベルト自身の著作を参照しながらこの記事を書いているが，やはり，専門家に太刀打ちできるほど理解しているわけではないということは自覚している*1．
次に，この記事の内容の大半が「数学の哲学*2」の領域の話ということも承知してほしい．数学徒の中には「哲学」にアレルギーを持つものが多いが，もし読者にその自覚があるのであれば，ここで回れ右をして帰った方が良い．
最後に，普段数学をする際に役に立つような知識が得られるわけではないことも承知してほしい．歴史的な話という側面もかなり大きいので，現代で数学をするうえで何か役に立つものがあるとはわたしには思えない．強いて言えば，哲学っぽいモチベーションで証明論をやっている人々のことがほんの少しよくわかるようになることくらいだろうか．「そういやヒルベルトの有限主義ってどんなものなんだろうなぁ．参考程度に知っておきたいな」くらいのテンションで読むのが良いと思う．
ヒルベルトプログラムとは何か
最初にヒルベルトプログラムの確認をしよう．この節の内容は『【詳細版】 1+1=2 笑えない数学 ～笑わない数学の笑えない間違いの話～ - Sokratesさんの備忘録ないし雑記帳』と重複するところが多いので，先の記事を既読の人は飛ばして読んでも良い．
ヒルベルトプログラムは1922年に（現在知られている形で）宣言された計画で，「数学（の理論）の無矛盾性」を示すためのプログラムであった．詳細には次のようなプログラムである．
- 数学（の理論）で扱われるような言明を表せるくらい十分な記述力を持った「人工的な言語」を作る．この「人工的な言語」の「文」は「論理式」と呼ばれる（数学的言明の形式化）*3．
- 上記の「人工的な言語」において「証明」を定義する．演繹的推論は「推論規則」という「論理式」に対する「機械的な操作（一種の計算）」として定義される．「証明」は「推論規則」による「論理式」の操作の列や図として定義される（証明の形式化）*4．こうしてできた「形式化された数学（の理論）」の証明は「有限算術」において（何らかのコーディングを介して）シミュレーション可能（「有限の立場」で扱うことが可能）であることに注意する．
- 「形式化された数学（の理論）」で証明可能な言明の証明は「有限算術」でシミュレーション可能であり，逆にシミュレーション可能なときのみ「形式化された数学（の理論）」で証明可能であることを示す．（還元プログラム）
- 「有限算術」を用いて，「形式化された数学（の理論）」が無矛盾であることを示す．（無矛盾性プログラム）
さて，ヒルベルトプログラムのかなめ「有限算術（Finitary arithmetic）」が今回の主役である．ヒルベルト自身の説明に曖昧な部分があり，よくわからない部分も多いが，「有限算術」とは「数学に限らず，あらゆる科学的な思考，理解，コミュニケーションにとって必要な」もの（D. Hilbert, "Über das Unendliche." Math. Ann. (1926). p.171）で「有限的な手法で決定できるような（自然数の）算術に関する言明」を扱える（形式的でない有意味な）体系らしい．現在では，「原始帰納的算術（PRA）」と呼ばれる体系が「有限算術」に対応するのではないかとされているが，ヒルベルト（とベルナイス）による数学の基礎についての研究においても「原始帰納的でない」手法が用いられているらしく，この辺りもまだ議論の余地があるらしい．ともかく，こういう基盤（有限の立場）に則って「理論が無矛盾である」ことを示すことができれば，哲学的な論難から「数学の手法」を守ることができると考えていたようだ（Hilbert’s Program (Stanford Encyclopedia of Philosophy)）．
この記事では，有限算術を主に『数学を哲学する』およびその原文 "Thinking About Mathematics: The Philosophy of Mathematics" さらに"Hilbert’s Program (Stanford Encyclopedia of Philosophy)"の記述を参考に説明する*5．
有限算術
この節では有限算術の説明をする．
ヒルベルトは整合的に思考するためには
あらゆる思考に先だって直接経験されるものとして，直観される，一定の論理の外にある具体的な対象が与えられなければならない（Hilbert, D. Über das Unendliche. Math. Ann. 95, 161–190 (1926). p.171）
と考えていた．有限算術はそういった「あらゆる思考に先だって直接経験されるものとして，直観される，一定の論理の外にある具体的な対象」を扱う算術である．
「あらゆる思考に先だって直接経験されるものとして，直観される，一定の論理の外にある具体的な対象」ってなんだ？そんなんホンマにあるんか？というのが率直な感想だが，ヒルベルトおじさんやその支持者のアタマの中ではそういうことになっているらしい．ともかく，そういった対象としてヒルベルトは記号(英：signs/独：Zeichen)をあげている．たとえば，数記号として次のようなものをあげている：
1, 11, 111, 1111, ......
ヒルベルト曰く「各々の数記号は，それが複数の"1"しか含まないという事実によって直観的に認識可能になる」らしい（？！）．これらは「自然数」と同一視され，"\(2\)"やら"\(3\)"やらは "11" や "111" の略記として導入される．\(10^{{10}^{10}}\) を「直観的に認識する」のは辛そうな気がしてしょうがないが，これは単に大きすぎる自然数を想像するのは難しいというだけの話なのかもしれない．ちょうど \(10^{{10}^{10}}\) 本の "1" が並んでいる光景は（なんとなく）想像はできるだろうから，「直観的に認識できる」というのをそういう話だと思えば言いたいことはわからんでもない*6．
当然，数記号だけでは何もできないので，これらに加えてさらに "+", "=", " <", などが導入される．ここで，"+"は「数記号の結合」を意味し，"="は「左右の数記号が同じ長さを持つこと」" <"は「左の数記号が右の数記号の真の部分になっていること」を意味している．これらによって，有限算術の中では "\(2+3\)"（つまり "11111"）や "\(2+3=3+2\)"（つまり "11111は11111と等しい"）などが扱える．当然，偽の言明である "\(1=2\)"（つまり "1は11と等しい"）なども扱えるし，それが偽であることも「直観的に」わかる（ということになっているらしい）．さらに一般性を表現するための文字（英：letter/独：Buchstabe）\(\mathfrak{a}\), \(\mathfrak{b}\), \(\mathfrak{c}\) なども導入される．たとえば，「\(\mathfrak{a}\)+36=36+\(\mathfrak{a}\)」という文によって，「『1+36=36+1』や『100+36=36+100』など\(\mathfrak{a}\)に具体的な数記号を代入したものが真である」と表すことができるようになっている．これによって，他にも「\(\mathfrak{a}\)+\(\mathfrak{b}\)=\(\mathfrak{b}\)+\(\mathfrak{a}\)」のような加法の可換性なども（有限的な定式化で）表現できる（実はこれが後で問題になるが一回おいておく）．
これらの「記号」は「具体的対象(英：Concrete object/独：Konkrete objekt)」と言っているが「物理的なトークン」ではなく「抽象的なタイプ」と受け取られるべきらしい．ここでいうトークンというのは「タイプを具体的に表す物理的対象」を表し，タイプは「時空間に位置を持たない（唯一の）抽象的な対象」を指す．これだけではよくわからないので例を使って説明する*7．
次のような文を考えよう：
にわにはにわにわとりがいる．
この文章には「8文字のひらがなが含まれている」という見方と「13 文字のひらがなが含まれている」という見方がある．前者の見方のひらがなをタイプと言い，後者の見方のひらがなをトークンと言う．タイプは一般に抽象的で唯一なものと言える．それに対して，トークンはインクや黒鉛で書かれていたりやスクリーンに投影された線だったり，場合によっては音声だったりもする具体的（物理的）なものである．
さて，ヒルベルトの「記号」に話を戻そう．「あらゆる思考に先だって直接経験される」のがヒルベルトの「記号」とされている．ということは，この「記号」は時空間に位置を持たない対象と思うしかない．また，" <"を「左の数記号が右の数記号の真の部分になっていること」と言うが，"11 <111"を考えるとき，トークンとして考えると「左の数記号が右の数記号の真の部分になっている」とは言えない．なぜなら，左の数記号（という物理的な対象）は右の数記号（という物理的な対象）は別の位置にあるので，どうやっても，「真の部分」にはなれないからである．以上のようなことから，「具体的対象」と言っているものの「物理的なトークン」ではなく「抽象的なタイプ」として受け取るのが良さそうである．「具体的」と言うと，実際に目の前にあって触れてしまうような印象を受けるが，「（微分可能な関数の具体例として多項式関数をあげるようなときに使われるような意味で，どちらかといえば）具体的」ということならしい．数学徒にはおなじみの用法ですね．
さて，「有限算術」の中ではこのように用意した「記号」を用いて「有限な手続き」で「決定」できることを議論できるような「（形式的でない）体系」である．たとえば，「\(2^{10^{{10}^{10}}}+1\)は素数である」のような言明も（有限な時間）で判定ができるので，「有限算術」の言明として扱える．
ここで注意をしなければならないのが「有界な量化子」という概念である．次の二文を考えてみよう．
(1) \(100\)より大きいが\(10^{{10}^{10}}\)より小さい素数\(p\)が存在する．
(2) \(10^{{10}^{10}}\)より大きい数 で，\(p\)も\(p+2\)も素数であるような\(p\)が存在する．
(1) と (2) にはどちらも「\(p\)が存在する」という存在量化子が含まれている．しかし，これらには決定的な差がある．
(1)は「 \(100\)より大きいが\(10^{{10}^{10}}\)より小さい」範囲に\(p\)が存在するので「有限な手続き」で「決定」できる*8．それに対して，(2) は探索範囲が有限ではないので，そうではない．このとき (1) の量化子は有界な量化子と言い，(2) の量化子は非有界な量化子と言う．ヒルベルトは「(1)は有限的だが，(2) は有限的でない」と見なした．
ここで問題になるのが「\(\mathfrak{a}\)+36=36+\(\mathfrak{a}\)」などの文である．これは非有界な量化子を含むので「有限に」決定できる命題ではない．しかし，ヒルベルトは「代入例が正当な有限的命題」は「有限的」と見なした．
しかし，このような「一般性を表す文字を含む」文の否定についてはよくわからないことを述べている．ヒルベルトによると「\(\mathfrak{a}\)+1=1+\(\mathfrak{a}\)」は
有限の立場では否定するということができない．
（D. Hilbert, "Über das Unendliche." Math. Ann. (1926). p.173）
ので，「\(\mathfrak{a}\)+1\(\neq\)1+\(\mathfrak{a}\)」という文は有限算術において意味を持たないらしい．これは「\(\mathfrak{a}\)+1\(\neq\)1+\(\mathfrak{a}\)をすべての自然数について試すことはできない」かららしい．同様の理由で，「無限の論理的結合子」なども意味を持たない．
このように，一般性を表す文字を含む文については「何が正当で何が意味を持たないか」をヒルベルトはしっかり述べてくれていない．とりあえず，現在では有限算術は「原始帰納的算術（英：Primirive recursive arithmetic/PRA）」と同一視して扱われることが多い．が，それに対する反対意見もあるようで，結局，何を指しているのかについてはまだ議論があるようだ（数学を哲学する）．実際問題，ヒルベルトやその盟友であるベルナイスも PRA では扱えない手法を1923年の時点で用いているらしい（Hilbert’s Program (Stanford Encyclopedia of Philosophy)）．
有限算術の説明において決定的に大事なこととして，すくなくとも有限算術では「（何らかの）形式的体系Tの無矛盾性を表す言明」は扱えることは想定されていた．つまり，
\(\mathfrak{a}\) は，矛盾（0\(\neq\)0）の T における（形式的）証明ではない．
は「有限的」な意味のある言明と思われていたようだ．ただ，形式的体系の証明を有限算術内でどう扱うかについてはヒルベルト自身ははっきりとは言っていない．ゲーデルコーディングみたいなものを想定していたのだろうか……？
総括
結局「有限算術」って何かって？わたしにはよくわからん．ヒルベルトおじさんの頭の中にあった「なにか」らしいが，とりあえず，はっきりしていることは次の通り：
- 形式的体系ではなく，有意味である
- あらゆる思考に先だって直接経験されるものとして，直観される，一定の論理の外にある具体的な対象（記号）を扱っている
- ある程度の算術を扱える
- 有限的に決定できる言明のみ扱える
- 一般性を表す「文字」を含む正当性がなぜ言えるのかはよくわからない
- 現在は Primirive recursive arithmetic と扱われることが多いが，もう少し強くしても良いとする研究者も多い．
- （ある程度の）形式的体系の無矛盾性は扱える
この記事で書いた以外にも「有限の立場」については他にも認識論的なイシューなどもあるらしい．が，これ以上詳しいことは現時点のわたしの手には余るので，詳しく知りたければ以下の参考文献などに目を通してほしい．何かわかったら追記するかも知れない．
参考文献
有限算術の説明は主に『数学を哲学する』およびその原文 "Thinking About Mathematics: The Philosophy of Mathematics" さらに"Hilbert’s Program (Stanford Encyclopedia of Philosophy)"の記述を参考にした．ちなみに，"Hilbert’s Program (Stanford Encyclopedia of Philosophy)"だと「有限算術」を"finite reasoning"と言っている．
全部は読めてないのだが，Zach, Richard. “Hilbert's program then and now.” arXiv: Logic (2005): 411-447. や Detlefsen, Michael. "Hilbert’s Program: An Essay on Mathematical Instrumentalism." Dordrecht and Boston: Reidel. (1986) なども詳しいらしい．
*1:ただし，林晋氏の著作におけるヒルベルト思想についての記述や歴史著述については意図的に無視して書いている．というのは，林晋氏の手によるヒルベルト解説に疑義が生じているためである．その理由は，1. 林晋氏の著述の小さくない部分が他の人間の手による説明から大きく離れていること，2. 史料に書いていないことを「読み取ってしまっている」林晋氏の手による文章を発見してしまったから，である．そのような理由から日本における林晋氏の立ち位置を承知しつつも氏の説明などは無視して書いている．この立場は，『【詳細版】 1+1=2 笑えない数学 ～笑わない数学の笑えない間違いの話～ - Sokratesさんの備忘録ないし雑記帳』でも変わらない．ちなみに，仮に林晋氏の意見を採用しても「1+1=2 笑わない数学」は誤っている部分だらけだったので，上記の記事の大意に変更はない．
*2:もしかしたら，ふざけているように見えるかもしれないが，これが正式名称の分野である．一般に「○○の哲学」（○○は学術分野の名前）とは，○○という分野に関わる哲学のイシューを研究する分野である．「個別科学の哲学」と総称されることが多いが，○○に普通「科学」として扱われない分野も入ることを鑑みると「個別学問領域の哲学」などと呼んだ方が良いように思う．この説明，このブログだとおなじみだと思うし，そろそろさぼっていいかな．（2023/12/23 追記）汎用注釈作った：【汎用注釈】〇〇の哲学 - Sokratesさんの備忘録ないし雑記帳．（追記終わり）
*3:公理化とは異なる．また，たまに数理論理学系の人間でも勘違いしていることがあるが，何かが厳密になっているわけでもない．
*4:これも公理化とは異なるし，また何かが厳密になっているわけでもない．
*5:ドイツ語で書かれた D. Hilbert, "Über das Unendliche." Math. Ann. (1926). などを短時間で読むのは流石に無理だった．
*6:正直，やっぱりよくわからんが，ここは飲み込んで次に進もう．このあたりは認識論的なイシューのような気がするが，そもそも「直観ってなんだ」は未だに永遠と喧々諤々やっておるわけで，ここでは立ち入りたくない．
*7:ここに書いてある以上のことが知りたければTypes and Tokens (Stanford Encyclopedia of Philosophy)を見よ．
*8:より現代的な言い方をすると「(1) の文の真偽を計算するアルゴリズムが存在する」ということである．
