ヒルベルトシステム

論理学、より具体的には証明論において、ヒルベルト体系は、ヒルベルト計算、ヒルベルト式体系、ヒルベルト式証明体系、ヒルベルト式演繹体系、またはヒルベルト・アッカーマン体系とも呼ばれ、ゴットロブ・フレーゲ^[1]とダヴィド・ヒルベルト^[2]に帰せられる形式的証明 体系の一種である。これらの演繹体系は、第一階述語論理について研究されることが最も多いが、他の論理についても興味深い。

ヒルベルト体系は、公理と推論規則から定理を生成する演繹体系として定義されます。^{[3] [4] [5]}特に、唯一仮定される推論規則が可能性（modus ponens）である場合に当てはまります。^{[6] [7]すべてのヒルベルト体系は}公理体系であり、多くの著者は、より具体的な用語を一切使用せずに、自らのヒルベルト体系を宣言する際に、公理体系というより限定的な用語のみを使用しています。 ^{[8] [9] [10]}この文脈において、「ヒルベルト体系」は、公理を使わず推論規則のみを用いる自然演繹体系^[3]と対比されます。

「公理的」論理証明体系に言及する文献はすべて、それを単に公理を含む論理証明体系と特徴づけているが、「ヒルベルト体系」という用語の派生語を用いる文献では、異なる定義が用いられる場合がある。本稿ではこの定義は用いない。例えば、トロルストラは「ヒルベルト体系」を、公理を含み、かつ、を唯一の推論規則とする体系と定義している。 ^[11]特定の公理集合は、「ヒルベルト体系」^[12]あるいは「ヒルベルト式計算」^{[13]と呼ばれることもある。「ヒルベルト式」は、公理}を図式的に表すタイプの公理体系を指すために使用される場合もある^[2]。例えば、以下のP2の§ 図式的形式を参照のこと。しかし、他の文献では、図式的公理を含む体系と置換規則を含む体系の両方を包含するものとして「ヒルベルト式」という用語が用いられている。^[14]本稿も同様である。論理学における公理的証明体系を説明するために「ヒルベルト式」や類似の用語が使われるようになったのは、ヒルベルトとアッカーマンの『数理論理学の原理』 （1928年）の影響によるものである。^[2]${\displaystyle {\rightarrow }E}$ ${\displaystyle {\forall }I}$

ヒルベルト体系の多くの変種は、論理公理と推論規則のトレードオフのバランスをとるという点で特徴的な方針をとる。^{[1] [6] [15] [11]}ヒルベルト体系は、多数の論理公理のスキーマと少数の推論規則の選択によって特徴づけられる。自然演繹の体系は反対の方針をとり、多くの演繹規則を含むが、公理スキーマはほとんどないかまったくない。^[3]最も一般的に研究されているヒルベルト体系は、 命題論理の場合は推論規則を1つだけ、または述語論理も処理できるように一般化を 加えて2つと、無限の公理スキーマをいくつか持つ。 論理的様相論理のヒルベルト体系（ヒルベルト・ルイス体系とも呼ばれる）では、必然性規則も必要となる。いくつかのシステムでは、公理スキーマを介した無限の式集合の代わりに、具体的な式の有限リストを公理として使用しており、その場合には均一な置換規則が必要である。^[14]

ヒルベルト体系の多くの変種に共通する特徴は、その推論規則のいずれにおいても文脈が変化しないということである。一方、自然演繹とシーケント計算はどちらも文脈を変える規則を含んでいる。^{[16]したがって、仮説的判断ではなく}トートロジーの導出可能性のみに興味がある場合、ヒルベルト体系を、その推論規則にかなり単純な形式の判断のみが含まれるように形式化することができる。他の 2 つの演繹体系では同じことはできない。^[要出典]それらの推論規則の一部では文脈が変化するため、トートロジーの導出可能性を証明するためだけにそれらの規則を使いたい場合でも、仮説的判断を回避できるように形式化することはできない。

正式な控除

控除制度の図解

ヒルベルト体系において、形式的演繹（または証明）とは、各式が公理であるか、あるいは推論規則によって前の式から得られる式からなる有限列である。これらの形式的演繹は自然言語による証明を模倣したものであるが、より詳細である。

