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

${\displaystyle 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 (${\displaystyle 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.

References

• Krajíček, Jan (1995). "Bounded Arithmetic, Propositional Logic, and Complexity Theory", Cambridge University Press.
• Template:Cite article
• Buss, S. R. (1987). "Polynomial size proofs of the propositional pigeonhole principle", Journal of Symbolic Logic 52, pp. 916–927.
• Pudlák, P., Buss, S. R. (1995). "How to lie without being (easily) convicted and the lengths of proofs in propositional calculus", in: Computer Science Logic'94 (Pacholski and Tiuryn eds.), Springer LNCS 933, 1995, pp. 151–162.