Derivation Glossary
Definition
A simple derivation of a formula A is a finite sequence (i.e. a list) of formulae whose last member is A. It is a derivation of A from a set X if every formula in it which is not an immediate consequence of earlier ones is a member of X.
A compound derivation is similarly a finite sequence, except that each item in the sequence is either a formula or else a sub-derivation in its own right. The total number of items, including those in sub-derivations, is still required to be finite.
Comments
Different specifications of what counts as "immediate consequence" may give rise to different systems of logic.
Compound derivations are convenient for making sense of natural deduction rules which discharge assumptions. Some presentations of logic use only simple derivations, but then the effect of discharging assumptions must be secured in some other way, which is usually less intuitive.
Examples
- Any natural deduction proof can be seen as a derivation, if the inference rules of the system are expressed as definitions of immediate consequence rather than as transformations on sequents.