Derivation Systems — Read

Introduction

Logics commonly have both a semantics and a derivation system. The semantics concerns concepts such as truth, satisfiability, validity, and entailment. The purpose of derivation systems is to provide a purely syntactic method of establishing entailment and validity. They are purely syntactic in the sense that a derivation in such a system is a finite syntactic object, usually a sequence (or other finite arrangement) of sentences or formulas. Good derivation systems have the property that any given sequence or arrangement of sentences or formulas can be verified mechanically to be “correct.”

The simplest (and historically first) derivation systems for first-order logic were axiomatic. A sequence of formulas counts as a derivation in such a system if each individual formula in it is either among a fixed set of “axioms” or follows from formulas coming before it in the sequence by one of a fixed number of “inference rules”—and it can be mechanically verified if a formula is an axiom and whether it follows correctly from other formulas by one of the inference rules. Axiomatic derivation systems are easy to describe—and also easy to handle meta-theoretically—but derivations in them are hard to read and understand, and are also hard to produce.

Other derivation systems have been developed with the aim of making it easier to construct derivations or easier to understand derivations once they are complete. Examples are natural deduction, truth trees, also known as tableaux proofs, and the sequent calculus. Some derivation systems are designed especially with mechanization in mind, e.g., the resolution method is easy to implement in software (but its derivations are essentially impossible to understand). Most of these other derivation systems represent derivations as trees of formulas rather than sequences. This makes it easier to see which parts of a derivation depend on which other parts.

So for a given logic, such as first-order logic, the different derivation systems will give different explications of what it is for a sentence to be a theorem and what it means for a sentence to be derivable from some others. However that is done (via axiomatic derivations, natural deductions, sequent derivations, truth trees, resolution refutations), we want these relations to match the semantic notions of validity and entailment. Let's write $\Proves !A$source 57 for “$!A$source 57 is a theorem” and “$\Gamma \Proves !A$source 58” for “$!A$source 58 is derivable from $\Gamma$source 58.” However $\Proves$source 59 is defined, we want it to match up with $\Entails$source 59, that is:

1. $\Proves !A$source 62 if and only if $\Entails !A$source 62

2. $\Gamma \Proves !A$source 63 if and only if $\Gamma \Entails !A$source 63

The “only if” direction of the above is called soundness. A derivation system is sound if derivability guarantees entailment (or validity). Every decent derivation system has to be sound; unsound derivation systems are not useful at all. After all, the entire purpose of a derivation is to provide a syntactic guarantee of validity or entailment. We'll prove soundness for the derivation systems we present.

The converse “if” direction is also important: it is called completeness. A complete derivation system is strong enough to show that $!A$source 75 is a theorem whenever $!A$source 75 is valid, and that $\Gamma \Proves !A$source 76 whenever $\Gamma \Entails !A$source 76. Completeness is harder to establish, and some logics have no complete derivation systems. First-order logic does. Kurt Gödel was the first one to prove completeness for a derivation system of first-order logic in his 1929 dissertation.

Another concept that is connected to derivation systems is that of consistency. A set of sentences is called inconsistent if anything whatsoever can be derived from it, and consistent otherwise. Inconsistency is the syntactic counterpart to unsatisfiability: like unsatisfiable sets, inconsistent sets of sentences do not make good theories, they are defective in a fundamental way. Consistent sets of sentences may not be true or useful, but at least they pass that minimal threshold of logical usefulness. For different derivation systems the specific definition of consistency of sets of sentences might differ, but like $\Proves$source 92, we want consistency to coincide with its semantic counterpart, satisfiability. We want it to always be the case that $\Gamma$source 94 is consistent if and only if it is satisfiable. Here, the “only if” direction amounts to completeness (consistency guarantees satisfiability), and the “if” direction amounts to soundness (satisfiability guarantees consistency). In fact, for classical first-order logic, the two versions of soundness and completeness are equivalent.

The Sequent Calculus