が仮説として考えられる式の集合であると仮定します。例えば、 は群論または集合論の公理の集合である可能性があります。 という表記は、の論理公理と要素のみを公理として用いることで終わる演繹が存在することを意味します。したがって、非公式には、は のすべての式を仮定して が証明可能であることを意味します。 ${\displaystyle \Gamma }$ ${\displaystyle \Gamma }$ ${\displaystyle \Gamma \vdash \phi }$ ${\displaystyle \phi }$ ${\displaystyle \Gamma }$ ${\displaystyle \Gamma \vdash \phi }$ ${\displaystyle \phi }$ ${\displaystyle \Gamma }$

ヒルベルト体系は、論理公理の多数のスキーマを用いることで特徴付けられます。公理スキーマとは、ある形式のすべての式を特定のパターンに置き換えることで得られる公理の無限集合です。論理公理の集合には、このパターンから生成される公理だけでなく、それらの公理のいずれかの一般化も含まれます。式の一般化は、式に0個以上の全称量化子を接頭辞として付加することで得られます。例えば、はの一般化です。 ${\displaystyle \forall y(\forall xPxy\to Pty)}$ ${\displaystyle \forall xPxy\to Pty}$

命題論理

以下は命題論理で用いられてきたヒルベルト体系の一部である。そのうちの一つ、§ P2 の図式的形式はフレーゲ体系とも考えられている。

フレーゲの用語集

公理的証明は、紀元前300年頃の古代ギリシャの有名な教科書、ユークリッドの『幾何学原論』以来、数学において用いられてきました。しかし、ヒルベルト体系とみなされる最初の完全に形式化された証明体系は、ゴットロープ・フレーゲの1879年の『ベグリフシュリフト』に遡ります。^{[9] [17]}フレーゲの体系は、結合子として含意と否定のみを用い、[18 ^] 6つの公理を有し、^[17]以下の通りです。^{[19] [20]}

• 命題1:${\displaystyle a\supset (b\supset a)}$
• 命題2:${\displaystyle (c\supset (b\supset a))\supset ((c\supset b)\supset (c\supset a))}$
• 命題8:${\displaystyle (d\supset (b\supset a))\supset (b\supset (d\supset a))}$
• 提案28:${\displaystyle (b\supset a)\supset (\neg a\supset \neg b)}$
• 提案31:${\displaystyle \neg \neg a\supset a}$
• 提案41:${\displaystyle a\supset \neg \neg a}$

フレーゲはこれらを、モーダス・ポネンスや置換規則（使用されたが、正確に述べられたことはなかった）とともに使用して、古典的な真理機能的命題論理の完全かつ一貫した公理化を実現した。^[19]

ŁukasiewiczのP₂

ヤン・ウカシェヴィチは、フレーゲの体系において、「第三公理は先行する二つの公理から導かれるため不要であり、最後の三つの公理は一つの文に置き換えることができる」ことを示した。^{[20]これをウカシェヴィチの}ポーランド語表記から現代表記に置き換えると、次のようになる。したがって、ウカシェヴィチはこの三つの公理の体系を 考案したとされている^{[17] 。}${\displaystyle CCNpNqCqp}$ ${\displaystyle (\neg p\rightarrow \neg q)\rightarrow (q\rightarrow p)}$

• ${\displaystyle p\to (q\to p)}$
• ${\displaystyle (p\to (q\to r))\to ((p\to q)\to (p\to r))}$
• ${\displaystyle (\neg p\to \neg q)\to (q\to p)}$

フレーゲのシステムと同様に、このシステムは置換規則を使用し、推論規則としてモーダス・ポネンスを使用します。^[17]全く同じシステムが（明示的な置換規則とともに）アロンゾ・チャーチによって提示され、^[21]彼はそれをP 2システムと呼び_、^{[21] [22]}普及に貢献しました。^[22]

Pの模式図₂

置換規則の使用を避けるには、公理を図式的に表し、それを用いて無限の公理集合を生成するという方法がある。したがって、ギリシャ文字を用いて図式（任意の整形式式を表すメタ論理変数）を表すと、公理は次のように表される。^{[9] [22]}

