ゲンツェンは何をした人？業績・生涯・名言をわかりやすく｜自然演繹・シークエント計算・無矛盾性証明

ゲンツェンは何をした人？業績・生涯・名言をわかりやすく｜自然演繹・シークエント計算・無矛盾性証明

有名な数学者一覧 › 20世紀 › ドイツ

大学受験

ゲンツェンGerhard Gentzen

ひとことで言うと

「証明」そのものを数学の研究対象にした論理学者。自然演繹・シークエント計算・カット除去定理を作り、1936年に算術の無矛盾性を証明した。

名前ゲルハルト・ゲンツェン（Gerhard Gentzen）
生没年1909年11月24日〜1945年8月4日（35歳）
国ドイツ（グライフスヴァルト生まれ、プラハで死去）
分野数学基礎論・証明論・論理学
主な業績自然演繹、シークエント計算（LK・LJ）、カット除去定理、ペアノ算術の無矛盾性の証明（1936年）
名前がつくものゲンツェンの無矛盾性証明・ゲンツェン流のシークエント計算・ゲーデル・ゲンツェン翻訳
よばれ方証明論の創始者。ヒルベルトの学派の最後の世代の論理学者

このページのポイント

  • 人が考えるとおりの証明の形式「自然演繹」と、証明を式の並びで調べる「シークエント計算」を作った
  • カット除去定理で、どんな証明も回り道のない形に作りかえられることを示した
  • 1936年、ε₀までの超限帰納法でペアノ算術の無矛盾性を証明。算術の「強さ」をはかる順序数解析のもとになった

ゲンツェンは何をした人？（業績をひとことで）

ゲルハルト・ゲンツェン（1909〜1945年）は、ドイツの数学者・論理学者です。ひとことで言えば、「証明」という作業そのものを、数学の研究の対象にした人です。35歳で亡くなりましたが、残した仕事は今の論理学とコンピュータ科学の土台になっています。

代表的な業績は3つあります。1つ目は、人が数学で自然に行う考え方に近い証明の形式「自然演繹」を作ったこと。2つ目は、証明を「式の並び」として調べる道具「シークエント計算」（LK・LJ）を作り、その基本定理「カット除去定理」（ハウプトザッツ）を証明したこと。3つ目は、1936年に、ペアノ算術（自然数の足し算・かけ算の理論）に矛盾がないことを証明したことです。

3つ目の業績は、ゲーデルの不完全性定理と一緒に語られます。1931年にゲーデルは、「十分に強い体系は、自分で自分の無矛盾性を証明できない」ことを示しました。ゲンツェンは、「算術より少し強い道具」を使えば、算術の無矛盾性が確かめられることを示したのです。くわしい経緯は、ヒルベルトの第2問題（算術の無矛盾性）の記事にもまとめてあります。

ゲンツェンの名前は、高校までの教科書には出てきません。でも、命題とは、背理法とは、数学的帰納法といった「証明のしかた」は、ゲンツェンが研究した対象そのものです。この記事では、図と身近な例で、ゲンツェンの仕事をやさしく説明します。

うかるくん

うかるくん

数学の「証明」を研究するって、どういうことですか？ 証明は、数学をするためのものですよね。

合格先生

合格先生

ふつうはそうだね。でもゲンツェンは、証明そのものを、図形や数のように「ながめる」対象にしたんだ。証明にも形があって、長いものや短いもの、回り道のあるものがある。その形を調べると、「数学は矛盾しないか」という大きな問いにも答えが見えてくるんだよ。

ゲンツェンの生涯と年表

グライフスヴァルトに生まれ、島で育つ

ゲンツェンは1909年11月24日、ドイツ北部のバルト海に近い町グライフスヴァルトで生まれました。父はリューゲン島のベルゲンで弁護士をしていましたが、第一次世界大戦で戦死したと伝えられています。1920年に母親とともに、近くの町シュトラールズントへ移りました。シュトラールズントの人文系ギムナジウム（大学へ進む生徒のための中等学校）に通い、1928年には学校で1番の成績で卒業資格（アビトゥーア）を得ました。

ゲッティンゲンへ：ヒルベルトの学派の中で

