Frege system

Last updated

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. [1] Frege systems (more often known as Hilbert systems in general proof theory) are named after Gottlob Frege.

Contents

The name "Frege system" was first defined [2] by Stephen Cook and Robert Reckhow, [3] [4] and was intended to capture the properties of the most common propositional proof systems. [2]

Formal definition

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. 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

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

Properties

Extended Frege system

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 , where abbreviates its definition in the language of the particular F and the atom does not occur in previously derived formulas including axioms and in the formula .

The purpose of the new derivation rule is to introduce 'names' or shortcuts for arbitrary formulas. It allows one to interpret proofs in Extended Frege as Frege proofs operating with circuits instead of formulas.

Cook's correspondence allows one to interpret Extended Frege as a nonuniform equivalent of Cook's theory PV and Buss's theory formalizing feasible (polynomial-time) reasoning.

References

  1. 1 2 Krajicek, Jan (1995-11-24). Bounded Arithmetic, Propositional Logic and Complexity Theory. Cambridge University Press. p. 42. ISBN   978-0-521-45205-2.
  2. 1 2 3 Pudlák, Pavel; Buss, Samuel R. (1995). "How to lie without being (easily) convicted and the lengths of proofs in propositional calculus". In Pacholski, Leszek; Tiuryn, Jerzy (eds.). Computer Science Logic. Lecture Notes in Computer Science. Vol. 933. Berlin, Heidelberg: Springer. pp. 151–162. doi:10.1007/BFb0022253. ISBN   978-3-540-49404-1.
  3. 1 2 Cook, Stephen; Reckhow, Robert (1974-04-30). "On the lengths of proofs in the propositional calculus (Preliminary Version)". Proceedings of the sixth annual ACM symposium on Theory of computing - STOC '74. New York, NY, USA: Association for Computing Machinery. pp. 135–148. doi:10.1145/800119.803893. ISBN   978-1-4503-7423-1.
  4. 1 2 3 4 5 Cook, Stephen A.; Reckhow, Robert A. (1979). "The relative efficiency of propositional proof systems" . The Journal of Symbolic Logic. 44 (1): 36–50. doi:10.2307/2273702. ISSN   0022-4812. JSTOR   2273702.
  5. Buss, Samuel R. (1987). "Polynomial Size Proofs of the Propositional Pigeonhole Principle" . The Journal of Symbolic Logic. 52 (4): 916–927. doi:10.2307/2273826. ISSN   0022-4812. JSTOR   2273826.