• ${\displaystyle \varphi \to (\psi \to \varphi )}$
• ${\displaystyle (\varphi \to (\psi \to \chi ))\to ((\varphi \to \psi )\to (\varphi \to \chi ))}$
• ${\displaystyle (\neg \varphi \to \neg \psi )\to (\psi \to \varphi )}$

_{P 2}の図式的バージョンは、ジョン・フォン・ノイマンに帰属し、^[17]メタマスの「set.mm」形式証明データベースで使用されています。 ^[22]実際、置換規則を公理スキーマで置き換えるというアイデア自体がフォン・ノイマンに帰属しています。^{[23] P} ₂の図式的バージョンは、ヒルベルトにも帰属し、この文脈で命名されました。^[24]${\displaystyle {\mathcal {H}}}$

推論規則が図式的な命題論理体系はフレーゲ体系とも呼ばれる。「フレーゲ体系」という用語を最初に定義した著者ら^[25]が指摘するように、この用語は実際には、公理スキーマではなく公理を用いていた上記のフレーゲ自身の体系を除外するものである^{[23] 。}

Pにおける証明例₂

例として、P ₂における の証明を以下に示します。まず、公理に名前を付けます。 ${\displaystyle A\to A}$

（A1）${\displaystyle (p\to (q\to p))}$

（A2）${\displaystyle ((p\to (q\to r))\to ((p\to q)\to (p\to r)))}$

（A3）${\displaystyle ((\neg p\to \neg q)\to (q\to p))}$

そしてその証明は次のようになります。

1. ${\displaystyle A\to ((B\to A)\to A)}$       （（A1）の例）
2. ${\displaystyle (A\to ((B\to A)\to A))\to ((A\to (B\to A))\to (A\to A))}$       （（A2）の例）
3. ${\displaystyle (A\to (B\to A))\to (A\to A)}$       （(1)と(2)からmodus ponensによる）
4. ${\displaystyle A\to (B\to A)}$       （（A1）の例）
5. ${\displaystyle A\to A}$       （（4）と（3）から、modus ponensによる）

述語論理（例のシステム）

述語論理の公理化は無限に存在する。なぜなら、いかなる論理においても、その論理を特徴付ける公理と規則を選択する自由があるからである。ここでは、9つの公理と、モーダス・ポネンス規則のみを持つヒルベルト体系について説明する。これは、1規則公理化と呼ばれ、古典的な等式論理を記述する。この論理のための最小限の言語を扱う。そこでは、式は接続詞とのみ、量指定子 のみを使用する。後ほど、演繹可能な式のクラスを拡張することなく、この体系を拡張して、やなどの追加の論理接続詞を含める方法を示す。 ${\displaystyle \lnot }$ ${\displaystyle \to }$ ${\displaystyle \forall }$ ${\displaystyle \land }$ ${\displaystyle \lor }$

最初の 4 つの論理公理スキーマは、（modus ponens とともに）論理接続詞の操作を可能にします。

P1.${\displaystyle \phi \to \phi }$

P2.${\displaystyle \phi \to \left(\psi \to \phi \right)}$

P3.${\displaystyle \left(\phi \to \left(\psi \rightarrow \xi \right)\right)\to \left(\left(\phi \to \psi \right)\to \left(\phi \to \xi \right)\right)}$

P4.${\displaystyle \left(\lnot \phi \to \lnot \psi \right)\to \left(\psi \to \phi \right)}$

公理P1は冗長であり、P3、P2、および可能性（証明参照）から導かれる。これらの公理は古典的な命題論理を記述する。公理P4がなければ、肯定的含意論理が得られる。最小論理は、代わりに公理P4mを追加するか、 と定義することで実現される。 ${\displaystyle \lnot \phi }$ ${\displaystyle \phi \to \bot }$

P4m。${\displaystyle \left(\phi \to \psi \right)\to \left(\left(\phi \to \lnot \psi \right)\to \lnot \phi \right)}$

直観主義論理は、正含意論理に公理P4iとP5iを追加するか、または極小論理に公理P5iを追加することで実現されます。P4iとP5iはどちらも古典的な命題論理の定理です。

P4i。${\displaystyle \left(\phi \to \lnot \phi \right)\to \lnot \phi }$

P5i。${\displaystyle \lnot \phi \to \left(\phi \to \psi \right)}$

