Zero-Order Logic: Proof Theory
Norman M. Martin · Cambridge University Press eBooks · 1989
Our next task is to formulate exactly the notion of a derivation of a wff A from a set of wffs α (in a calculus). The basic notion is that of a string or sequence of wffs each of which is an element of α or follows from earlier wffs by application of a rule of the calculus and whose last element is A. For suitable calculi, a minor revision of this condition would suffice to define derivation. But because we also want to allow systems that use subordinate derivations (sometimes called “natural deduction” systems), we will have to take a more complicated path. Perhaps the paradigm of the kind of rule we have to accommodate is “conditionalizcuion, ” which asserts that if we can derive B from a set of premises a together with an additional premise A, we can derive “if A, then B” from the premise set a. Intuitively, we have a sequence of derivations in the first sense, except that the rules must allow reference to earlier “derivations” in the sequence. Here the matter is complicated by the fact that, normally at least, it is not the details of the subordinate derivation, but what conclusion follows from what premises, which is the relevant information. However, the fact that the principal derivation has certain premises and conclusions unfortunately does not specify what wffs are allowed to be premises and conclusions in the subordinate derivations.