ヒルベルトシステム

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

これは、公理と推論規則から定理を生成する演繹システムとして定義されます。^{[3] [4] [5]}特に、唯一の推論規則が可能性法である場合。^{[6] [7]}すべてのヒルベルトシステムは公理システムであり、多くの著者がヒルベルトシステムを宣言するための唯一のより特定的でない用語として使用します。 ^{[8] [9] [10]より具体的な用語に言及する必要はありません。 この文脈では、「ヒルベルトシステム」は、公理を使用せず、推論規則のみを使用する}自然演繹システムと対比されます。 ^[3]

「公理的」な論理証明システムについて言及しているすべての情報源は、それを単に公理を伴う論理証明システムと特徴づけているが、「ヒルベルトシステム」という用語の変形を使用する情報源は、それを異なる方法で定義することがあり、この記事では使用しない。たとえば、トロルストラは「ヒルベルトシステム」を、公理を持ち、およびを唯一の推論規則とするシステムと定義している。 ^[11]特定の公理のセットは、「ヒルベルトシステム」^[12]または「ヒルベルトスタイルの計算」[ ^{13] と呼ばれることもある。[ 2 ] 「ヒルベルトスタイル」は、以下の P2 の § 概略形式のように、公理が}図式的形式で与えられるタイプの公理システムを表すために使用されることがあるが、他の情報源は、図式的公理を伴うシステムと置換規則を伴うシステムの両方を包含するものとして「ヒルベルトスタイル」という用語を使用している。 ^[14]この記事も同様である。論理学における公理的証明システムを説明するために「ヒルベルト式」や類似の用語が使用されるようになったのは、ヒルベルトとアッカーマンの『数理論理学の原理』 （1928年）の影響によるものである。^[2]${\displaystyle {\rightarrow }E}$${\displaystyle {\forall }I}$

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

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

ヒルベルト体系では、形式的演繹（または証明）は、各式が公理であるか、または推論規則によって前の式から得られる式の有限のシーケンスです。これらの形式的演繹は、自然言語の証明を反映することを目的としていますが、はるかに詳細です。

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

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

以下は命題論理で使用されているヒルベルト システムの一部です。そのうちの 1 つである P2 の § 図式形式は、フレーゲ システムとも考えられています。

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

• 命題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}$

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

ヤン・ウカシェヴィチは、フレーゲの体系では「3番目の公理は前の2つの公理から導き出せるので不要であり、最後の3つの公理は「」という1つの文に置き換えることができる」ことを示した。^{[23]これは、ウカシェヴィチの}ポーランド語表記法から現代の表記法に置き換えると、次のようになる。したがって、ウカシェヴィチは^[20]この3つの公理の体系の考案者とされている。 ${\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)}$

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

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

• ${\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}の概略版はジョン・フォン・ノイマンに帰属し、^[20] Metamathの「set.mm」形式証明データベースで使用されています。 ^[25]実際、置換規則を公理スキーマで置き換えるというアイデア自体がフォン・ノイマンに帰属しています。^{[26] P} ₂の概略版はヒルベルトにも帰属し、この文脈で命名されました。^[27]${\displaystyle {\mathcal {H}}}$

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

例として、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)}$       （（１）と（２）から、モーダスポネンスによる）
4. ${\displaystyle A\to (B\to A)}$       （（A1）の例）
5. ${\displaystyle A\to A}$       （（4）と（3）から、モーダスポネンスによる）

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

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

1.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(\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、および modus ponens から導かれるため冗長です (証明を参照)。これらの公理は古典的な命題論理を記述します。公理 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 }$

2 番目の均一置換規則 (US) を使用すると、これらの公理スキーマをそれぞれ単一の公理に変更し、各図式変数をどの公理にも記載されていない命題変数に置き換えて、置換公理化と呼ばれるものを得ることができます。どちらの形式化にも変数がありますが、1 つの規則の公理化にはロジックの言語外にある図式変数があるのに対し、置換公理化では、置換を使用する規則を使用して式にまたがる変数の概念を表現することで同じ機能を果たす命題変数を使用します。

を命題変数 の 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 }$

Q6.${\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 は冗長になります。

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

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 )}$

ヒルベルト システムには演繹規則がほとんどないため、新しい演繹規則を使用した演繹は、元の演繹規則のみを使用した演繹に変換できるという意味で、追加の演繹規則によって演繹力が追加されないことを示すメタ定理を証明することが一般的です 。

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

• カリー、ハスケル B.、ロバート フェイズ (1958)。組合せ論理第 I 巻、第 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 年の「基礎」講義 (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 章形式システム (69 ～ 85 ページ) を参照してください。この章で、Kleene はサブチャプター §16 形式記号、§17 形成規則、§18 自由変数と束縛変数 (置換を含む)、§19 変換規則 (例: 可能法) を提示し、これらから 21 の「公理」を提示しています。これは 18 の公理と 3 つの「即時帰結」関係で、次のように分類されます。命題計算の公理 #1 ～ 8、述語計算の追加公理 #9 ～ 12、および数論の追加公理 #13 ～ 21。

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