これらは公理スキーマであり、公理の無限に多くの具体的なインスタンスを表すことに注意してください。例えば、P1 は特定の公理インスタンス を表す場合もあれば、 を表す場合もあります。 は任意の式を配置できる場所です。このように式をまたぐ変数は「スキーマ変数」と呼ばれます。 ${\displaystyle p\to p}$ ${\displaystyle \left(p\to q\right)\to \left(p\to q\right)}$ ${\displaystyle \phi }$

均一置換（US）の第二規則を用いることで、これらの公理スキームをそれぞれ単一の公理に変換し、各図式変数をどの公理にも記載されていない命題変数に置き換えることで、いわゆる置換公理化を実現できます。どちらの形式化も変数を使用しますが、単一規則公理化では論理言語の外部にある図式変数を使用するのに対し、置換公理化では、置換を用いた規則を用いて式をまたぐ変数の概念を表現することで、同じ機能を果たす命題変数を使用します。

米国。を命題変数 を1つ以上含む式とし、 を別の式とします。そして、 から を推論します。${\displaystyle \phi (p)}$ ${\displaystyle p}$ ${\displaystyle \psi }$ ${\displaystyle \phi (p)}$ ${\displaystyle \phi (\psi )}$

次の 3 つの論理公理スキーマは、全称量指定子を追加、操作、および削除する方法を提供します。

Q5.ここでtはxの代わりに使用できる。${\displaystyle \forall x\left(\phi \right)\to \phi [x:=t]}$ ${\displaystyle \,\!\phi }$

質問6.${\displaystyle \forall x\left(\phi \to \psi \right)\to \left(\forall x\left(\phi \right)\to \forall x\left(\psi \right)\right)}$

Q7.ここで、x はでは自由ではありません。${\displaystyle \phi \to \forall x\left(\phi \right)}$ ${\displaystyle \phi }$

これらの3つの追加規則は、命題論理体系を拡張して古典的な述語論理を公理化する。同様に、これらの3つの規則は、直観主義命題論理（P1-3、P4i、P5iを含む）の体系を直観主義述語論理に拡張する。

全称量化には、追加の一般化規則を使用した代替公理化が与えられることが多く、その場合、規則 Q6 と Q7 は冗長になります。

• 一般化:およびx がのどの式にも出現しない場合は となります。${\displaystyle \Gamma \vdash \phi }$ ${\displaystyle \Gamma }$ ${\displaystyle \Gamma \vdash \forall x\phi }$

最終的な公理スキーマは、等号記号を含む数式を処理するために必要です。

I8.すべての変数xについて。${\displaystyle x=x}$

19.${\displaystyle \left(x=y\right)\to \left(\phi [z:=x]\to \phi [z:=y]\right)}$

保守的な拡張

ヒルベルト体系には、関数の完全性に向けて、論理演算子である含意と否定の公理のみを含めるのが一般的です。これらの公理が与えられれば、追加の接続詞の使用を許可する演繹定理の保守的な拡張を形成することができます。これらの拡張が保守的と呼ばれるのは、新しい接続詞を含む式 φ を、否定、含意、全称量化のみを含む論理的に同値な式 θ に書き直すと、拡張された体系で φ が導出可能であることと、元の体系で θ が導出可能であることが等しいためです。完全に拡張されたヒルベルト体系は、自然演繹の体系により近くなります。

存在量化

• 導入

${\displaystyle \forall x(\phi \to \exists y(\phi [x:=y]))}$

• 排除

${\displaystyle \forall x(\phi \to \psi )\to \exists x(\phi )\to \psi }$ ここで はの自由変数ではありません。${\displaystyle x}$ ${\displaystyle \psi }$

連言と選言

• 接続詞の導入と除去

導入：${\displaystyle \alpha \to (\beta \to \alpha \land \beta )}$

残り排除数:${\displaystyle \alpha \wedge \beta \to \alpha }$

排除権：${\displaystyle \alpha \wedge \beta \to \beta }$

• 選言の導入と除去

紹介左：${\displaystyle \alpha \to \alpha \vee \beta }$

紹介権：${\displaystyle \beta \to \alpha \vee \beta }$

除去：${\displaystyle (\alpha \to \gamma )\to ((\beta \to \gamma )\to \alpha \vee \beta \to \gamma )}$

