ヒルベルト系

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

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

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

ヒルベルトシステムのほとんどの変種は、論理公理と推論規則のトレードオフのバランスの取り方において特徴的なアプローチをとっている。^{[ 1 ] [ 6 ] [ 15 ] [ 11 ]}ヒルベルトシステムは、多数の論理公理のスキーマと少数の推論規則の選択によって特徴づけられる。自然演繹システムは、多くの演繹規則を含むが、公理スキーマは非常に少ないかまったくないという、反対のアプローチをとる。^{[ 3 ]}最もよく研​​究されているヒルベルトシステムは、命題論理の場合はモーダス・ポネンスという推論規則が1つだけ、または述語論理も扱うための一般化付きの推論規則が2つ、そしていくつかの無限の公理スキーマを持つ。真理様相論理のヒルベルトシステムは、ヒルベルト・ルイスシステムと呼ばれることもあり、さらに必然規則を必要とする。一部のシステムでは、公理図式による無限の数式の代わりに、有限個の具体的な数式を公理として使用しており、その場合は一様置換規則が必要となる。^{[ 14 ]}    

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

ヒルベルト体系では、形式的演繹（または証明）は、各式が公理であるか、または推論規則によって前の式から得られる有限個の式の列である。^{[ 17 ]}これらの形式的演繹は、自然言語の証明を模倣することを意図しているが、はるかに詳細である。^{[ 18 ]}

仮定する${\displaystyle \Gamma }$は、仮説とみなされる一連の式です。例えば、${\displaystyle \Gamma }$群論または集合論の公理の集合である可能性がある。表記法${\displaystyle \Gamma \vdash \phi }$控除が終わることを意味します${\displaystyle \phi }$論理公理と要素のみを公理として使用する${\displaystyle \Gamma }$[ ^{19 ]したがって、非公式には}、${\displaystyle \Gamma \vdash \phi }$つまり${\displaystyle \phi }$すべての式を仮定すると、証明可能である。${\displaystyle \Gamma }$。

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

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

述語論理の公理化は無数に存在します。なぜなら、どのような論理においても、その論理を特徴づける公理と規則を選択する自由度があるからです。ここでは、9 つ​​の公理と規則モーダスポネンスのみを持つヒルベルト体系について説明します。これを「1 規則公理化」と呼び、古典的な等式論理を記述します。この論理のための最小限の言語を扱います。この言語では、論理式は結合子のみを使用します。${\displaystyle \lnot }$そして${\displaystyle \to }$そして量化子のみ${\displaystyle \forall }$後ほど、このシステムを拡張して、次のような追加の論理結合子を含める方法を示します。${\displaystyle \land }$そして${\displaystyle \lor }$演繹可能な公式の範囲を拡大することなく。

最初の4つの論理公理図式は、（モーダス・ポネンスとともに）論理結合子の操作を可能にする。

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 }$は、任意の数式を配置できる場所です。このように数式の範囲を持つ変数は、「スキーマ変数」と呼ばれます。

2つ目の規則である一様置換（US）を用いることで、これらの公理図式をそれぞれ単一の公理に変換し、各図式変数をどの公理にも言及されていない命題変数に置き換えることで、置換公理化と呼ばれるものを得ることができます。どちらの形式化にも変数がありますが、1規則公理化では論理言語の外にある図式変数が用いられるのに対し、置換公理化では、置換を用いる規則によって式の範囲を表す変数の概念を表現することで同じ働きをする命題変数を用います。

私たちに。${\displaystyle \phi (p)}$命題変数のインスタンスを1つ以上含む式である${\displaystyle p}$、そして${\displaystyle \psi }$別の公式とする。${\displaystyle \phi (p)}$推論する${\displaystyle \phi (\psi )}$。

次の３つの論理公理図式は、全称量化子を追加、操作、削除する方法を提供する。

Q5.${\displaystyle \forall x\left(\phi \right)\to \phi [x:=t]}$ここで、t はxの代わりに使用できます。${\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.${\displaystyle \phi \to \forall x\left(\phi \right)}$ここでxは自由ではない${\displaystyle \phi }$。

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

全称量化は、追加の一般化規則を用いた別の公理化が与えられることが多く、その場合、規則Q6とQ7は冗長となる。

• 一般化：もし${\displaystyle \Gamma \vdash \phi }$また、x はどの式にも単独では現れない。${\displaystyle \Gamma }$それから${\displaystyle \Gamma \vdash \forall x\phi }$。

最終的な公理スキーマは、等号を含む数式を扱うために必要となる。

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

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

ヒルベルト体系では、機能的完全性を目指して、論理演算子である含意と否定の公理のみを含めるのが一般的です。これらの公理が与えられれば、追加の論理結合子の使用を可能にする演繹定理の保守的な拡張を形成することができます。これらの拡張は、新しい論理結合子を含む式 φ を、否定、含意、および全称量化のみを含む論理的に同値な式 θ に書き換えた場合、拡張された体系で φ が導出可能であるのは、元の体系で θ が導出可能な場合に限るという理由から、保守的と呼ばれます。完全に拡張されたヒルベルト体系は、自然演繹体系により近いものになります。

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

• カリー、ハスケル B.、ロバート フェイズ (1958)。組み合わせ論理学 第 1巻。 アムステルダム: ノース ホランド。
• モンク、J.ドナルド（1976）。数理論理学。大学院数学テキスト。ベルリン、ニューヨーク：シュプリンガー・フェルラーク。ISBN 978-0-387-90170-1。
• ルザ、イムレ。マテ、アンドラス (1997)。Bevezetés は現代のロジカバ(ハンガリー語)。ブダペスト：オシリス・キアド。
• タルスキー、アルフレッド (1990)。Bizonyítás és igazság (ハンガリー語)。ブダペスト：ゴンドラ。これは、アルフレッド・タルスキによる真理の意味論に関する選集をハンガリー語に翻訳したものである。
• デイヴィッド・ヒルベルト（1927）「数学の基礎」、ステファン・バウアー＝メングラーベルクおよびダグフィン・フォレスダル訳（ 464 ～ 479頁）。
  • ファン・ヘイエノールト、ジャン（1967）。『フレーゲからゲーデルへ：数学論理学の資料集、1879年～ 1931年』（第3刷、1976年 版）。マサチューセッツ州ケンブリッジ：ハーバード大学出版局。ISBN 0-674-32449-8。
  • ヒルベルトの1927年の著作は、1925年の「基礎」講義（ 367 ～ 392ページ）に基づいており、含意の公理1～4、&とVに関する公理5～10、否定の公理11～12、論理ε公理13、等号の公理14～15、数の公理16～17といった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。{{cite book}}ISBN /日付の不一致（ヘルプ）
  • 特に第 IV 章「形式体系」（ 69 ～ 85 ページ）を参照のこと。そこでは、クリーネは、§16 形式記号、§17 形成規則、§18 自由変数と束縛変数（置換を含む）、§19 変換規則（例えば、モーダス・ポネンス）という小節を提示し、これらから 21 の「公理」を提示している。18 の公理と 3 の「直接的結果」関係は、次のように分類される。命題論理の公理 #1-8、述語論理の追加公理 #9-12、数論の追加公理 #13-21。

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