この1ヶ月、日本語の論理学の入門書を1節ずつ読み進めていて、章ごとの証明を小さなHaskellのコードに訳しながら追っている。2000年に出た命題論理・述語論理の教科書が、自分の使ってるツールがなぜ止まったり止まらなかったりするのかの見方を変えるとは思ってなかった。でも第7章あたりで、まさにそれが起きた。

日本語と実際のコードを抜いた形で、その論の骨格だけ書く。

命題論理がタダでくれるもの

命題論理――「かつ」「または」「でない」「ならば」を、それ以上分解しない原子的な文に適用する論理――には、最初は超能力みたいに見えるものが付いてくる。この言語で立てられる問い(「この式はトートロジーか」「この2つの式は同値か」「この論証は前提から妥当に導けるか」)は、全部力技で決着がつく。原子式に真/偽を割り当てるすべての組み合わせを列挙して、各行をチェックすればいい。原子式がn個なら行は2ⁿ通り。表は有限で、手続きは必ず終わり、必ずはっきりした答えが出る。これが決定可能性で、命題論理はそれをタダで持ってる。

なぜこれが可能なのか、少し立ち止まる価値がある。真理表がくれるのは可能性の空間全体を尽くす網羅的な探索で、それが機能するのは空間が有限だからにすぎない。すべてのケースを列挙できる瞬間、テストは証明になる――「テストはバグの存在は示せるが不在は示せない」というダイクストラの有名な言葉と、この教科書が自信満々に見せる2ⁿ行の表は、同じ事実を反対側から言っているだけだと気づくと、対立は消える。ダイクストラの警告は無限の入力空間についての話で、そこではテストスイートは必然的にサンプルでしかない。真理表はサンプルじゃない。全数調査だ。

ただし落とし穴もあって、それも軽くない。この網羅性は、野心の低さから来ている。命題論理は個体について、個体の性質について、個体同士の関係について何も語れない。「誰もが誰かを愛している」も「AからBへの経路がある」も表現できない。その意味論的な内容は全部、原子的な真理値の有限集合から真理値への関数に押し込まれている――つまり書ける式は無限にあっても、n個の原子式が表現しうる本当に異なる意味は2^(2ⁿ)個しかない。構文は無限、意味は有限。このギャップこそが、全数チェックを可能にしている遊びの部分だ。

床が抜ける場所

述語論理は量化子(「すべての」「存在する」)と個体間の関係を足すが、ここでタダのランチは終わる。「すべてのxについて、あるyが存在してR(x,y)」――グラフの到達可能性や経路、関係の連鎖についての主張の根っこにあるこの形――を言える言語になった瞬間、命題論理の有限な意味論的内容は消える。ある個体の他の個体への関係は、真理値割り当てのように有限の表に潰すことができない。

面白いのは、これが定理の主張としてだけでなく手続きとして具体的にどう現れるかだ。教科書は妥当性を検証する証明探索の手続き(タブロー法)を扱っていて、そこには構造的な非対称性が組み込まれている――存在量化子を扱う規則は式1本につき一度発火して終わる。新しい個体を1つ導入して、それで終わり。全称量化子を扱う規則は、証明中のどの個体に対しても、後の手続きで生成された個体を含めて、何度でも再適用できる。命題論理ではこの非対称性は見えない――「個体」はただの真理値で、2ⁿ個しかないから、探索は必ず底を打つ。述語論理では「すべてのxについて、あるyが存在してR(x,y)」のような式が連鎖を引き起こしうる――存在の要求を満たすため個体を導入し、それに全称規則を適用すると新たな存在の要求が出て、また個体を導入し、また全称規則を適用し……終わりが保証されていない。これはProlog のクエリが再帰的な節を満たそうとして永遠に戻ってこないのと構造的にまったく同じで、それは偶然ではない――自動定理証明系はまさにこの種の探索の上に組み立てられている。

これは特定の証明法の欠陥ではない。アロンゾ・チャーチとアラン・チューリングが1936年、それぞれ全く異なる形式的道具を使って(チャーチはラムダ計算、チューリングは今日チューリングマシンと呼ぶもの)独立に証明した何かの症状だ――「この述語論理の式は妥当か」という問いは、すべての入力について必ず停止するアルゴリズムでは答えられない。これがヒルベルトの決定問題(Entscheidungsproblem)で、2つの異なる方向から到達した答えは、どちらもノーだった1。この結果を扱う章のタイトルは、わざと安心させるように「論理学者を責めないで」となっている――要点は、これが賢さの欠如ではないということ。もっと賢い探索手続きではこれを直せない。この限界は、アルゴリズムのクラスにできることについて証明済みの数学的事実であって、まだ試されていないだけのギャップではないからだ。