1928年にグライフスヴァルト大学で学び始め、1929年4月に、数学の中心地ゲッティンゲン大学へ移りました。ミュンヘン大学とベルリン大学でも1学期ずつ学び、またゲッティンゲンへ戻っています。ここでは、ヒルベルト（数学の基礎づけをめざした大数学者）、ワイル（数学と物理の大家）のほか、ランダウ、クーラント、カラテオドリといった、そうそうたる先生たちに学びました。ネーター（現代代数学の母）も、同じころのゲッティンゲンにいた数学者です。

数学の基礎については、ヒルベルトの弟子で論理学者のパウル・ベルナイスから強く影響を受けました。1933年にゲッティンゲンで博士号を受けています。博士論文の指導教員の名前はワイルになっていますが、これはベルナイスが1933年4月に大学を追われたためだと説明されることが多いです。ベルナイスはユダヤ系の家系だとして、ナチス政権の法律で職を失ったのです。ゲンツェンは、第二次世界大戦が始まるまで、ベルナイスと連絡を取り続けたと伝えられています。

1930年代：自然演繹とシークエント計算

1930年代の前半、ゲンツェンは論文「論理的推論の研究」（1934〜35年）で、自然演繹とシークエント計算、そしてカット除去定理を発表しました。自然演繹の形は、すでに1932年9月ごろにまとまっていたとされます。同じころ、ポーランドのヤシコフスキも、よく似た形式を別々に考えていました。

この間、ゲンツェンは1930年代の半ばから1939年まで、ヒルベルトの助手を務めました（資料により、始まりの年は1934年とも1935年ともされます）。算術の無矛盾性の最初の証明は1934年末に完成し、その後、何度か書き直されました。1935年には、ベルナイスとゲーデルから内容について指摘を受けたとされます。最終的に、1936年の論文として『数学年報（Mathematische Annalen）』に載りました。

戦争の時代：兵役、そしてプラハ

1939年の秋に、ゲンツェンは軍の通信関係の仕事に就くことになりました。1941年ごろまで兵役につき、その後、体調をくずしてゲッティンゲンへ戻ったと伝えられています。1942年のはじめには、心の病で苦しんだとされます。その後、解析学の研究を再開し、大学教員の資格論文を提出しました。1943年には、占領下のプラハにあったドイツ大学（シャルル・フェルディナント大学のドイツ側の大学）の講師になります。

1945年：プラハでの最期

1945年5月5日、プラハ市民が占領軍に対して立ち上がった日に、ゲンツェンはほかの大学の教員たちとともに拘束されました。その後、収容所に入れられ、1945年8月4日、約3か月の拘束のあとに、栄養失調（飢え）のため亡くなりました。35歳でした。収容所がどの国の管理下にあったかについては、資料によって書き方がちがいます。墓は、プラハのダーブリツェ墓地の無名の墓だろうといわれますが、はっきりとは分かっていません。

ゲンツェンの歩み1909生まれる（グライフスヴァルト）1929ゲッティンゲン大学へ1933博士号を受ける1935自然演繹・シークエント計算1936算術の無矛盾性の証明1943プラハのドイツ大学で講師に19458月4日、プラハで亡くなる
ゲンツェンの歩み。1909年に生まれ、1936年に算術の無矛盾性を証明し、1945年8月にプラハで亡くなるまで
年できごと
1909年11月24日、ドイツのグライフスヴァルトで生まれる
1920年母とともにシュトラールズントへ。ギムナジウムに通う
1928年学校で首席の成績で卒業資格を得て、グライフスヴァルト大学へ
1929年4月、ゲッティンゲン大学へ移る。ヒルベルトの学派の中で学ぶ
1932年このころ（9月ごろとされる）、自然演繹の形がまとまる
1933年ゲッティンゲン大学で博士号を受ける。ゲーデル・ゲンツェン翻訳の研究もこのころ
1934〜35年論文「論理的推論の研究」で自然演繹・シークエント計算・カット除去定理を発表
1936年ペアノ算術の無矛盾性を、ε₀までの超限帰納法で証明（『数学年報』）
1938年無矛盾性の証明の新しい形を『論理学研究』に発表
1939年ヒルベルトの助手の仕事を終える。秋、兵役につく
1943年プラハのドイツ大学の講師になる。ε₀までの帰納法が算術で証明できないことを示した論文が出る
1945年5月5日にプラハで拘束され、8月4日、飢えのため亡くなる（35歳）

