[2] Derived from Suppes' method,[3] it represents natural deduction proofs as sequences of justified steps.
However, Kleene's version has the advantage that it is presented, although only very sketchily, within a rigorous framework of metamathematical theory, whereas the books by Suppes[3] and Lemmon[2] are applications of the tabular layout for teaching introductory logic.
The third holds a wff, which is justified by the rule held in the fourth along with auxiliary information about other wffs, possibly in other proofs.
The first column represents the line numbers of the assumptions the wff rests on, determined by the application of the cited rule in context.
Some have called the following technique, demonstrated in lines 3-6, the Rule of (Finite) Augmentation of Premises:[6] An example of substitution and ∨E: The historical development of tabular-layout natural deduction systems, which are rule-based, and which indicate antecedent propositions by line numbers (and related methods such as vertical bars or asterisks) includes the following publications.