[2] Cook and Reckhow[3][4] gave the first[2] formal definition of a Frege system, to which the one below, based on Krajicek,[1] is equivalent.
Let K be a finite functionally complete set of Boolean connectives, and consider propositional formulas built from variables p0, p1, p2, ... using K-connectives.
If R is a finite set of Frege rules, then F = (K,R) defines a derivation system in the following way.
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. Cook and Reckhow also defined an extension of a Frege system, called Extended Frege,[4] which takes a Frege system F and adds an extra derivation rule which allows one to derive a formula
The purpose of the new derivation rule is to introduce 'names' or shortcuts for arbitrary formulas.