ゲンツェンの主な業績をやさしく解説

業績1　自然演繹：人が考えるとおりの証明の形

ゲンツェンの時代、論理学の証明は、公理（出発点のきまり）をたくさん並べて、少ない推論の規則でつなぐ形が主流でした。フレーゲやラッセルの体系がそうです。しかし、この形式は、実際に数学者が頭の中で行う証明とは、かなりちがって見えます。

ゲンツェンは、「実際の推論にできるだけ近い形式を作りたい」と考えたと、論文の序文で述べています。それが自然演繹です。自然演繹では、公理はほとんど使わず、「仮定を置く」「仮定を閉じる」という操作と、「かつ」「または」「ならば」「すべての」「ある」ごとの導入の規則と除去の規則を使います。

私はまず、実際の推論にできるだけ近い形式を作りたいと思った。

ゲンツェン（論文の序文の趣旨）（「論理的推論の研究」（1935年）。言いまわしは要約です）

たとえば「A かつ B ならば、B かつ A」を示してみましょう。まず「A かつ B」が成り立つと仮定します。そこから B と A を取り出し（かつの除去）、2つを合わせて「B かつ A」を作り（かつの導入）ます。最後に、最初の仮定を閉じると、「A かつ B ならば B かつ A」になります（ならばの導入）。

自然演繹：「A∧B ならば B∧A」 A∧B（仮定①）A∧B（仮定①） ∧を分ける∧を分ける BA B∧A（∧を作る） A∧B ならば B∧A（仮定①を閉じる）
AかつBを仮定し、BとAを取り出して合わせ、最後に仮定を閉じて、AかつBならばBかつAを示す

この「仮定を置いて、結論が出たら、仮定を閉じて「ならば」にする」という流れは、数学的帰納法の書き方や、背理法の考え方（「Aでないと仮定して矛盾が出たら、Aである」）と同じ形です。高校の数学の証明は、実は自然演繹にとても近いのです。

業績2　シークエント計算（LK・LJ）：証明を「式の並び」で調べる

自然演繹は人にはなじみやすいのですが、証明の性質を調べるには少し扱いにくいところがありました。そこでゲンツェンは、証明をべつの形で書き直す道具、シークエント計算を作りました。

基本の単位は、シークエントという式の並びです。「A, B ⇒ C, D」と書き、「左のA、Bがぜんぶ成り立つなら、右のC、Dのどれかが成り立つ」という意味をもたせます。証明は、いくつものシークエントを、規則でつないだ「木」の形になります。

シークエント（式の並び） A, B ⇒ C, D 左の式がぜんぶ成り立つなら、右の式のどれかが成り立つ、という意味 LK（古典論理）右側にいくつでも置いてよい排中律が使える LJ（直観主義論理）右側は1つまで（空でもよい）排中律は使えない Kは「古典的」、Jは「直観主義的」を表すドイツ語の頭文字
シークエントA,B⇒C,Dは、左がすべて成り立つなら右のどれかが成り立つという意味。LKは右側に式をいくつでも置け、LJは1つまで

ゲンツェンは、ふつうの数学で使う古典論理の体系を LK、ブラウワーらの直観主義論理（「Aでない、でないならA」という考えを認めない論理）の体系を LJ と名づけました。この2つのちがいは、右側の式の数を制限するだけという、とても美しい形でまとめられています。左右の対称性が、ド・モルガンの法則のような「かつ」と「または」の対応を、見えやすくしています。

業績3　カット除去定理（ハウプトザッツ）：回り道のない証明がある

シークエント計算の中心にある定理が、カット除去定理です。ゲンツェン自身は「基本定理（Hauptsatz、ハウプトザッツ）」とよびました。

証明の途中で、「まず補題Aを証明して、それをあとで使う」という形を考えます。シークエント計算では、この操作を「カット」という規則で表します。カットを使うと、結論に出てこない別の式Aが証明の途中に現れます。補題を使う証明は短く書けますが、中身が追いにくくなります。

カット除去定理は、「カットを使って示せる文は、カットを使わなくても示せる」という主張です。つまり、どんな証明も、回り道のない形に作りかえられます。