While many derivation systems operate with arrangements of sentences, the sequent calculus operates with sequents. A sequent is an expression of the form $$!A_1, \dots, !A_m \Sequent !B_1, \dots, !B_m,$$source 18 that is a pair of sequences of sentences, separated by the sequent symbol $\Sequent$source 22. Either sequence may be empty. A derivation in the sequent calculus is a tree of sequents, where the topmost sequents are of a special form (they are called “initial sequents” or “axioms”) and every other sequent follows from the sequents immediately above it by one of the rules of inference. The rules of inference either manipulate the sentences in the sequents (adding, removing, or rearranging them on either the left or the right), or they introduce a complex formula in the conclusion of the rule. For instance, the $\LeftR{\land}$source 30 rule allows the inference from $!A, \Gamma \Sequent \Delta$source 30 to $!A \land !B, \Gamma \Sequent \Delta$source 31, and the $\RightR{\lif}$source 32 allows the inference from $!A, \Gamma \Sequent \Delta, !B$source 32 to $\Gamma \Sequent \Delta, !A \lif !B$source 33, for any $\Gamma$source 33, $\Delta$source 34, $!A$source 34, and $!B$source 34. (In particular, $\Gamma$source 34 and $\Delta$source 34 may be empty.)

The $\Proves$source 37 relation based on the sequent calculus is defined as follows: $\Gamma \Proves !A$source 38 iff there is some sequence $\Gamma_0$source 38 such that every $!A$source 39 in $\Gamma_0$source 39 is in $\Gamma$source 39 and there is a derivation with the sequent $\Gamma_0 \Sequent !A$source 40 at its root. $!A$source 41 is a theorem in the sequent calculus if the sequent $\Sequent !A$source 41 has a derivation. For instance, here is a derivation that shows that $\Proves (!A \land !B) \lif !A$source 43:

A set $\Gamma$source 52 is inconsistent in the sequent calculus if there is a derivation of $\Gamma_0 \Sequent$source 53 (where every $!A \in \Gamma_0$source 53 is in $\Gamma$source 54 and the right side of the sequent is empty). Using the rule right weakening rule, any sentence can be derived from an inconsistent set.

The sequent calculus was invented in the 1930s by Gerhard Gentzen. Because of its systematic and symmetric design, it is a very useful formalism for developing a theory of derivations. It is relatively easy to find derivations in the sequent calculus, but these derivations are often hard to read and their connection to proofs are sometimes not easy to see. It has proved to be a very elegant approach to derivation systems, however, and many logics have sequent calculus systems.

Natural Deduction

Natural deduction is a derivation system intended to mirror actual reasoning (especially the kind of regimented reasoning employed by mathematicians). Actual reasoning proceeds by a number of “natural” patterns. For instance, proof by cases allows us to establish a conclusion on the basis of a disjunctive premise, by establishing that the conclusion follows from either of the disjuncts. Indirect proof allows us to establish a conclusion by showing that its negation leads to a contradiction. Conditional proof establishes a conditional claim “if … then …” by showing that the consequent follows from the antecedent. Natural deduction is a formalization of some of these natural inferences. Each of the logical connectives and quantifiers comes with two rules, an introduction and an elimination rule, and they each correspond to one such natural inference pattern. For instance, $\Intro{\lif}$source 28 corresponds to conditional proof, and $\Elim{\lor}$source 29 to proof by cases. A particularly simple rule is $\Elim{\land}$source 30 which allows the inference from $!A \land !B$source 30 to $!A$source 30 (or $!B$source 31).

One feature that distinguishes natural deduction from other derivation systems is its use of assumptions. A derivation in natural deduction is a tree of formulas. A single formula stands at the root of the tree of formulas, and the “leaves” of the tree are formulas from which the conclusion is derived. In natural deduction, some leaf formulas play a role inside the derivation but are “used up” by the time the derivation reaches the conclusion. This corresponds to the practice, in actual reasoning, of introducing hypotheses which only remain in effect for a short while. For instance, in a proof by cases, we assume the truth of each of the disjuncts; in conditional proof, we assume the truth of the antecedent; in indirect proof, we assume the truth of the negation of the conclusion. This way of introducing hypothetical assumptions and then doing away with them in the service of establishing an intermediate step is a hallmark of natural deduction. The formulas at the leaves of a natural deduction derivation are called assumptions, and some of the rules of inference may “discharge” them. For instance, if we have a derivation of $!B$source 50 from some assumptions which include $!A$source 51, then the $\Intro{\lif}$source 51 rule allows us to infer $!A \lif !B$source 52 and discharge any assumption of the form $!A$source 52. (To keep track of which assumptions are discharged at which inferences, we label the inference and the assumptions it discharges with a number.) The assumptions that remain undischarged at the end of the derivation are together sufficient for the truth of the conclusion, and so a derivation establishes that its undischarged assumptions entail its conclusion.

