ABSTRACT
By a deductive system for a particular symbolic language, like a first-order language, we shall mean a set of rules, like the tree rules, which are purely formal, or syntactical, in character and which determine formal proofs of sentences from sets of sentences formalised in that language. The deductive system based on trees is not the only one for first-order logic. Indeed, there are several, all of which are known to possess analogous soundness and completeness properties. Some, like the so-called natural deduction system described in section 3, attempt to model themselves on our informal reasoning; others, like the system H described below, do not-or at any rate, not to the same extent.
