User:Bynne

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

Further reading

• MacKay, D. J. (2008). "Information Theory, Inference, and Learning Algorithms"