参照

• ヒルベルト系の一覧
• 自然演繹
• シーケント計算

注記

1. Máté & Ruzsa 1997:129より
2. スミス、ピーター (2013-02-21). ゲーデルの定理入門. ケンブリッジ大学出版局. p. 10. ISBN 978-1-107-02284-3。
3. レストール、グレッグ (2002-09-11). 部分構造論理入門. ラウトレッジ. pp.  73– 74. ISBN 978-1-135-11131-1。
4. Gaifman, Haim (2002). 「文論理、完全性、コンパクト性のためのヒルベルト型演繹システム」(PDF) .コロンビア. 2024年8月19日閲覧。
5. 、グプタ、アミタバ、パリク、ロヒット（2011年4月2日）。『証明、計算、そしてエージェンシー：岐路に立つ論理』シュプリンガー・サイエンス＆ビジネス・メディア、p. 41。ISBN 978-94-007-0080-2。
6. ベーコン、アンドリュー (2023-09-29). 高階論理への哲学的入門. テイラー＆フランシス. p. 424. ISBN 978-1-000-92575-3。
7. エイク、ヤン・ヴァン (1991-02-26) AI のロジック: 欧州ワークショップ JELIA '90、オランダ、アムステルダム、1990 年 9 月 10 ～ 14 日。議事録。シュプリンガーのサイエンス＆ビジネスメディア。 p. 113.ISBN​ 978-3-540-53686-4。
8. ハック、スーザン（1978年7月27日）『論理の哲学』ケンブリッジ大学出版局、19頁。ISBN 978-0-521-29329-7。
9. ボストック、デイヴィッド (1997). 『中間論理学』 オックスフォード：ニューヨーク：クラレンドン・プレス；オックスフォード大学出版局. pp.  4– 5, 8– 13, 18– 19, 22, 27, 29, 191, 194. ISBN 978-0-19-875141-0。
10. ルーカス・JR (2018年10月10日). 『時間と空間に関する論文』ラウトレッジ. p. 152. ISBN 978-0-429-68517-0。
11. Troelstra, AS; Schwichtenberg, H. (2000). 基礎証明理論. Cambridge Tracts in Theoretical Computer Science (第2版). Cambridge: Cambridge University Press. p. 51. doi :10.1017/cbo9781139168717. ISBN 978-0-521-77911-1。
12. 「論理学入門 - 第4章」intrologic.stanford.edu . 2024年8月16日閲覧。
13. Buss, SR (1998-07-09). 証明理論ハンドブック. エルゼビア. pp.  552– 553. ISBN 978-0-08-053318-6。
14. 小野 宏明 (2019-08-02). 証明論と論理における代数. シュプリンガー. p. 5. ISBN 978-981-13-7997-0。
15. エイク、ヤン・ヴァン (1991-02-26) AI のロジック: 欧州ワークショップ JELIA '90、オランダ、アムステルダム、1990 年 9 月 10 ～ 14 日。議事録。シュプリンガーのサイエンス＆ビジネスメディア。 p. 113.ISBN​ 978-3-540-53686-4。
16. ガベイ, ドヴ・M.; ゲントナー, フランツ (2013-03-14). 哲学論理ハンドブック. シュプリンガー・サイエンス＆ビジネス・メディア. p. 201. ISBN 978-94-017-0458-8。
17. スムリアン、レイモンド・M. (2014-07-23). 数学論理入門. クーリエ社. pp.  102– 103. ISBN 978-0-486-49237-7。
18. Franks, Curtis (2023)、「Propositional Logic」、Zalta, Edward N.、Nodelman, Uri (eds.)、The Stanford Encyclopedia of Philosophy (Fall 2023 ed.)、Metaphysics Research Lab、Stanford University 、 2024年3月22日閲覧。
19. メンデルソン, リチャード・L. (2005-01-10). ゴットロープ・フレーゲの哲学. ケンブリッジ大学出版局. p. 185. ISBN 978-1-139-44403-3。
20. Łukasiewicz、1 月 (1970)。ヤン・ルカシェヴィチ: 厳選作品。北オランダ。 p. 136.
21. チャーチ、アロンゾ (1996). 数理論理学入門. プリンストン大学出版局. p. 119. ISBN 978-0-691-02906-1。
22. "Proof Explorer - Home Page - Metamath". us.metamath.org . 2024年7月2日閲覧。
23. クック, スティーブン A.; レックハウ, ロバート A. (1979). 「命題証明システムの相対的効率」 .シンボリックロジックジャーナル. 44 (1): 39. doi :10.2307/2273702. ISSN  0022-4812. JSTOR  2273702.
24. Walicki, Michał (2017).数理論理学入門（拡張版）. ニュージャージー州: World Scientific. p. 126. ISBN 978-981-4719-95-7。
25. パドラック, パベル; バス, サミュエル R. (1995). 「（簡単に）有罪判決を受けずに嘘をつく方法と命題計算における証明の長さ」. パコルスキ, レシェク; ティウリン, イェジ (編).コンピュータサイエンス・ロジック. コンピュータサイエンス講義ノート. 第933巻. ベルリン, ハイデルベルク: シュプリンガー. p. 152. doi :10.1007/BFb0022253. ISBN 978-3-540-49404-1。

