THE LOGIC NOTES

Proof Glossary

Definition

In the natural deduction calculus, a proof is a finite sequence of lines of proof, each of which is either an assumption or connected to earlier lines by a rule of inference. Each line represents a sequent: the assumption numbers in the left column refer to the formulae assumed on the specified lines and represent the premises of the sequent, while the formula displayed on the line is the conclusion. The sequent represented by each line is proved because the proof above it is a derivation of its conclusion from its premises.

Comments

In applications of logic, especially in mathematics, it is common to regard certain assumptions as given—as axioms of a theory. A logical derivation of a conclusion from those assumptions shows that conclusion to be a theorem of the theory in question. Mathematicians use "proof" in this sense: the theorem is proved in the theory. This is clearly a matter of reading: the purely logical view is that what is proved is a sequent with the axioms of the theory as premises.

Other ways of presenting logic give rise to other notions of "proof". Proofs in the sequent calculus, for example, or in tableaux, are rather different from natural deduction proofs. This should not cause any great confusion.

Examples

See the links below for many examples of natural deduction proofs.

Links