An elementary completeness proof for a system of natural deduction.
David W. Bennett · Notre Dame Journal of Formal Logic · 1973
The system of deduction of this paper is based on three operations: negation, conjunction, and universal quantification.Let formulas be formed for these operations in the usual way, except that distinct styles of letter are to be used for free and bound variables.A finite string of formulas, each preceded by one of the three lables '[' (assume), '/' (infer), or ']/> (discharge an assumption and infer), is called a deduction if the brackets are appropriately mated.This will be the case if mated pairs of left and right brackets can be successively eliminated from the inside out to leave only left brackets or no brackets at all.By the scope of a labelled formula in a deduction is meant the string of formulas which precede it, exclusive of those already enclosed in brackets.Let the following Rules of Inference be given:Simplification: From a conjunction infer either conjunct.Conjunction: From two formulas infer their conjunction.Instantiation: From a universal formula infer any of its instances.Generalisation: From a formula a infer a universal generalisation of a.A deduction is valid if it satisfies the following Rules of Deduction: Direct Proof: A formula labelled '/' must follow from other formulas in its scope by the Rules of Inference.Indirect Proof: A formula labelled '[', called an assumption, must be a negation, and, in fact, the negation of the formula with the mated label ']/', provided such a formula occurs.This will be the case only if the assumption appears in the scope of some formula and its negation.Special Rule: In any application of the Rule of Generalisation the instantial variable must have no occurrence in any assumption in the scope of the derived formula.