Natural Deduction

Abstract Axiomatic proofs are hard to construct, and often very lengthy. So in practice one does not actually construct such proofs; rather, one proves that there is a proof, as originally defined. One way in which we make use of this technique is when we allow ourselves to use, in a proof, any theorem that has been proved already. For officially this is short for writing out once more, as part of the new proof, the whole of the original proof of that theorem. Another way is when we are explicitly relying on the deduction theorem, and so are actually concerned with a proof from assumptions, and not an axiomatic proof as first defined. Proofs from assumptions are much easier to find, and much shorter. A third way is when we introduce new symbols by definition, for in practice one will go on at once to derive new rules for the new symbols, and these will usually be rules for use in proofs from assumptions. So it comes about that, after a few initial moves, the development of an axiomatic system will scarcely ever involve writing out real axiomatic proofs, but will rely on a number of short cuts.