Frege system
In proof complexity, a Frege system is a propositional proof system whose proofs are sequences of formulas derived using a finite set of sound and implicationally complete inference rules. Frege systems (more often known as Hilbert systems in general proof theory) are named after Gottlob Frege. Formal definition. Let "K" be a finite functionally complete set of Boolean connectives, and consider propositional formulas built from variables "p", "p", "p", ... using "K"-connectives. A Frege rule is an inference rule of the form where "B", ..., "B", "B" are formulas. If "R" is a finite set of Frege rules, then "F  = (K","R") 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 "A", ..., "A" such that "A" = "A", and every "A" is a member of "X", or it is derived from some of the formulas "A", "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 (X=∅). "F" is called a Frege system if The length (number  of lines) in a proof "A", ..., "A" 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". Extended Frege system. 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 formula_7, where formula_8 abbreviates its definition in the language of the particular "F" and the atom formula_9 does not  occur in previously derived formulas including axioms and in the formula formula_10. 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 formula_11 formalizing feasible (polynomial-time) reasoning.