Frege system
   HOME

TheInfoList



OR:

In
proof complexity In logic and theoretical computer science, and specifically proof theory and computational complexity theory, proof complexity is the field aiming to understand and analyse the computational resources that are required to prove or refute statements. ...
, a Frege system is a
propositional proof system In propositional calculus and proof complexity a propositional proof system (pps), also called a Cook–Reckhow propositional proof system, is a system for proving classical propositional tautologies. Mathematical definition Formally a pps is a ...
whose proofs are
sequence In mathematics, a sequence is an enumerated collection of objects in which repetitions are allowed and order matters. Like a set, it contains members (also called ''elements'', or ''terms''). The number of elements (possibly infinite) is calle ...
s of
formulas In science, a formula is a concise way of expressing information symbolically, as in a mathematical formula or a ''chemical formula''. The informal use of the term ''formula'' in science refers to the general construct of a relationship betwee ...
derived using a finite set of
sound In physics, sound is a vibration that propagates as an acoustic wave, through a transmission medium such as a gas, liquid or solid. In human physiology and psychology, sound is the ''reception'' of such waves and their ''perception'' by the ...
and implicationally complete
inference rules In the philosophy of logic, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion (or conclusions). For example, the rule of i ...
. Frege systems (more often known as
Hilbert system :''In mathematical physics, ''Hilbert system'' is an infrequently used term for a physical system described by a C*-algebra.'' In logic, especially mathematical logic, a Hilbert system, sometimes called Hilbert calculus, Hilbert-style deductive ...
s in general
proof theory Proof theory is a major branchAccording to Wang (1981), pp. 3–4, proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. Jon Barwise, Barwise (1978) consists of four correspo ...
) are named after
Gottlob Frege Friedrich Ludwig Gottlob Frege (; ; 8 November 1848 – 26 July 1925) was a German philosopher, logician, and mathematician. He was a mathematics professor at the University of Jena, and is understood by many to be the father of analytic phil ...
.


Formal definition

Let ''K'' be a finite
functionally complete In logic, a functionally complete set of logical connectives or Boolean operators is one which can be used to express all possible truth tables by combining members of the set into a Boolean expression.. ("Complete set of logical connectives").. (" ...
set of Boolean connectives, and consider
propositional formula In propositional logic, a propositional formula is a type of syntactic formula which is well formed and has a truth value. If the values of all variables in a propositional formula are given, it determines a unique truth value. A propositional fo ...
s built from variables ''p''0, ''p''1, ''p''2, ... using ''K''-connectives. A Frege rule is an inference rule of the form :r=\fracB, where ''B''1, ..., ''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 ''A''1, ..., ''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 Substitution may refer to: Arts and media *Chord substitution, in music, swapping one chord for a related one within a chord progression * Substitution (poetry), a variation in poetic scansion * "Substitution" (song), a 2009 song by Silversun Pi ...
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 ''A''1, ..., ''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 In mathematical logic, Frege's propositional calculus was the first axiomatization of propositional calculus. It was invented by Gottlob Frege, who also invented predicate calculus, in 1879 as part of his second-order predicate calculus (although ...
is a Frege system. * There are many examples of sound Frege rules on the
Propositional calculus Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions (which can be true or false) and relations b ...
page. *
Resolution Resolution(s) may refer to: Common meanings * Resolution (debate), the statement which is debated in policy debate * Resolution (law), a written motion adopted by a deliberative body * New Year's resolution, a commitment that an individual mak ...
is not a Frege system because it only operates on
clauses In language, a clause is a constituent that comprises a semantic predicand (expressed or not) and a semantic predicate. A typical clause consists of a subject and a syntactic predicate, the latter typically a verb phrase composed of a verb with ...
, 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 A \lor B from A. However, adding the ''weakening'' rule: \frac makes it implicationally complete. Resolution is also refutationally complete.


Properties

*Reckhow's theorem (1979) states that all Frege systems are p-equivalent. *
Natural deduction In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use axiom ...
and
sequent calculus In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology (called a sequent by Gerhard Gentzen) instead of an unconditional tautology. Each conditional tautology i ...
(Gentzen system with cut) are also p-equivalent to Frege systems. * There are polynomial-size Frege proofs of the
pigeonhole principle In mathematics, the pigeonhole principle states that if items are put into containers, with , then at least one container must contain more than one item. For example, if one has three gloves (and none is ambidextrous/reversible), then there mu ...
(Buss 1987). * Frege systems are considered to be fairly strong systems. Unlike, say, resolution, there are no known superlinear lower bounds on the number of lines in Frege proofs, and the best known lower bounds on the size of the proofs are quadratic. * The minimal number of rounds in the ''prover-adversary'' game needed to prove a tautology \phi is proportional to the logarithm of the minimal number of steps in a Frege proof of \phi. File:Proofstrength.png, Proof strengths of different systems.


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 p \leftrightarrow D, where \leftrightarrow abbreviates its definition in the language of the particular ''F'' and the atom p does not occur in previously derived formulas including axioms and in the formula D. 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 S^1_2 formalizing feasible (polynomial-time) reasoning.


References

*Krajíček, Jan (1995). "Bounded Arithmetic, Propositional Logic, and Complexity Theory", Cambridge University Press. *{{cite journal, first1=Stephen, last1=Cook, authorlink1=Stephen Cook, first2=Robert A., last2=Reckhow, title=The Relative Efficiency of Propositional Proof Systems, journal=Journal of Symbolic Logic, volume=44, number=1, year=1979, pages=36–50, doi=10.2307/2273702, jstor=2273702 *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. Propositional calculus Logic in computer science