A coding method for a sequent calculus of propositional logic (Q946138)

Given a sequent of propositional calculus, one can construct its deduction tree to see if the sequent is derivable and how. Drawbacks of this procedure are that subformulas must be copied over and over again, and the tree can expand rapidly because it has many branches. (The author gives an example of a formula with four letters that has 64 branches in its deduction tree.) But from a sequent \(\to F\), one can read off \(F\)'s main connective and so what inference rule is to be used, with two premises or one, and which subformulas belong in the antecedent or succedent of the premise sequent(s). One can repeat this process for new sequents, and read off how many branches there are and what all the leaves are. The author's aim in this paper is to code the above information in a neat and handy way, and get all the leaves without constructing the tree. His instruction for coding is precise and natural, and he gives a number of examples for illustration and as applications.