The relation $\Gamma \Proves !A$source 60 based on natural deduction holds iff there is a derivation in which $!A$source 61 is the last sentence in the tree, and every leaf which is undischarged is in $\Gamma$source 62. $!A$source 62 is a theorem in natural deduction iff there is a derivation in which $!A$source 64 is the last sentence and all assumptions are discharged. For instance, here is a derivation that shows that $\Proves (!A \land !B) \lif !A$source 65:

The label $1$source 74 indicates that the assumption $!A \land !B$source 74 is discharged at the conditional introduction rule inference.

A set $\Gamma$source 77 is inconsistent iff $\Gamma \Proves \lfalse$source 77 in natural deduction. The rule falsehood rule makes it so that from an inconsistent set, any sentence can be derived.

Natural deduction systems were developed by Gerhard Gentzen and Stanisław Jaśkowski in the 1930s, and later developed by Dag Prawitz and Frederic Fitch. Because its inferences mirror natural methods of proof, it is favored by philosophers. The versions developed by Fitch are often used in introductory logic textbooks. In the philosophy of logic, the rules of natural deduction have sometimes been taken to give the meanings of the logical operators (“proof-theoretic semantics”).

tableau

While many derivation systems operate with arrangements of sentences, tableaus operate with signed formulas. A signed formula is a pair consisting of a truth value sign ($\True$source 18 or $\False$source 18) and a sentence $$\sFmla{\True}{!A} \text{ or } \sFmla{\False}{!A}.$$source 19 A tableau consists of signed formulas arranged in a downward-branching tree. It begins with a number of assumptions and continues with signed formulas which result from one of the signed formulas above it by applying one of the rules of inference. Each rule allows us to add one or more signed formulas to the end of a branch, or two signed formulas side by side—in this case a branch splits into two, with the two added signed formulas forming the ends of the two branches.

A rule applied to a complex signed formula results in the addition of signed formulas which are immediate sub-formulas. They come in pairs, one rule for each of the two signs. For instance, the $\TRule{\True}{\land}$source 34 rule applies to $\sFmla{\True}{!A \land !B}$source 34, and allows the addition of both the two signed formulas $\sFmla{\True}{!A}$source 36 and $\sFmla{\True}{!B}$source 36 to the end of any branch containing $\sFmla{\True}{!A \land !B}$source 37, and the rule $\TRule{\False}{!A \land !B}$source 38 allows a branch to be split by adding $\sFmla{\False}{!A}$source 39 and $\sFmla{\False}{!B}$source 39 side-by-side. A tableau is closed if every one of its branches contains a matching pair of signed formulas $\sFmla{\True}{!A}$source 41 and $\sFmla{\False}{!A}$source 42.

The $\Proves$source 44 relation based on tableaus is defined as follows: $\Gamma \Proves !A$source 45 iff there is some finite set $\Gamma_0 = \{!B_1, \dots, !B_n\} \subseteq \Gamma$source 45 such that there is a closed tableau for the assumptions $$\{\sFmla{\False}{!A}, \sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\}$$source 48 For instance, here is a closed tableau that shows that $\Proves (!A \land !B) \lif !A$source 51:

A set $\Gamma$source 65 is inconsistent in the tableau calculus if there is a closed tableau for assumptions $$\{\sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\}$$source 67 for some $!B_i \in \Gamma$source 70.

