弗雷格系统

在证明复杂性中，弗雷格系统是一个命题证明系统，其证明是使用有限的健全和隐含完整的推理规则得出的公式序列。弗雷格系统（在一般证明理论中更多地被称为希尔伯特系统）是以戈特洛夫-弗雷格命名的。

让K是一个有限的功能完整的布尔连接词集，并考虑使用K连接词从变量p0,p1,p2,...建立命题公式。弗雷格规则是一个推理规则，其形式为其中B1，...，Bn，B是公式。如果R是一个有限的弗雷格规则集，那么F=(K,R)以如下方式定义了一个推导系统。

如果X是一个公式集，A是一个公式，那么从公理X出发的A的F派生是一个公式A1，...，Am的序列，使得Am=A，并且每个Ak都是X的成员，或者它是通过R的规则的替换实例从一些公式Ai，i<k派生的。

在下列情况下，F被称为弗雷格系统F是健全的：每一个F证明的公式都是同义反复。F是隐含完整的：对于每一个公式A和一组公式X，如果X包含A，那么就有一个来自X的A的F衍生。

如果对于每一个不一致的公式集X，都有一个来自X的固定矛盾的F派生系统，那么上述派生系统F就是反驳完整的。

弗雷格的命题微积分是一个弗雷格系统。在命题微积分网页上有许多健全的弗雷格规则的例子。解析不是一个弗雷格系统，因为它只在子句上操作，而不是在由功能完整的连接词集以任意方式建立的公式上。此外，它不是隐含完整的，也就是说，我们不能得出A∨B特性Reckhow定理(1979)指出，所有弗雷格系统都是p等价的。

自然演绎和顺序计算(Gentzensystemwithcut)也是p等价于弗雷格系统的。有多项式的弗雷格证明鸽子洞原理(Buss1987)。弗雷格系统被认为是相当强大的系统。

与决议不同的是，在弗雷格证明的行数上没有已知的超线性下限，而已知的关于证明大小的最佳下限是二次的。证明者-反驳者游戏中证明同义词j所需的最小回合数{displaystyle/phi}所需的最小回合数与对数成正比。

弗雷格系统的一个重要扩展，即所谓的扩展的弗雷格，是通过对弗雷格系统F的定义，并增加一个额外的推导规则，允许推导出公式新推导规则的目的是为任意公式引入"名称"或捷径。

它允许将扩展弗雷格的证明解释为用电路而不是公式操作的弗雷格证明。

库克的对应关系允许将扩展弗雷格解释为库克理论PV和Buss理论的非统一等价物{displaystyleS_{2}{1}}将可行的（多项式）形式化。将可行的（多项式时间）推理形式化。