Frege Systems

In propositional calculus a Frege system is an implicationally complete deduction system with a set of logical connectives and a set of sound inference rules.

Implicational completeness

We say that a deduction system $I$ is implicationally complete iff, for every formula $S$ that is a tautology, there exists a derivation from the axioms using the rules of the system.

Formal Definition

Let ${\mathcal {K}}$ be a set of boolean connectives on which we will define our system, let ${\mathcal {R}}$ be a set of sound inference rules. We denote the deduction system by ${\mathcal {F}}=({\mathcal {K}},{\mathcal {R}})$ , if ${\mathcal {F}}$ is implicationally complete we call it a Frege system.

F-Proof

Let $A$ and $B$ be formulas. Let $F$ be a sequence of formulas $A_{1},\ldots ,A_{n},B$ such that we can derive $A_{i}$ from $A_{1},\ldots ,A_{i-1},A$ using a rule from ${\mathcal {R}}$ , and such that we can derive $B$ from $A_{1},\ldots ,A_{n},A$ using a rule from ${\mathcal {R}}$ . We call $F$ , an ${\mathcal {F}}$ -proof/derivation of the formula $B$ from $A$ .

Refutational completeness

We define a Frege system to be refutationally complete if for every formula $S$ that is a contradiction, there exists an ${\mathcal {F}}$ -derivation of False from $S$ .

Length of formulas

We define the length of a ${\mathcal {F}}$ -proof to be the number of applications of rules in the proof.

Examples

Common axioms are:
- $(\ ;A\lor {\overline {A}})$
- $(\ ;A\to A)$
Common rules are:
- ${\frac {A\quad A\to B}{B}}$ (Modus Ponens rule).
- ${\frac {A\lor C\quad B\lor {\overline {C}}}{A\lor B}}$ (Resolution rule).

Rules are interpreted as follows, the two statements above the line entails the one below the line.

Resolution is not a Frege system because it is not implicationally complete, i.e. we cannot conclude $A\lor B$ from $A$ - However adding the weakening rule: ${\frac {A}{A\lor B}}$ makes it implicationally complete and hence a Frege System.
Resolution is refutationally complete.
Natural deduction is a Frege system
Gentzen with cut is a Frege system
Frege's propositional calculus

Properties

A Frege proof can be converted to a sequent proof with at most a polynomial increase in length.
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$ .
Any Frege system is equivalent to a Gentzen with cut system, in the sense that there exists a translation of any frege proof/refutation to a Gentzen proof/refutation, with atmost a polynomial increase in length.
Same holds true for Natural deduction

Proof strengths of different systems

References

Buss, S. R. Pitassi, T. (1998). "Resolution and the weak pigeonhole", "Ann. Scuola Norm. Sup. Pisa".
Cook, S. Reckhow, R. (1974). "On the lengths of proofs in the propositional calculus: preliminary"
Pudlák, P. Buss, S. R. (1995). "How to lie without being (easily) convicted and the lengths of proofs in propositional calculus", "Ann. Scuola Norm. Sup. Pisa".

User:Bynne