Tableaus were invented in the 1950s independently by Evert Beth and Jaakko Hintikka, and simplified and popularized by Raymond Smullyan. They are very easy to use, since constructing a tableau is a very systematic procedure. Because of the systematic nature of tableaus, they also lend themselves to implementation by computer. However, a tableau is often hard to read and their connection to proofs are sometimes not easy to see. The approach is also quite general, and many different logics have tableau systems. Tableaus also help us to find structures that satisfy given (sets of) sentences: if the set is satisfiable, it won't have a closed tableau, i.e., any tableau will have an open branch. The satisfying structure can be “read off” an open branch, provided every rule it is possible to apply has been applied on that branch. There is also a very close connection to the sequent calculus: essentially, a closed tableau is a condensed derivation in the sequent calculus, written upside-down.

Axiomatic derivation

Axiomatic derivations are the oldest and simplest logical derivation systems. Its derivations are simply sequences of sentences. A sequence of sentences counts as a correct derivation if every sentence $!A$source 18 in it satisfies one of the following conditions:

1. $!A$source 21 is an axiom, or

2. $!A$source 22 is an element of a given set $\Gamma$source 22 of sentences, or

3. $!A$source 23 is justified by a rule of inference.

To be an axiom, $!A$source 25 has to have the form of one of a number of fixed sentence schemas. There are many sets of axiom schemas that provide a satisfactory (sound and complete) derivation system for first-order logic. Some are organized according to the connectives they govern, e.g., the schemas $$!A \lif (!B \lif !A) \qquad !B \lif (!B \lor !C) \qquad (!B \land !C) \lif !B$$source 30 are common axioms that govern $\lif$source 33, $\lor$source 33 and $\land$source 33. Some axiom systems aim at a minimal number of axioms. Depending on the connectives that are taken as primitives, it is even possible to find axiom systems that consist of a single axiom.

A rule of inference is a conditional statement that gives a sufficient condition for a sentence in a derivation to be justified. Modus ponens is one very common such rule: it says that if $!A$source 40 and $!A \lif !B$source 40 are already justified, then $!B$source 41 is justified. This means that a line in a derivation containing the sentence $!B$source 42 is justified, provided that both $!A$source 43 and $!A \lif !B$source 43 (for some sentence $!A$source 43) appear in the derivation before $!B$source 44.

The $\Proves$source 46 relation based on axiomatic derivations is defined as follows: $\Gamma \Proves !A$source 47 iff there is a derivation with the sentence $!A$source 48 as its last formula (and $\Gamma$source 48 is taken as the set of sentences in that derivation which are justified by (2) above). $!A$source 49 is a theorem if $!A$source 50 has a derivation where $\Gamma$source 50 is empty, i.e., every sentence in the derivation is justified either by (1) or (3). For instance, here is a derivation that shows that $\Proves !A \lif (!B \lif (!B \lor !A))$source 52:

The sentence on line 1 is of the form of the axiom $!A \lif (!A \lor !B)$source 59 (with the roles of $!A$source 60 and $!B$source 60 reversed). The sentence on line 2 is of the form of the axiom $!A \lif (!B \lif !A)$source 61. Thus, both lines are justified. Line 3 is justified by modus ponens: if we abbreviate it as $!D$source 63, then line 2 has the form $!C \lif !D$source 63, where $!C$source 64 is $!B \lif (!B \lor !A)$source 64, i.e., line 1.

A set $\Gamma$source 66 is inconsistent if $\Gamma \Proves \lfalse$source 66. A complete axiom system will also prove that $\lfalse \lif !A$source 67 for any $!A$source 67, and so if $\Gamma$source 68 is inconsistent, then $\Gamma \Proves !A$source 68 for any $!A$source 68.

Systems of axiomatic derivations for logic were first given by Gottlob Frege in his 1879 Begriffsschrift, which for this reason is often considered the first work of modern logic. They were perfected in Alfred North Whitehead and Bertrand Russell's Principia Mathematica and by David Hilbert and his students in the 1920s. They are thus often called “Frege systems” or “Hilbert systems.” They are very versatile in that it is often easy to find an axiomatic system for a logic. Because derivations have a very simple structure and only one or two inference rules, it is also relatively easy to prove things about them. However, they are very hard to use in practice, i.e., it is difficult to find and write proofs.