Proof procedure

From Wikipedia, the free encyclopedia

In logic, and in particular proof theory, a proof procedure is a method of proving statements. A statement p that is provable from a non-empty set Γ of statements in a theory K is called a deduction of p from Γ in K. If Γ is empty then p is either a theorem of K (i.e. p∈K) or an axiom of K if K is axiomatic. We express that p is deducible (or provable or derivable or demonstrable) from Γ in K in symbols as

.

There are several types of proof procedures. The most popular are natural deduction, sequent calculi (i.e. Gentzen type systems), Hilbert type axiomatic systems, and semantic tableaux or trees.

We call a proof procedure M for a theory K sound if each and every member of the set of deducible formulas is valid (with respect to the semantics of K). We say that M is complete if the set of deducible formulas is a superset of the set of valid formulas of K. (Generally this last statement regarding completeness states that M is complete if the set of deducible formulas is exactly the set of valid formulas of K. But proof procedures that prove e.g. every formula are trivially complete even if K is consistent. They are, however, unsound.)

[edit] See also

• Automated theorem proving
• Proof complexity