Derivations

In 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 $\varphi \,\!$ to be valid (a tautology) in the following ways.

Do a truth table for $\varphi \,\!$ .

Obtain $\varphi \,\!$ as a substitution instance of a formula already known to be valid.

Obtain $\varphi \,\!$ by applying interchange of equivalents to a formula already known to be valid.

These methods fail in predicate logic, however, because truth tables are unavailable for predicates. Without an alternate method, we cannot use the second and third methods since they rely on knowing the validity of other formulas. An alternative method for showing a formula is valid—without using truth tables—is the use of derivations. This page and those that follow 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 in Formal Semantics that a formal language such as ${\mathcal {L_{S}}}\,\!$ 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. Given a logical system, the derivation system is called sound if it achieves these goals. That is, a derivation system is sound (has the property of soundness) 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 said to be complete 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 substantial results. Their proofs will not be given here, but are available in many standard metalogic text books.

Turnstiles

The $\vDash \,\!$ symbol is sometimes called a turnstile, in particular a semantic turnstile. We previously introduced the following three uses of this symbol.

(1)	${\mathfrak {v}}\vDash \varphi \,\!$	${\mathfrak {v}}\,\!$ satisfies $\varphi \,\!$ .
(2)	$\vDash \varphi \,\!$	$\varphi \,\!$ is valid.
(3)	$\Gamma \vDash \varphi \,\!$	$\Gamma \,\!$ implies (has as a logical consequence) $\varphi \,\!$ .

where ${\mathfrak {v}}$ is a valuation and $\Gamma$ is a set of premises, as introduced in Validity.

Derivations have a counterpart to the semantic turnstile, namely the syntactic turnstile. Item (1) above has no syntactic counterpart. However, (2) and (3) above have the following counterparts.

	(4)		$\vdash \varphi \,\!$		$\varphi \,\!$ is provable.
	(5)		$\Gamma \vdash \varphi \,\!$		$\Gamma \,\!$ proves (has as a derivational consequence) $\varphi \,\!$ .

Item (4) is the case if and only if there is a correct derivation of $\varphi \,\!$ from no premises. Similarly, (5) is the case if and only if there is a correct derivation of $\varphi \,\!$ which takes the members of $\Gamma \,\!$ as premises.

The negations of (4) and (5) above are

	(6)		$\not \vdash \varphi \,\!$
	(7)		$\Gamma \not \vdash \varphi \,\!$

We can now define soundness and completeness as follows:

Given a logical system, its derivation system is sound if and only if:

{\mbox{If }}\Gamma \vdash \varphi ,{\mbox{ then }}\Gamma \vDash \varphi .\,\!

Given a logical system, its derivation system is complete if and only if:

{\mbox{If }}\Gamma \vDash \varphi ,{\mbox{ then }}\Gamma \vdash \varphi .\,\!