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 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 = (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 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 (X=∅). 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 (number of lines) in a proof A1, ..., 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. Examples Frege's propositional calculus is a Frege system. There are many examples of sound Frege rules on the Propositional calculus page. 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 (1979) states that all Frege systems are p-equivalent. Natural deduction and sequent calculus (Gentzen system with cut) are also p-equivalent to Frege systems. There are polynomial-size Frege proofs of the pigeonhole principle (Buss 1987). Frege systems are considered