Jump to content

User:Bynne

From Wikipedia, the free encyclopedia

Frege Systems

[edit]

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

[edit]

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

Formal Definition

[edit]

Let be a set of boolean connectives on which we will define our system, let be a set of sound inference rules. We denote the deduction system by , if is implicationally complete we call it a Frege system.

F-Proof

[edit]

Let and be formulas. Let be a sequence of formulas such that we can derive from using a rule from , and such that we can derive from using a rule from . We call , an -proof/derivation of the formula from .

Refutational completeness

[edit]

We define a Frege system to be refutationally complete if for every formula that is a contradiction, there exists an -derivation of False from .

Length of formulas

[edit]

We define the length of a -proof to be the number of applications of rules in the proof.

Examples

[edit]
  • Common axioms are:
  • Common rules are:
    • (Modus Ponens rule).
    • (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 from - However adding the weakening rule: 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

[edit]
  • 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 is proportional to the logarithm of the minimal number of steps in a Frege proof of .
  • 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

References

[edit]
  • 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

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