カット除去（ハウプトザッツ） カットありカットなし 補題 A を証明する A を使う（カット） 結論 部品だけで直接 結論 つくり直す 途中で別の式 A が出る結論に出る式の部分だけ この性質を「部分論理式性質」という
左は途中で別の式Aを証明して使う、回り道のあるカットありの証明。右は結論に出る式の部分だけで直接つくる、カットなしの証明

カットなしの証明には、部分論理式性質があります。証明の途中に出てくる式は、すべて結論に出てくる式の「部分」になっているのです。この性質のおかげで、次のことが分かります。

  • 証明を探すときに、出てくる式の範囲が限られるので、探しやすくなる（命題論理が「決定できる」ことも、ここから導かれます）。
  • 「0 = 1」のような矛盾した式は、結論に出てくる式の部分だけでは証明できない。そのため、論理そのものが無矛盾だと示せる。

この「証明を整理して、回り道をなくす」という考え方は、のちのプログラムの計算と深くつながりました。20世紀の後半に、証明の簡単化がプログラムの実行に対応することが分かったのです（カリー・ハワード対応といいます）。ゲンツェンは、コンピュータ科学の土台にもなる考えを、1930年代に作っていたことになります。

業績4　1936年：算術の無矛盾性の証明

ゲンツェンの名前を最も有名にしたのが、ペアノ算術の無矛盾性の証明です。ペアノの公理の公理にもとづく算術は、0、次の数、足し算、かけ算、そして数学的帰納法を使える体系です。これに矛盾がないことを、ゲンツェンは証明しました。

ゲーデルの第二不完全性定理（1931年）は、「体系は自分自身の無矛盾性を証明できない」と言うので、ゲンツェンの証明は算術の外にある、もう少し強い原理を使います。その原理が、ε₀（イプシロン・ゼロ）までの超限帰納法です。

考え方の筋道は、次のとおりです。

  1. もし算術から矛盾が証明できたとしたら、その証明の木があるはずです。
  2. カット除去と同じように、証明の木を少しずつ簡単な形に作りかえる手順を考えます。
  3. 証明の木ごとに、「順序数」という番号をつけます。手順を1回行うたびに、この番号が必ず小さくなるように、番号のつけ方を工夫します。
  4. 番号は ε₀ より小さい順序数ですから、小さくなり続ける番号はいつか必ず 0 に着いて止まります。手順の終わりでは、矛盾を表す「0 = 1」が、かんたんな証明になってしまいます。ところが、それはありえません。
  5. だから、矛盾を導く証明は最初から存在しない、というわけです。
手順1回ごとに、番号は小さくなる ω²ω×3＋2ω×3＋1ω×3ω×2＋1000…ω＋5ω100…10（止まる） どんな順番で小さくしてもいつか必ず有限回で止まる（ε₀より小さい番号）
手順を1回行うたびに、順序数の番号が小さくなる。オメガの2乗から始まり、どんな順番で下がっても有限回で0に着いて止まる

順序数は、自然数 0, 1, 2, … を全部数え終わったあとの「次の数」ω（オメガ）から先へ、数え方を伸ばしたものです。カントールが集合論の中で作りました。ω、ω+1、…、ω×2、…、ω²、…、さらに ω の塔 ωω、ωωω、… と積み上げた先にある数が、ε0\varepsilon_0 です。くわしくはヒルベルトの第2問題の解説にも書きました。

この証明について、有名な議論があります。ε₀までの帰納法は、ペアノ算術の中では証明できない原理です。そのため、ゲーデルの定理と矛盾はしません。一方で、これがヒルベルトの望んだ「だれもが納得する有限の方法」に入るのかどうかは、意見が分かれました。ゲンツェン自身は、この原理が「十分に明らか」であると考えていたと伝えられています。

業績5　ε₀の意味：算術の「強さ」をはかるものさし

ゲンツェンは、1939年に書き、1943年に発表された最後の論文で、さらに大事なことを示しました。ε₀より小さい順序数までの帰納法は、ペアノ算術の中で証明できること、そしてε₀までの帰納法そのものは、ペアノ算術では証明できないことです。つまり、ε₀はペアノ算術がちょうど届く範囲の限界を表す数だと分かったのです。

ここから、「体系の強さを、順序数ではかる」という考え方（順序数解析）が生まれました。ペアノ算術の強さは ε₀、もっと強い体系はもっと大きな順序数、という具合です。また、この結果は、ゲーデルの不完全性定理を別の道すじから証明したことにもなります。ε₀までの帰納法という、算術の言葉で書ける文が、算術では証明できないからです。

ε₀は、ふつうの数の問題ともつながっています。たとえばグッドスタイン数列（練習問題にも出します）は、どんな数から始めても必ず 0 に着きますが、そのことはペアノ算術では証明できないと、1982年にカービーとパリスが示しました。証明には、ε₀までの帰納法が使えます。

そのほかの仕事

1933年ごろには、ゲーデルと別々に、古典論理の算術を直観主義の算術の中に書き移す方法（ゲーデル・ゲンツェン翻訳）を考えました。これにより、古典算術の無矛盾性は直観主義算術の無矛盾性に帰着できることが分かります。また、ヒルベルトの弟子として、数学の基礎についての研究を続け、1938年には無矛盾性の証明の新しい形（シークエント計算にもとづく証明）も発表しています。

ゲンツェンの名前がつく公式・定理・用語

ゲンツェンの名前がつくものは、論理学と証明論の用語です。高校数学の公式ではありませんが、「証明」を学ぶうえで知っておくと役に立ちます。

  • 自然演繹：仮定を置いて閉じるという、人の推論に近い証明の形式。
  • シークエント計算（LK・LJ）：「A, B ⇒ C, D」という式の並びで証明を書く体系。LK は古典論理、LJ は直観主義論理。
  • カット除去定理（ハウプトザッツ）：回り道（カット）のない証明に、いつでも作りかえられるという定理。
  • 部分論理式性質：カットのない証明には、結論の式の部分しか出てこないという性質。
  • ゲンツェンの無矛盾性証明：ε₀までの超限帰納法を使って、ペアノ算術に矛盾がないことを示した証明。
  • ゲーデル・ゲンツェン翻訳：古典論理の式を直観主義論理の式に変える方法。
  • 順序数解析：体系の強さを順序数ではかる研究（ゲンツェンの仕事から生まれた分野）。

覚える必要はありませんが、高校数学の命題とは、逆・裏・対偶、必要条件・十分条件などを学ぶときに、「証明とは、仮定から結論へ、規則どおりに進むことだ」という感覚をもっていると、論理の問題が分かりやすくなります。

「ここが大事！」と説明する合格先生

合格先生

自然演繹の「仮定を置いて、結論が出たら閉じて「ならば」にする」という流れは、高校数学の証明そのものだよ。証明を書くときは、いま何を仮定しているかをいつも確かめよう。

ゲンツェンの逸話と名言

「実際の推論に近い形式」を求めた論理学者

ゲンツェンの論文の序文には、自分の研究の出発点が書かれています。それまでの論理学の体系が、数学者が実際に行う推論からはかなり遠いことに不満をもち、「実際の推論にできるだけ近い形式」を作ろうとした、という趣旨です。こうして生まれた自然演繹は、今の論理学の教科書でも、最初のほうで学ぶ形式としてよく使われています。

書き直され続けた無矛盾性の証明

算術の無矛盾性の証明は、一度で完成したのではなく、何度も書き直されました。1934年末に最初の証明ができたあと、2番目の証明に対して、ベルナイスやゲーデルからの指摘があったと伝えられています。最終的に、4つの証明が作られ、1938年の最後の証明は、ゲンツェンの得意としたシークエント計算を使ったものです。論理の世界では、1つの結論にいくつもの別の証明があることは珍しくなく、それぞれが新しい見方を教えてくれます。

ヒルベルトの助手として

ゲンツェンは、ヒルベルトの助手を務めました。ヒルベルトは数学の基礎についての計画を進めた大数学者で、ゲンツェンの無矛盾性の証明は、その計画を受けつぐ研究の1つです。ヒルベルトは1943年に亡くなりました。ゲンツェンの業績を、ヒルベルトがどう受けとめたかについては、くわしい記録が分かりにくいところがあります。

時代にのみこまれた研究者：政治との関わり

ゲンツェンの生涯を語るうえで、ナチス時代との関わりにふれないわけにはいきません。資料に書かれている事実は、次のとおりです。ゲンツェンは1933年11月に突撃隊（SA）に入り、1937年にナチス党（NSDAP）に入りました。1939年4月には、大学の職に就く手続きの一部として、ヒトラーへの忠誠の宣誓をしています。一方で、ユダヤ系だとして職を追われたベルナイスとは、戦争が始まるまで連絡を取り続けました。また、1935年にはユダヤ系の数学者フレンケルと手紙をやりとりしたことを、ナチス系の教員団体から問題にされたことがあります。ワイルは、1935〜36年に、ゲンツェンをアメリカのプリンストン高等研究所に迎えようと動いたとされます。

ゲンツェンがどのような考えで、これらの行動をとったのかについては、研究者のあいだでも見方が分かれています。伝記をまとめたメンツラー＝トロットは、当時の時代の背景をくわしく調べています。ここでは、事実だけを知ったうえで、数学の仕事と、人の行いを分けて考えることが大切です。

プラハでの最期

戦争が終わろうとする1945年の5月、ゲンツェンはプラハで拘束され、収容所で飢えのために亡くなりました。35歳でした。もし生きていれば、証明論はもっと早く、もっと大きく発展したのではないか、とよく言われます。

サクラちゃん

サクラちゃん

35歳で亡くなったのに、こんなにたくさんの仕事を残したんですね。

合格先生

合格先生

そうだね。自然演繹もシークエント計算も、無矛盾性の証明も、ぜんぶ20代の仕事なんだ。そして今、コンピュータのプログラムを検証するソフトの中で、ゲンツェンの考えた形式が使われているんだよ。

受験・勉強とゲンツェンのつながり

中学受験：「もし〜なら」で筋道を立てる

中学受験の算数でも、「もし〜だとしたら、〜になる」と仮定を置いて考える問題がたくさん出ます。つるかめ算の「全部つるだと仮定すると」は、まさに自然演繹の「仮定を置く」です。仮定から結論まで、筋道を追う習慣が、のちの数学の力になります。整数の性質を扱う素因数分解のやり方と例題も、「ただ1通りに分けられる」という性質をもとに、筋道を立てて答えを出す練習になります。

高校受験・大学受験：命題・集合・数学的帰納法

数学I・Aの「論理と集合」では、命題の真偽、逆・裏・対偶、必要条件・十分条件、背理法を習います。対偶の意味や集合の記号は、ゲンツェンの論理の言葉の入口です。数学Bの数列で学ぶ数学的帰納法の使い方と例題は、「n = 1 で成り立つ」「n = k で成り立つと仮定すると n = k + 1 でも成り立つ」の2段階で、すべての自然数について示す方法です。これは、ペアノの公理の中心にある考えで、ゲンツェンの超限帰納法は、この数学的帰納法を「無限の先」まで広げたものです。

大学の勉強へ：論理学・情報科学・プログラムの検証

大学の数学科や情報科学科では、ゲンツェンの自然演繹とシークエント計算を、論理学の授業で学びます。また、プログラムが正しく動くことを証明するソフト（定理証明支援系）には、ゲンツェンの形式の考えが使われています。数学を学ぶ人にも、プログラミングを学ぶ人にも、ゲンツェンの仕事は土台になっています。チューリング（計算の理論を作った人）の計算の理論と並んで、現代の「計算と証明」の学問の出発点の1つです。

勉強法として：証明を「整理」する習慣

ゲンツェンのカット除去の考えを、受験の勉強にたとえるなら、答案を整理し直すことです。回り道をした答案を、あとから見直して、いちばん短い筋道に書き直す。こうしたふり返りは、記述式の答案を書く力を確実に伸ばします。勉強の進め方は数学の勉強法（解法の暗記→演習→過去問）、論理の記号の読み方は数学でよく使う記号の意味一覧（∀・∃・Σ）も参考にしてください。