生き残る非対称性

決定可能性の代わりに手に入るのは半決定可能性だ。式が妥当なら、何らかの探索手続きが最終的にそれを確認して停止することが保証されている。式が妥当でないなら、それを教えてくれることが保証された手続きは存在しない――永遠に走り続けるかもしれないし、長い間証明を見つけられずに走っている探索は、「これは妥当でない」と「証明はまだどこかにある」を区別する手立てをくれない。ゲーデルの完全性定理が「はい」側を保証している――意味論的に妥当な式の集合は帰納的可算だから、候補の証明を体系的に列挙してチェックしていけば、存在するならいつか必ず表面に出てくる2。「いいえ」側を救ってくれる同種の保証はなく、これは見落としじゃない――停止性問題と証明可能な形で等価だ。「このプログラムは停止するか」を「この式は妥当か」としてエンコードできて、その形式は、一般的な妥当性判定器があれば停止性判定もできてしまうことを示す――そしてそれはすでに不可能だと分かっている。

これは打ちのめされるというより、腑に落ちる感覚だった。名前がなかったものに名前がついた。十分に表現力の高い型システム(高階多相・依存型)での型推論はフリーズすることがある。SMTソルバはフリーズすることがある。充足可能性問題に帰着するパッケージのバージョン解決はフリーズすることがある。どの場合も裏に設計判断が隠れている――ツールは停止を保証できるほど小さな論理の断片に留まって表現力を差し出すのか、それとも表現力を取って、実務では答えがタイムアウトになることを受け入れるのか。型システムの設計者は、自動推論やロジックプログラミングの世界より前者を選ぶ傾向が強いように見えるけど、なぜ文化がそう分かれたのか、分野全体で一貫していないのか、僕にはまだ自信を持って言えない。「たまにコンパイルを拒否する型検査器」の方が「たまにビルドをフリーズさせる型検査器」より我慢できる、というだけの話かもしれない。

もうひとつ、教科書がずっと注意深く扱っている点がある――チューリングマシンとラムダ計算がどちらも「計算」という非形式的で理論以前の概念の正しい形式化を捉えている、というチャーチ=チューリングのテーゼが、なぜ定理ではなくテーゼと呼ばれるのか、には本当の理由がある。独立に発明された2つの形式体系が互いに等価だというのは定理で、数学の中で証明できる。この共有された概念が、「何が計算可能か」という曖昧な人間的概念の正しい形式化である、というのは数学で検証できることじゃない。曖昧な人間的概念はそもそも数学的対象だったことがないから。これは世界についての主張で、その後のあらゆる計算の形式化の試み――再帰関数、レジスタ機械、セル・オートマトン――が同じ同値類に着地してきたという事実に支えられているけど、それでも正直に言えば証明というより帰納的な主張のままだ。教科書がこの線をぼかさず引くことにこだわっているのが好きだ。証明済みのものと単に「まだ反証されていない」ものの境界は、確認が積み重なるほど滑りやすくなるまさにその種の区別だから。

未解決の問い

僕がいま抱えているのは、技術的というより実務的な問いだ。ある問題がこういう壁の向こう側にある――難しいだけでなく、本当に決定不能――と分かっているとき、取れる手は2つしかないように見える。決定可能な断片に収まるまで言語を縮めるか、表現力を保ったままヒューリスティック・深さ制限・タイムアウトで非停止のリスクを運用でしのぐか。どちらも正当なエンジニアリングの選択で、異なるコミュニティが、僕が指し示せるような論拠なしに、慣習として逆の賭けをしてきたように見える。ここに唯一の正解があるとは思わないけど――なぜその2つの文化がそう分かれたのかを、分野がたまたまそう育っただけでなく、誰かが実際に形式化したことがあるのか気になっている。

  1. Entscheidungsproblem. Wikipedia. Accessed 2026-08-11. ↩

  2. Gödel’s completeness theorem. Wikipedia. Accessed 2026-08-11. ↩