Formal Logic/Sentential Logic/Derivations
|← Translations||↑ Sentential Logic||Inference Rules →|
At Validity, we introduced the notion of validity for formulae and for arguments. In sentential logic, a valid formula is a tautology.
Up to now, we could show a formula to be valid (a tautology) in the following ways.
- Do a truth table for .
- Obtain as a substitution instance of a formula already known to be valid.
- Obtain by applying interchange of equivalents to a formula already known to be valid.
Truth tables become unavailable in predicate logic. Without an alternate method, there will be no way of getting the second two methods started since they need already known validities to work. Derivations provide such an alternate method for showing a formula valid, a method that continues to work even after truth tables become unavailable. This page, together with the several following it, introduce this technique. Note, the claim that a derivation shows an argument valid assumes a sound derivation system, see soundness below.
A derivation is a series of numbered lines, each line consisting of a formula with an annotation. The annotations provide the justification for adding the line to the derivation. A derivation is a highly formalized analogue to—or perhaps a model of—a mathematical proof.
A typical derivation system will allow some of the following types of lines:
- A line may be an axiom. The derivation system may specify a set of formulae as axioms. These are accepted as true for any derivation. For sentential logic the set of axioms is a fixed subset of tautologies.
- A line may be an assumption. A derivation may have several types of assumptions. The following cover the standard cases.
- A premise. When attempting to show the validity of an argument, a premise of that argument may be assumed.
- A temporary assumption for use in a subderivation. Such assumptions are intended to be active for only part of a derivation and must be discharged (made inactive) before the derivation is considered complete. Subderivations will be introduced on a later page.
- A line may result from applying an inference rule to previous lines. An inference is a syntactic transformation of previous lines to generate a new line. Inferences are required to follow one of a fixed set of patterns defined by the derivation system. These patterns are the system's inference rules. The idea is that any inference fitting an inference rule should be a valid argument.
Soundness and validity
We noted at Formal Semantics that a formal language such as can be interpreted via several alternative and even competing semantic rule-sets. Multiple derivation systems can be also defined for a given syntax-semantics pair. A triple consisting of a formal syntax, a formal semantics, and a derivation system is a logical system.
A derivation is intended to show an argument to be valid. A derivation of a zero-premise argument is intended to show its conclusion to be a valid formula—in sentential logic this means showing it to be a tautology. These are the intentions. Given a logical system, the derivation system is sound if and only if it achieves this goal. That is, a derivation system is sound (has the property of soundness) if and only if every formula (and argument) derivable in its derivation system is valid (given a syntax and a semantics).
Another desirable quality of a derivation system is completeness. Given a logical system, its derivation system is complete if and only if every valid formula is derivable. However, there are some logics for which no derivation system is or can be complete.
Soundness and completeness are metalogic substantial results. Their proofs will not be given here, but are available in many standard metalogic text books.
The symbol is sometimes called a turnstile, in particular a semantic turnstile. We previously introduced the following three uses of this symbol.
|(3)||implies (has as a logical consequence) .|
Derivations have a counterpart to the semantic turnstile, namely the syntactic turnstile. (1) above has no syntactic counterpart. However, (2) and (3) above have the following counterparts.
|(5)||proves (has as a derivational consequence) .|
(4) is the case if and only if there is a correct derivation of from no premises. Similarly, (5) is the case if and only if there is a correct derivation of which takes the members of as premises.
The negations of (4) and (5) above are
We can now define soundness and completeness as follows:
- Given a logical system, its derivation system is sound if and only if:
- Given a logical system, its derivation system is complete if and only if: