様々な定式化による算術の無矛盾性証明と Gentzen の当初の目標
Consistency proofs for ﬁrst-order arithmetic in various formulations andGentzen’s original goal
安東 里沙子Abstract
This paper compares and analyzes the consistency proofs for ﬁrstorder arithmetic in various formulations, in light of Gentzen’s originalgoal. First, Natural deduction and Sequent calculus systems are compared, and proofs of Normalization theorem and Cut-elimination theorem are outlined. Next, Gentzen’s consistency proofs for ﬁrst-orderarithmetic, subsequent works on the consistency proofs for ﬁrst-orderarithmetic (by normalization) after Gentzen, and works on inﬁnite
proof systems are introduced. Then, focusing on the compatibility of“naturalness” and “technical advantage” of proof systems, this paper
focuses on the consistency proof in Troelstra and Schwichtenberg [16].

1

研究テーマ

本稿では、特に自然演繹に着目した上で、様々な定式化による算術の無矛盾性証明を比較し、関連を探求する。Gentzen により提案された自然演繹体系は、証明体系の自然な定式化が実現されている代わりに、特にその構造の分析に際して、ある種の技術的困難が伴っているといえる。そこで、主にその技術的困難をどう克服するかという観点から、無矛盾性証明で用いられる様々な手法を概観し、算術の無矛盾性証明に関する諸研究の位置付けについて整理する。また、それを通じて、無矛盾性証明に関する Gentzen のオリジナルの着想について検討する。最後に、形式的体系の「自然さ」と、その正確な無矛盾性証明に必要な「技術的利点」は両立するかといった問いについて、両立する体系が可能であることを示唆する。

2

研究の背景・先行研究

証明論の代表的な証明体系として、自然演繹 (NJ, NK) とシークエント計算 (LJ, LK) がある。自然演繹において、仮定を閉じる操作が与えられ、さらに単一の論理式のみが結論に現れること、シークエント計算において、複数の論理式の集合が結論に現れてもよいことは、両者の体系を比較した際に、各々を特徴づける性質の一部として挙げられるだろう。自然演繹における導入規則（除去規則）はシークエント計算における R 規則（L 規則）にそれぞれ対応しており、例えば、条件法の導入規則は以下の左の推論規則であり、条件法の R 規則 1 は以下の右の推論規則である。

1

[A]
B→IA→BA, Γ ⊢ ∆, B→RΓ ⊢ ∆, A → B

自然演繹は、数学の証明を典型とするような、我々が実際に行なっている推論とできるだけ近い形で推論規則を定式化した体系である (Gentzen [5]) 。
その一方で、自然演繹は、古典論理においてはその定式化に成功しているとはいえないだろう。後で詳しく述べるが Gentzen [5] には、正規化定理は、直観主義的自然演繹 (NJ) では直ちに証明できたが、古典的自然演繹 (NK) では証明できなかったとある。Gentzen は正規化定理の帰結を古典的体系に拡張するために、古典的シークエント計算 (LK) を考案し、それに対応する定理であるカット消去定理を証明した。たしかに、シークエント計算は（特に古典論理における）その技術的利点においては優れた定式化であるといえる。しかし、その定式化において「自然さ」が失われている点は軽視できない 2 。例
えば、Steinberger [15] は、論理的推論主義者（証明論的意味論の立場）は、複数の結論をもつ論理体系を拒否すべきであると主張する。証明論的意味論の観点からいえば、演繹体系は我々の推論実践と適切に結びついていなければならないが、複数の結論をもつ論理体系は我々の通常の推論様式を自然に表現できていないからである 3 。このように、自然演繹は、推論の自然な定式化に成功している代わりに技術的な困難を伴い、シークエント計算は、定式化において自然さを失っている代わりに技術的な利点を備えている。すなわ
ち、両者の体系はそれらの体系がもつ自然さと技術的利点において、各々相反する優位性を備えているといえる。
Gentzen の純粋論理に関する研究は、算術と解析学の無矛盾性証明のための予備的なものであった。Gentzen は当初、自然演繹の正規化定理を直観主義算術の体系に拡張することで、算術の無矛盾性を証明することを目指していた (Gentzen [5])。
正規化定理とは、ある前提 Γ から結論 A への証明 d が与えられたとき、dに簡約手続きを有限回適用することで、Γ から A への正規形の証明を得ることができる、というものである。この定理の帰結として、自然演繹体系の無矛盾性が示される。正規形の証明とは、遠回りを含まない証明、すなわち、導入規則が適用された直後に除去規則が適用されているような論理式（極大論理式）を含まない証明のことであり、以下は、簡約手続きの一部である。

2

[A]
d2
B→IA→BB
d3d1A →E,→d1A
d2B
d3

長らく、Gentzen は正規化定理に関しては、証明の背後にある直観的な考えを説明するにとどまっており、完全な証明は Prawitz [10] で与えられたとされていたが、von Plato [17] によれば、2005 年 2 月に発見された Gentzen の博士論文の初期の手書き原稿には、直観主義的自然演繹の正規化に関する詳細な証明が含まれていたのである。それにもかかわらず、Gentzen はカット消去定理を応用することで、算術の無矛盾性証明を得た。カット消去定理とは、シークエント計算において、ある前提 Γ から結論 ∆ への証明が与えられたとき、有限回の操作により、Γ から ∆ へのカット規則の適用を含まない証明（遠回りを含まない証明）を得ることができる、というものであり、ちょうど自然演繹における正規化定理に相当するものである 4 。
Gentzen が無矛盾性証明のために自然演繹ではなくシークエント計算による定式化を選択したのは、ひとつには、自然演繹における、直観主義的体系に追加されねばならない二重否定除去則（¬¬A → A）の特別な立ち位置による。二重否定除去則は、否定の導入則から正当化できないという点から、簡約手続きを与えることができないのである。これはシークエント計算を採用する際には全く問題とならない。もうひとつには、自然演繹ではおおよそ保たれるインフォーマルな証明における文の自然な連続が、シークエント計算
では、ある目的のもとつくられた人工的な列に置き換わり、それが無矛盾性証明において技術的に有利であることによる。
最小論理に算術の公理と爆発則（⊥ → A）を追加することで、直観主義算術（ハイティング算術、以下 HA）の体系が得られ、さらに二重否定除去則を追加することで、古典算術（ペアノ算術、以下 PA）の体系が得られる。論
理体系の無矛盾性を算術の理論に拡張する際の問題点は、主に、算術の場合は複雑な論理式（量化子を含む論理式）が論理規則の適用のみならず、数学的帰納法の使用によって導出されることもある点である。つまり、数学的帰納法の使用を構成的に正当化することに困難が生じる。
Gentzen は生涯に数回にわたって算術の無矛盾性証明に取り組んでいる。
1934 年に発表された最初の無矛盾性証明は、ファン定理を暗黙のうちに使用しているという Bernays の批判により取り下げられたが、この批判は Bernays自身により撤回され、Gentzen [7] として Gentzen の死後に出版されている。

3

また、Gentzen [5] は算術の無矛盾性に関するもうひとつの重要な帰結として、PA、特にその無矛盾性の問題が、HA に還元されることを示した。1936 年に発表された第二の無矛盾性証明では、証明図への順序数記法の割り当てが定義され、0 までの超限帰納法の原理の構成的証明に依拠したものとなっている。1938 年に発表された第三の無矛盾性証明は、第二の無矛盾性証明を純粋なシークエント計算で行った改訂版である。Akiyoshi and Takahashi [1] の分
析によれば、第一の証明が内容的（意味論的）正しさに関する証明であり、第三の証明が形式的（証明論的）正しさに関する証明である。また、Akiyoshiand Takahashi [1] によれば、第二の証明は内容に関する証明でも形式に関する証明でもあり、二つの側面が互いにどのように関連しているかに関する議論もなされている。第三の無矛盾性証明までとは対照的に、1943 年に発表された第四の無矛盾性証明は、非導出可能性に基づいている。また、Gentzen は1939 年から 1943 年にかけてさらなる無矛盾性証明に取り組んでいた。1938年の第三の無矛盾性証明を直観主義的シークエント計算によって再構成し、HA の無矛盾性を証明するというものである。
Gentzen によって与えられた標準的な無矛盾性証明はシークエント計算によるものであり、後続の研究の多くはそれに基づいているが、自然演繹による無矛盾性証明に関する研究も存在する。Kanckos [9] は、自然演繹で形式化された HA の無矛盾性証明を与えた。この証明は、Howard [8] による証明図へのベクトル記法の割り当てに基づく、正規化の手法がベースとなっている。
この手法を用いた証明は、Gentzen のオリジナルの証明で必要となる等高線(Höhenlinie) の概念の使用を避けられている。また、この HA の無矛盾性証明での議論を一般化し、Siders [14] は自然演繹で形式化された PA の無矛盾性証明を与えている。一方で、Prawitz [11] は、Gentzen の 1936 年の無矛盾性証
明での手法を自然演繹に応用することで、PA の無矛盾性証明を与えている。
また、無矛盾性証明に関する議論を順序数解析というより数学的なトピックに移行するために、ω 規則という新たな道具立てが考案された。ω 規則とは、A(x)（x は任意の数）に具体的な数項を代入して得られた無限個の論理式 A(i)（i < ω ）から、∀xA(x) を導出する推論規則であり、以下の形をしている。

· · · A(i) · · ·ω∀xAω 規則の使用は、超限的命題の有意味性を実無限の概念に訴えることなく正当化することを目的とする Gentzen による無矛盾性証明の手法とはかけ離れてい4

るように見えるが、実は有限的に正当化される。Buchholz [3] によれば、ω 規則に基づくシークエント計算体系におけるカット消去の手続きから、Gentzenによるカット消去の手続きを復元することができるからである。ω 規則に基づく体系（無限的体系）による証明の分析は、現代の証明論研究においては標準的である。Buchholz [3] は Gentzen の 1938 年の無矛盾性証明を、無限的シークエント計算体系におけるカット消去法による現代的な形で再提示している。一方で Troelstra and Schwichtenberg [16] は、無限的自然演繹体系に基づく算術の正規化定理を証明しており、無矛盾性証明に相当する帰結が得られている。

3筆者の主張ここまで、自然演繹とシークエント計算の体系の比較から始まり、正規化定理とカット消去定理、Gentzen による算術の無矛盾性証明、Gentzen 以降の（正規化による）算術の無矛盾性証明に関する研究、無限的証明体系に基づく研究についてごく簡単に紹介してきた。これらの研究の中でも、特にPrawitz [11] と Troelstra and Schwichtenberg [16] による証明は、正規化定理を算術の体系に拡張することで算術の無矛盾性を証明するという仕事を、Gentzen による 1936 年の無矛盾性証明の手法に基づき達成しているものであるといえよう。Prawitz [11] ではかなり詳細な証明が示されている。Troelstraand Schwichtenberg [16] の証明はカリーハワード対応に基づいて、λ 記法によって記述されている 5 。
ここで、自然さと技術的利点を両立させるような体系は存在するかという問いが重要である。筆者は、Troelstra and Schwichtenberg [16] の証明で採用された無限的自然演繹体系はその一つに値するのではないかと考える。無限的体系は、無限個の前提を持つ推論規則という、我々の推論の実践からかけ離れているように見える概念を含んでいるという点で、自然さを備えていないと思われるかもしれない。しかし、標準的な証明体系に現れる固有変項(eigenvariable) の解釈も、果たして自然な思考の対象であるだろうか。標準的な証明体系と無限的な証明体系の間に、無限の解釈に関する実質的な違いが存在するようには思えないのである。
固有変項というある種の超越的な概念に関して、それが何であるかについては様々な立場があり、たとえば、道具主義的説明、量化的説明、そして指示的説明などが与えられている (Breckenridge and Magidor [2])。道具主義的説
明によれば、固有変項は意味をもたず、意味のある前提から意味のある結論に到達するための便利な道具としての役割にすぎない。量化的説明によれば、固有変項は、量化子によって暗黙のうちに束縛される変数である（あるいは、5

それ自体が形を変えた量化子である）。最後に、固有変項とはある種の対象を指示する名前であるという、指示的説明がある。指示的説明の代表的論者の一人である Fine [4] によれば、固有変項とは任意の対象 (arbitrary object) であり、また、Breckenridge and Magidor [2] によれば、なんらかの通常の対象である。ただし、どの特定の対象を指示しているのかは知りえないという。
ω 規則の従来の位置付けは、シュッテ学派により単なる技術的・数学的な工夫のため考案された道具立てである、というものである (Schütte [13])。それを使用することの利点は、証明図に現れる固有変項を消去できることにある。
例えば、数学的帰納法の適用を含む証明は、無限的自然演繹体系に以下のように埋めこまれる 6 。

[A(x)]..
..
..
..
A(0) A(S(x))
Ind∀xA(x)

,→

..
..
A(0)

[A(0)] [A(1)]
..
..
..
..
A(1)
A(2)
∀xA(x)···

ω

このように埋め込まれた証明は固有変項を含んでいないため、簡約手続きを問題なく適用することができる。ここで、固有変項を消去するということは、固有変項の現れを ω 規則の適用に置き換えているということでもあるが、そのような意味で、ω 規則は固有変項、すなわち任意の対象を、証明論的意味論の立場から意味づけているといえないだろうか。

4

今後の展望

