# 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 p0, p1, p2, ... using K-connectives. A Frege rule is an inference rule of the form

$r={\frac {B_{1},\dots ,B_{n}}{B}},$ 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=\varnothing$ ). 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 contradition from X.