Let K be a finite functionally complete set of Boolean connectives, and consider propositional formulas built from variables p0, p1, p2,... using K-connectives. A Frege rule is an inference rule of the form where B1,..., Bn, B are formulas. If R is a finite set of Frege rules, then F = defines a derivation system in the following way. If X is a set of formulas, and A is a formula, then an F-derivation of A from axioms X is a sequence of formulas A1,..., Am such that Am = A, and every Ak is a member of X, or it is derived from some of the formulas Ai, i < k, by a substitution instance of a rule from R. An F-proof of a formula A is an F-derivation of A from the empty set of axioms. F is called a Frege system if
F is sound: every F-provable formula is a tautology.
F is implicationally complete: for every formula A and a set of formulas X, if X entails A, then there is an F-derivation of A from X.
The length in a proofA1,..., Am is m. The size of the proof is the total number of symbols. A derivation system F as above is refutationally complete, if for every inconsistent set of formulas X, there is an F-derivation of a fixed contradiction from X.
Resolution is not a Frege system because it only operates on clauses, not on formulas built in an arbitrary way by a functionally complete set of connectives. Moreover, it is not implicationally complete, i.e. we cannot conclude from. However, adding the weakening rule: makes it implicationally complete. Resolution is also refutationally complete.
Properties
Reckhow's theorem states that all Frege systems are p-equivalent.
Frege systems are considered to be fairly strong systems. Unlike, say, resolution, there are no known superlinear lower bounds on the number of lines in Frege proofs, and the best known lower bounds on the size of the proofs are quadratic.
The minimal number of rounds in the prover-adversary game needed to prove a tautology is proportional to the logarithm of the minimal number of steps in a Frege proof of.
An important extension of a Frege system, the so called Extended Frege, is defined by taking a Frege system F and adding an extra derivation rule which allows to derive formula, where abbreviates its definition in the language of the particular F and the atom does not occur in previously derived formulas including axioms and in the formula. The purpose of the new derivation rule is to introduce 'names' or shortcuts for arbitrary formulas. It allows to interpret proofs in Extended Frege as Frege proofs operating with circuits instead of formulas. Cook's correspondence allows to interpret Extended Frege as a nonuniform equivalent of Cook's theory PV and Buss's theory formalizing feasible reasoning.
