フレーゲシステム

証明の複雑さにおいて、フレーゲ系は命題証明システムであり、その証明は健全かつ含意的に完全な推論規則の有限集合を使用して導出された式の列である。^{[1]フレーゲ系（一般的な}証明理論ではヒルベルト系としてよく知られている）はゴットロープ・フレーゲにちなんで名付けられている。

「フレーゲシステム」という名前は、スティーブン・クックとロバート・レックハウによって最初に定義され^{[2] 、 [3] [4]}、最も一般的な命題証明システムの特性を捉えることを目的としていました。^[2]

クックとレックハウ^{[3] [4]は}フレーゲシステムの最初の^{[2]正式な定義を与えたが、クライチェク[1]}に基づく以下の定義はそれと同等である。

Kをブール接続子の有限関数的完全集合とし、 K接続子を使用して変数p ₀、p ₁、p ₂、...から構築された命題式を考える。フレーゲ規則は、次の形式の推論規則である。

${\displaystyle r={\frac {B_{1},\dots ,B_{n}}{B}},}$

ここで、B ₁、...、B _n、Bは式である。R がフレーゲ規則の有限集合である場合、F = ( K、R ) は次のように導出システムを定義する。Xが式の集合でA が式である場合、公理XからのAのF導出は、 A _m  =  Aであり、すべてのA _{k が}Xのメンバーであるような式A ₁、...、A _mの列であるか、またはRからの規則の置換インスタンスによって式A _i、i  <  kの一部から導出される。式AのF証明は、空公理集合 (X=∅) からのAのF導出である。 F は、次の場合、フレーゲシステムと呼ばれる。

• Fは正しい: Fで証明可能なすべての式はトートロジーである。
• F は含意的に完全です。つまり、すべての式Aと式の集合Xに対して、X がA を含意する場合、XからAのF導出が存在します。

証明A ₁、...、A _mの長さ（行数）はmです。証明のサイズは記号の総数です。

上記の導出システムFは、矛盾する式のセットXごとに、 Xから固定された矛盾のF導出が存在する場合、反証的に完全です。

• フレーゲの命題計算は、公理体系の代わりに公理を使用しているため、フレーゲ体系ではないが、フレーゲ体系になるように修正することは可能である。^[4]
• 命題計算のページには、健全なフレーゲ規則の例が多数あります。
• 解決はフレーゲシステムではありません。なぜなら、解決は節のみに作用し、機能的に完全な接続子のセットによって任意の方法で構築された式には作用しないからです。さらに、解決は含意的に完全ではありません。つまり、から結論付けることはできません。ただし、弱める規則を追加すると、解決は含意的に完全になります^[要出典]。解決は反駁的にも完全です。${\displaystyle A\or B}$${\displaystyle A}$${\displaystyle {\frac {A}{A\lor B}}}$

• 1979年のレックハウの定理^[4]は、すべてのフレーゲ系はp-同値であると述べている。
• 自然演繹とシーケント計算（カット付きゲンツェンシステム）もフレーゲシステムと p 同値です。
• 鳩の巣原理には多項式サイズのフレーゲ証明がある。^[5]
• フレーゲ システムはかなり強力なシステムであると考えられています。たとえば、解像度とは異なり、フレーゲ証明の行数に関する超線形下限は知られておらず、証明のサイズに関する最もよく知られている下限は 2 次です。
• トートロジーを証明するために必要な証明者-敵対者ゲームにおける最小ラウンド数は、のフレーゲ証明における最小ステップ数の対数に比例します。${\displaystyle \phi}$${\displaystyle \phi}$

• 
  さまざまなシステムの証明の強さ。

クックとレックハウは、拡張フレーゲ^[4]と呼ばれるフレーゲ系の拡張も定義しました。これは、フレーゲ系Fを取り、式 を導出することを可能にする追加の導出規則を追加します。ここで、 は特定のFの言語での定義を省略し、原子 は、公理や式 を含む以前に導出された式には出現しません。 ${\displaystyle p\leftrightarrow D}$${\displaystyle \leftrightarrow}$${\displaystyle p}$${\displaystyle D}$

新しい導出規則の目的は、任意の式に「名前」またはショートカットを導入することです。これにより、拡張フレーゲの証明を、式ではなく 回路で動作するフレーゲの証明として解釈できるようになります。

クックの対応により、拡張フレーゲを、実行可能な（多項式時間）推論を形式化する クックの理論 PV とバスの理論の非一様等価物として解釈することができます。${\displaystyle S_{2}^{1}}$