算術が無矛盾であるという帰結自体は、Gentzen によりほとんど完全な形で得られている。しかし、どのような定式化によってそれが与えられるかについては今後も探求していく必要がある。特に、自然演繹で定式化された算術の無矛盾性証明、すなわち算術に対する正規化定理に関する研究は、これまで十分に注目されてこなかった。しかし、自然演繹は、推論規則の適用によって論理式の意味を捉えようとする証明論的意味論の立場において特に重視されており、この点において、自然演繹は証明論研究において重要な意義をもつはずである。さらに、人間の証明活動を自然に定式化することに成功し、証明支援系の研究をはじめとする様々な研究分野での応用可能性をもつ自然演繹について、より詳細な分析が与えられることは不可欠である。

6

注
1

規則に含まれる Γ 及び ∆ はそれぞれ 0 個以上の論理式の集合である。

2

自然演繹は 1980 年代以降、証明支援系の研究の基礎にある体系でもあり、人間にとって使いやすい証明支援系を設計する上でも、証明の「自然さ」の探究は重要性をもつ。
3

反対に、Restall [12] は、主張と否認の概念があれば、論理的帰結を複数の前提と結論をもつ論証として分析してよいと主張する。しかしこの主張は、ある種の意味論的観点からの分析において、複数結論をもつ論理体系の優位性を示したに過ぎないように思われる。
4

ただし、正規化の手続きとカット消去の手続きの間に対応関係が成り立つか否かについては議論の余地がある (Zucker [18])。
5

安東 [19] では、この証明を自然演繹に変換し、より詳細な証明を与えた。

6

実際には、埋めこみ後の証明図は無限個の前提をもつ。

文献[1] Ryota Akiyoshi and Yuta Takahashi. Contentual and formal aspects ofGentzen’s consistency proofs. In Philosophical Logic: Current Trends
in Asia: Proceedings of AWPL-TPLC 2016, pages 95–137. Springer,
2017.
[2] Wylie Breckenridge and Ofra Magidor. Arbitrary reference. Philosophical Studies, 158:377–400, 2012.
[3] Wilfried Buchholz. Explaining Gentzen’s consistency proof within inﬁnitary proof theory. In Kurt Gödel Colloquium on ComputationalLogic and Proof Theory, pages 4–17. Springer, 1997.
[4] Kit Fine. A defence of arbitrary objects. Proceedings of the AristotelianSociety, Supplementary Volumes, 57:55–89, 1983.
[5] Gerhard Gentzen. Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39:176–210, 405–431, 1935. English translationin [6].
[6] Gerhard Gentzen. The Collected Papers of Gerhard Gentzen. NorthHolland, 1969.

7

[7] Gerhard Gentzen. Der erste Widerspruchsfreiheitsbeweis für die klassische Zahlentheorie. Archive for Mathematical Logic, 16(3-4):97–118,
1974.
[8] William Alvin Howard. Assignment of ordinals to terms for primitive
recursive functionals of ﬁnite type. In Studies in Logic and the Foundations of Mathematics, volume 60, pages 443–458. Elsevier, 1970.
[9] Annika Kanckos. Consistency of Heyting arithmetic in natural deduction. Mathematical Logic Quarterly, 56(6):611–624, 2010.
[10] Dag Prawitz. Natural Deduction: A Proof-theoretical Study. Courier
Dover Publications, 2006.
[11] Dag Prawitz. A note on how to extend Gentzen’s second consistency
proof to a proof of normalization for ﬁrst order arithmetic. In Reinhard
Kahle and Michael Rathjen, editors, Gentzen’s Centenary: The Questfor Consistency, pages 131–176. Springer, 2015.
[12] Greg Restall. Multiple conclusions. In Logic, Methodology and Philosophy of Science: Proceedings of the Twelfth International Congress,
pages 189–205. Kings College Publications London, 2005.
[13] Kurt Schütte. Beweistheoretische Erfassung der unendlichen Induktion
in der Zahlentheorie. Mathematische Annalen, 122:369–389, 1950/51.
[14] Annika Siders. Normalization proof for Peano arithmetic. Archive forMathematical Logic, 54:921–940, 2015.
[15] Florian Steinberger. Why conclusions should remain single. Journal ofPhilosophical Logic, 40:333–355, 2011.
[16] Anne Sjerp Troelstra and Helmut Schwichtenberg. Basic Proof Theory.
Cambridge University Press, 2000.
[17] Jan von Plato. Gentzen’s logic. In Dov Gabbay, editor, The Handbookof the History of Logic, pages 667–721. Elsevier, 2009.
[18] Jeﬀrey Zucker. The correspondence between cut-elimination and normalization. Annals of mathematical logic, 7(1):1–112, 1974.
[19] 安東 里沙子. ω 規則に基づく自然演繹体系による算術の無矛盾性証明.
慶應義塾大学文学研究科修士論文, 2024.
（慶應義塾大学）8