Proofs in propositional calculus

One of the main uses of a propositional calculus, when interpreted for logical applications, is to determine relations of logical equivalence between propositional formulas. These relationships are determined by means of the available transformation rules, sequences of which are called derivations or proofs.

In the discussion to follow, a proof is presented as a sequence of numbered lines, with each line consisting of a single formula followed by a reason or justification for introducing that formula. Each premise of the argument, that is, an assumption introduced as a hypothesis of the argument, is listed at the beginning of the sequence and is marked as a "premise" in lieu of other justification. The conclusion is listed on the last line. A proof is complete if every line follows from the previous ones by the correct application of a transformation rule. (For a contrasting approach, see proof-trees).


Example of a proof in natural deduction system

  • To be shown that A → A.
  • One possible proof of this (which, though valid, happens to contain more steps than are necessary) may be arranged as follows:
Example of a proof

Number Formula Reason
1 A
 premise
2 A\lor A From (1) by disjunction introduction
3 (A\lor A)\land A From (1) and (2) by conjunction introduction
4 A From (3) by conjunction elimination
5 A\vdash A Summary of (1) through (4)
6 \vdash A\to A From (5) by conditional proof

Interpret A\vdash A as "Assuming A, infer A". Read \vdash A\to A as "Assuming nothing, infer that A implies A", or "It is a tautology that A implies A", or "It is always true that A implies A".


Example of a proof in a classical propositional calculus system

We now prove the same theorem A\to A in the axiomatic system by Jan Łukasiewicz described above, which is an example of a Hilbert-style deductive system for the classical propositional calculus.

The axioms are:

(p\to (q\to p))

((p\to (q\to r))\to ((p\to q)\to (p\to r)))

((\neg p\to \neg q)\to (q\to p))

And the proof is as follows:

  1.  A\to ((B\to A)\to A)      (instance of (A1))
  2. (A\to ((B\to A)\to A))\to ((A\to (B\to A))\to (A\to A))       (instance of (A2))
  3. (A\to (B\to A))\to (A\to A)      (from (1) and (2) by modus ponens)
  4. A\to (B\to A)       (instance of (A1))
  5. A\to A       (from (4) and (3) by modus ponens)