参考文献

• カリー、ハスケル・B.; ロバート・フェイズ (1958).組合せ論理学 第1巻. アムステルダム: 北ホラント.
• モンク、J. ドナルド (1976). 『数学論理学』 . 大学院数学テキスト. ベルリン、ニューヨーク:シュプリンガー・フェアラーク. ISBN 978-0-387-90170-1。
• ルザ、イムレ。マテ、アンドラス (1997)。Bevezetés は現代のロジカバ(ハンガリー語)。ブダペスト：オシリス・キアド。
• タルスキー、アルフレッド (1990)。Bizonyítás és igazság (ハンガリー語)。ブダペスト：ゴンドラ。これは、アルフレッド・タルスキの真理の意味理論に関する選集のハンガリー語訳です。
• デイヴィッド・ヒルベルト（1927）『数学の基礎』、ステファン・バウアー＝メングラーベルグとダグフィン・フォルレスダール訳（pp. 464–479）。
  • ファン・ヘイエノールト、ジャン（1967年）『フレーゲからゲーデルまで：1879年から1931年までの数理論理学の原典』（1976年第3刷）ケンブリッジ、マサチューセッツ州：ハーバード大学出版局。ISBN 0-674-32449-8。
  • ヒルベルトの 1927 年の著書『基礎』は、1925 年の以前の「基礎」講義 (367 ～ 392 ページ) に基づいており、彼の 17 個の公理 (含意の公理 #1 ～ #4、& と V に関する公理 #5 ～ #10、否定の公理 #11 ～ #12、論理的 ε 公理 #13、等式の公理 #14 ～ #15、数の公理 #16 ～ #17) を、彼の形式主義「証明理論」のその他の必要な要素 (帰納法公理、再帰公理など) とともに提示しています。また、彼は LEJ ブラウワーの直観主義に対しても精力的に反論しています。 Hermann Weyl (1927) のコメントと反論 (pp. 480–484)、Paul Bernay (1927) のヒルベルトの講義への付録 (pp. 485–489)、および Luitzen Egbertus Jan Brouwer (1927) の応答 (pp. 490–495) も参照してください。
• クリーネ、スティーブン・コール (1952). 『メタ数学入門』（1971年訂正版第10刷）アムステルダム、ニューヨーク州: ノースホランド出版社. ISBN 0-7204-2103-9。
  • 特に第 IV 章形式システム (pp. 69–85) を参照してください。この章で、Kleene はサブチャプター §16 形式記号、§17 形成規則、§18 自由変数と束縛変数 (置換を含む)、§19 変換規則 (例: 可能法) を提示しています。また、これらから 21 の「公理」を提示しています。これは、18 の公理と 3 つの「即時帰結」関係で、次のように分類されます。命題計算の公理 #1-8、述語計算の追加公理 #9-12、および数論の追加公理 #13-21。

外部リンク

• ガイフマン、ハイム。「文論理、完全性、コンパクト性のためのヒルベルト型演繹システム」（PDF）。
• Farmer, WM「命題論理」（PDF）。これは、（とりわけ）特定のヒルベルトスタイルの証明システム（命題計算に限定される）について説明します。