において、フレーゲ系（フレーゲけい、）とは、健全かつ含意完全な有限個の推論規則の集合を用いて導出される論理式の列を証明とする命題証明系である。フレーゲ系は（一般の証明論ではとしてより広く知られている）、ゴットロープ・フレーゲにちなんで名付けられている。
「フレーゲ系」という名称は、スティーヴン・クックとロバート・レックホウによって初めて定義され、最も一般的な命題証明系の性質を捉えることを意図していた。
形式的定義 クックとレックホウは、フレーゲ系についての最初の形式的定義を与えたが、以下に示す、クライチェクに基づく定義はそれと同値である。
K をブール結合子の有限な関数完全な集合とし、変数 p0, p1, p2, ... から K-結合子を用いて構成される論理式を考える。フレーゲ規則とは、次の形式の推論規則である。
ここで B1, ..., Bn, B は論理式である。R がフレーゲ規則の有限集合であるとき、F = (K,R) は次のようにして導出体系を定義する。X を論理式の集合、A を論理式とするとき、公理 X からの A の F-導出とは、論理式の列 A1, ..., Am であって、Am = A であり、かつすべての Ak が X の要素であるか、あるいは i < k であるいくつかの論理式 Ai から、R に属するある規則の代入事例によって導出されるものである。論理式 A の F-証明とは、空の公理集合（X=∅）からの A の F-導出のことである。F が次を満たすとき、F はフレーゲ系と呼ばれる。 F は健全である。すなわち、F-証明可能なすべての論理式はトートロジーである。 F は含意完全である。すなわち、任意の論理式 A と論理式の集合 X について、X が A を含意するならば、X からの A の F-導出が存在する。 証明 A1, ..., Am の長さ（行数）は m である。証明の大きさは、記号の総数である。
上記のような導出体系 F は、任意の矛盾する論理式の集合 X について、X からのある固定した矛盾の F-導出が存在するとき、反駁完全であるという。
例 フレーゲの命題計算は、公理図式ではなく公理を用いていたため、フレーゲ系ではない。ただし、フレーゲ系となるように修正することは可能である。 命題論理のページには、健全なフレーゲ規則の例が数多く掲載されている。 導出原理は、関数完全な結合子の集合によって任意の仕方で構成される論理式に対してではなく、節に対してのみ作用するため、フレーゲ系ではない。さらに、導出原理は含意完全でもない。すなわち、 から を結論することができない。しかし、弱化規則 を加えることで含意完全にすることができる。導出原理はまた反駁完全でもある。
性質 レックホウの1979年の定理は、すべてのフレーゲ系がp同値であることを述べている。 自然演繹と（切除を伴うゲンツェン体系である）シークエント計算も、フレーゲ系とp同値である。 鳩の巣原理には多項式サイズのフレーゲ証明が存在する。 フレーゲ系はかなり強力な体系であると考えられている。例えば導出原理とは異なり、フレーゲ証明の行数について既知の超線形下界は存在せず、証明の大きさについて既知の最良の下界は二次関数的なものである。 あるトートロジー を証明するために必要な証明者対敵対者ゲームにおける最小のラウンド数は、 のフレーゲ証明における最小のステップ数の対数に比例する。
拡張フレーゲ系 クックとレックホウはまた、フレーゲ系の拡張である拡張フレーゲを定義した。これは、フレーゲ系 F を取り、論理式 を導出することを可能にする追加の導出規則を加えるものである。ここで は特定の F の言語におけるその定義を略記したものであり、アトム は、公理を含めそれまでに導出された論理式や、論理式 の中には出現しない。
この新しい導出規則の目的は、任意の論理式に対して「名前」あるいは省略形を導入することである。これにより、拡張フレーゲにおける証明を、論理式ではなく論理回路を用いて操作するフレーゲ証明として解釈することが可能になる。
クックの対応により、拡張フレーゲを、実行可能な（多項式時間の）推論を形式化するクックの理論PVおよびバスの理論 の非一様な等価物として解釈することができる。
出典