ゲンツェンがその後の数学にあたえた影響

  • 証明論：「証明」を数学の対象として調べる分野は、ゲンツェンの仕事で大きく発展しました。カット除去と順序数解析は、今も現役の研究分野です。
  • 論理学の教科書：自然演繹とシークエント計算は、世界中の論理学の授業で、標準的な形式として教えられています。
  • コンピュータ科学：証明の簡単化とプログラムの実行が対応する（カリー・ハワード対応）ことが分かり、プログラミング言語の理論や、定理証明支援系のもとになりました。チューリングの計算の理論とも、深く関わっています。
  • 集合論との関係：順序数解析は、カントールの作った順序数を、算術の強さをはかるものさしとして使いました。
  • 日本の研究：日本の竹内外史は、ゲンツェンの方法を発展させ、より強い体系の無矛盾性の研究に取り組みました。
  • 数学基礎論全体：ヒルベルトの計画に対して、ゲーデルが「できないこと」を示し、ゲンツェンが「何を足せばできるか」を示しました。2人の仕事は、数学基礎論の2つの柱です。

ゲンツェンの仕事は、「数学の確かさ」を問う長い歴史の中に位置づけられます。ポアンカレやラッセルが考えた基礎の問いに、ゲンツェンは「どの道具を使えば、どこまで保証できるか」という、新しい形の答えを出したのです。

ゲンツェンに挑戦！練習問題

やさしい

  1. 命題「x > 0 ならば x² > 0」の対偶を答えなさい。
    答えと解説を見る対偶は「結論を否定したものならば、仮定を否定したもの」です。結論「x² > 0」の否定は「x² ≦ 0」、仮定「x > 0」の否定は「x ≦ 0」なので、対偶は「x² ≦ 0 ならば x ≦ 0」です。
  2. 自然演繹の考え方で、「p ならば q」と「q ならば r」が成り立つとき、「p ならば r」が成り立つ理由を説明しなさい。
    答えと解説を見るまず p が成り立つと仮定します。「p ならば q」から q が成り立ち、さらに「q ならば r」から r が成り立ちます。仮定した p から r が出たので、仮定を閉じて「p ならば r」が言えます。

ふつう

  1. 数学的帰納法で、すべての自然数 n について 1 + 2 + … + n = n(n + 1)/2 が成り立つことを示しなさい。
    答えと解説を見る(i) n = 1 のとき、左辺は 1、右辺は 1×2/2 = 1 で成り立つ。(ii) n = k で成り立つと仮定すると、1 + 2 + … + k + (k + 1) = k(k + 1)/2 + (k + 1) = (k + 1)(k + 2)/2。これは n = k + 1 のときの式です。(i)(ii) より、すべての自然数 n で成り立ちます。
  2. 自然数の組 (a, b) に対して、次の操作をくり返します。b > 0 なら (a, b − 1) にする。b = 0 で a > 0 なら、(a − 1, 好きな自然数) にする。この操作は、必ず有限回で止まることを説明しなさい。
    答えと解説を見るa は増えることがなく、a が減るのは b = 0 のときだけです。a の値ごとに、b は有限回しか減らないので、a が1つ減るまでの回数は有限です。a は最初の値より多くは減らせないので、全体で有限回で止まります。これは、組を ω×a + b という順序数と見て、操作のたびに番号が小さくなる、という考え方（ゲンツェンの方法を小さくした例）です。

むずかしい

  1. グッドスタイン数列を次のように作ります。数 m を「底 2 の累乗の和」で書き（例：3 = 2¹ + 1）、底の 2 をすべて 3 に取りかえてから 1 を引く。次は底を 3→4 に取りかえて 1 を引く。以下、底を 1 つずつ増やしながら同じことをくり返す。最初の数が 3 のとき、数列を 0 に着くまで書きなさい。
    答えと解説を見る3 → (底を 3 にして 3¹ + 1 = 4、1 を引く) 3 → (底を 4 にして、3 = 3¹ は 4¹ = 4、1 を引く) 3 → (3 は底 4 では「3」。底を 5 にしても 3、1 を引く) 2 → (底を 6 にしても 2、1 を引く) 1 → (1 を引く) 0。数列は 3, 3, 3, 2, 1, 0 となって、0 に着いて止まります。（3 より大きな数から始めると、とても大きくなってから 0 に着きます。必ず 0 に着くことは、ε₀までの帰納法で証明できます。）
  2. 順序数 ω×2（ω＋ω のこと）と ω² では、どちらが大きいですか。また、ω より大きく ω×2 より小さい順序数を3つ挙げなさい。
    答えと解説を見るω² は ω を ω 回足したものなので、ω×2 より大きく、ω² ＞ ω×2 です。ω より大きく ω×2 より小さい順序数は、ω＋1、ω＋2、ω＋100 など、ω に自然数を足したものです。

ゲンツェンと関係する数学者

数学の公式を1つずつ学ぶなら算数・数学の公式一覧（公式辞典）、数学全体の入口は算数・数学 公式と用語の一覧（学年別・分野別）もどうぞ。

20世紀の数学者

← 前の時代：ヴェイユの業績と生涯　｜　次の時代：角谷静夫の業績と生涯 →

有名な数学者一覧（年代順・国別・分野別）で、ほかの数学者も見られます。数学者たちが挑んだ問題は数学の難問・未解決問題の一覧にまとめています。

読みもの（合格大作戦の数学の記事）

よくある質問

ゲンツェンは何をした人ですか？

ゲンツェンは、20世紀前半のドイツの数学者・論理学者です。証明を数学の対象として調べる「証明論」の中心人物で、自然演繹、シークエント計算、カット除去定理を作り、1936年にペアノ算術の無矛盾性を証明しました。

自然演繹とは何ですか？

数学者が実際に行う推論に近い、証明の形式です。仮定を置き、結論が出たら仮定を閉じて「ならば」にします。「かつ」「または」「ならば」などごとに、導入と除去の規則があります。ゲンツェンが1930年代に作りました。

シークエント計算のLKとLJは、何がちがうのですか？

LKは、ふつうの数学で使う古典論理の体系で、シークエントの右側に式をいくつでも置けます。LJは、直観主義論理の体系で、右側を1つまでに制限します。Kは「古典的」、Jは「直観主義的」を表すドイツ語の頭文字です。

カット除去定理とは何ですか？

「補題を使った回り道（カット）のある証明は、カットのない証明に作りかえられる」という定理です。ゲンツェンはハウプトザッツ（基本定理）とよびました。カットのない証明には結論の式の部分しか出てこないので、論理の無矛盾性などが示せます。

ゲンツェンの無矛盾性の証明は、ゲーデルの定理と矛盾しないのですか？

矛盾しません。ゲーデルの第二不完全性定理は、体系が自分自身の無矛盾性を自分の中では証明できない、と言います。ゲンツェンは、算術では証明できないε₀までの超限帰納法という、より強い原理を使ったからです。

ε₀（イプシロン・ゼロ）とは何ですか？

ω、ω^ω、ω^(ω^ω)、…と積み上げた先にある順序数です。ペアノ算術は、ε₀より小さい順序数までの帰納法は証明できますが、ε₀までの帰納法は証明できません。ゲンツェンは、このε₀が算術の強さの限界だと示しました。

ゲンツェンは何歳で、どこで亡くなったのですか？

ゲンツェンは、1945年8月4日、第二次世界大戦が終わった直後のプラハで、35歳で亡くなりました。5月に拘束されたあと、約3か月の収容のなかで、栄養失調のためだったと伝えられています。

ゲンツェンはナチス党に入っていたのですか？

資料によると、1933年11月に突撃隊、1937年にナチス党に入り、1939年にはヒトラーへの忠誠の宣誓をしました。一方で、ユダヤ系で職を失った師のベルナイスとは連絡を取り続けています。本人の考えについては、見方が分かれています。

ゲンツェンは受験や高校数学に関係がありますか？

あります。高校数学の命題・対偶・背理法・数学的帰納法は、ゲンツェンが調べた「証明のしかた」そのものです。ゲンツェンの名前は入試に出ませんが、論理の問題や記述式の証明の土台になる考え方です。

あわせて読みたい

出典・参考

  • G. Gentzen, “Untersuchungen über das logische Schließen”（Mathematische Zeitschrift, 1934〜35年）
  • G. Gentzen, “Die Widerspruchsfreiheit der reinen Zahlentheorie”（Mathematische Annalen, 1936年）
  • MacTutor History of Mathematics「Gerhard Gentzen」（セント・アンドルーズ大学）
  • スタンフォード哲学百科事典「The Development of Proof Theory」
  • Eckart Menzler-Trott, “Logic’s Lost Genius: The Life of Gerhard Gentzen”（2007年）

最終更新：2026年11月3日／作成：大学受験合格大作戦