Automated Reasoning in Higher Order Logic
This page was created and is maintained by Chad E Brown.
Investigations into Logical Deduction (1934)
Introduction: At age 22 in 1932, Gentzen submitted the paper #1: "On the Existence of Independent Axiom Systems for Infinite Sentence Systems." He introduces a system of the propositional calculus as a sequent calculus based on Hertz's work. He modifies Hertz's "syllogism" rule to be Gentzen's "cut" rule. In this context he constructs an infinite set of sentences that has no independent set of axioms. He also shows that all "linear" sentence systems do have an independent axiomatization.
Tarski introduced the semantic notion of logical consequence in 1936. Gentzen had developed this idea (for propositional logic) in #1. Gentzen's natural deduction system in #3 [1935, see below] provides a formalization of the notion of consequence in the sense first used by Bolzano (which was introduced by Bolzano over a hundred years earlier and is analogous to Tarski's notion).
Gentzen studied axiom systems and axiomatic methods in order to contribute to Hilbert's program. Gentzen classifies mathematics into three levels (a classification which goes back to Weyl [1931]) based on how infinity is used: elementary number theory, analysis, general set theory. Gentzen, like the intuitionists, attributes the antimonies to a liberal use of infinity, but does not completely reject the law of the excluded middle in infinite situations. Gentzen showed in #2 [1934] that propositions of elementary number theory (the "first level" of mathematics) not involving any disjunction or existential quantifier is intuitionistically provable iff it is classically provable. He also proves that classical arithmetic can be interpreted in intuitionistic arithmetic using the same "double negation" transformation used by Kolmogorov [1925]. Gentzen notes that this implies, due to Godel's second incompleteness theorem, that the consistency of intuitionistic arithmetic cannot be proven within classical arithmetic.
In #3, Gentzen breaks free from the formulations of logic given by Frege, Russell and Hilbert by introducing natural deduction and sequent-style systems for predicate logic. After developing and examining the 'natural calculus' Gentzen conjectured that proofs should have a "normal form" in which "all concepts required for the proof would in some sense appear in the conclusion of the proof." This is the subformula property. The conjecture was proven as his Hauptsatz ("Main Theorem"--cut-elimination theorem). In the case of classical logic, Gentzen proved his sharpened Hauptsatz, that a proof can be divided into a propositional part and a quantification part (with the "midsequent" in the middle). This result is similar to Herbrand's theorem [1930]. Gentzen considered Herbrand's theorem a special case of his own. This mistake can be attributed to the fact that the form of Herbrand's theorem commonly known applied only to prenex formulas, when Herbrand's full theorem applies to any formula. Herbrand also supplies more information about the midsequent than Gentzen. However, unlike Herbrand's work, Gentzen's results generalize to intuitionistic logic and modal calculi. Curry [1950] extended the sharpened Hauptsatz to modal logic.
Due to the analogy between Gentzen's and Herbrand's theorems, we may refer to both in certain quantificational situations as the Gentzen-Herbrand theorem. Craig [1957] presented a modification of the theorem and used it to make a connection between model theory and proof theory.
Gentzen's natural deduction was reformulated by Beth [1965] who created "semantic tableau" as a system for studying the notion of "logical consequence". [Semantic tableau and its variants form a basis for many theorem proving systems.] Semantic tableau can be used to construct counterexamples (for propositions which are not a logical consequence of the hypotheses). Beth's system satisfies the subformula property and can be used to show Herbrand's theorem as well as the Lowenheim-Skolem theorem. Beth [1957] also proved his definability theorem using Gentzen's methods. Craig [1957] used the Herbrand-Gentzen theorem to prove a generalization of Beth's results.
Gentzen used the sharpened Hauptsatz to show the consistency of arithmetic without induction, which he acknowledged is of limited significance due to the importance of induction.
In #4 [1936], Gentzen proved the consistency of elementary number theory. This necessitated a reconsideration of the notion of the consistency proofs called for by Hilbert's program in light of Godel's second incompleteness theorem. Gentzen's "way out" was to use transfinite induction up to an ordinal which is not formalizable in elementary number theory. This is a "relative consistency" result, because the consistency of such a transfinite induction is assumed. Godel's theorem implies there is no absolute consistency proof. Such a transfinite induction may not be strictly "finitist", but can be considered to be, as Black [1940] said, elementary. Gentzen compares finitistic methods with (in some sense) less restrictive intuitionist methods. The consistency proof consists of showing how every derivable sequent can be put into a reduced form. Derivations are well-ordered in a way so that reduction steps reduce the ordering. This is how transfinite induction (up to the first epsilon-number epsilon_0--that is, the first ordinal satisfying omega^epsilon = epsilon--this ordinal may be constructed as the limit of the sequence omega, omega^omega, (omega^omega)^omega, . . .) is used in order to show the reduction terminations. Consistency follows from the fact that the sequent "1 = 2" is not in reduced form but any derivation of the sequent cannot be reduced. Hence, there can be no derivation of "1 = 2".
In #6 [1936] Gentzen argues that such a transfinite induction is in harmony with finitist intentions and expresses a hope that a similar consistency proof for analysis can be obtained. (In fact, Gentzen believed he could carry out such a proof while he was imprisoned by the new local authorities in Prague after World War II in 1945. Unfortunately, he died before being released and never was able to write such a proof.) Gentzen's ideas led to a number of consistency results for fragments of analysis.
In #5 [1936] Gentzen proves the consistency of the simple theory of types, essentially by assuming the domain of individuals is a singleton. Note that the only types he considers are the "set" domains. He numbers the types as type 0 [i], type 1 [oi], type 2 [o(oi)], etc. "Usually," Gentzen states in the paper, "multi-place predicates are used, and so are predicates of predicates, etc., necessitating a further hierarchy of predicates within the various types. As observed by Godel, however, this second hierarchy is dispensible." This refers to a small portion of Godel's 1931 paper on undecidability. Note also the result by Wiener [1914]. A similar proof of consistency of type theory was presented by Tarski [1933] in a more general context.
Takeuti [1953] showed how to represent mathematical theories in GLC, his sequent calculus for simple type theory. In 1956, Takeuti used techniques similar to Gentzen's to show the consistency of a certain system of ramified real numbers by proving a cut elimination theorem for the system. Schutte [1952, 1954, 1960] also proved cut elimination theorems from which followed the consistency of ramified and type-free analysis. Ackermann [1940, 1950-1953] adapted Gentzen's method of using transfinite induction to proofs which use Hilbert's epsilon-symbol.
In #8 [1938], Gentzen gives a new proof of consistency of elementary number theory based on his sequent calculus LK (where the one in #4 was based on natural deduction). He argues that epsilon_0 is the smallest ordinal we can expect to use to show such a consistency result, because induction up to smaller ordinals can be formalized within the formalism which would provide a contradiction to Godel's theorem. In #9 [1943], Gentzen proves that transfinite induction up to epsilon_0 cannot be proven in elementary number theory. This provides a confirmation of Godel's theorem and illustrates incompleteness in a direct way. Gentzen explains why he does not believe Godel's theorem is surprising and is a relatively minor obstacle in metamathematics. He compares his "restricted transfinite induction" method to be analogous to Weierstrass's epsilon-delta proofs in calculus.
In #7, Gentzen examines the state of foundations of mathematics. He contrasts the "constructive" conception of infinity with the "as if" conception. The idea is that we can use intuitionistic methods to show a formal system is without contradiction, and then operate with infinite sets within the formal system "as if" we can comprehend them in their entirity. This is not to say that such sets are fictions, but that the question of their actual interpretation is a matter of taste. The "as if" point of view, Gentzen argues, represents a minimal ontological commitment. Intuitionists reject nonconstructive mathematics as being "without sense." This objection seems to be based on Kant's conviction that all concepts are empirical intuitions based on sense data. Hilbert agrees with Kant in the sense that the symbols used in mathematics are objects of "immediate experience." This corresponds to Hilberts finitist view of formalist mathematics (which Gentzen helped develop).
#3 Investigations into Logical Deduction (1934): Gentzen introduces systems of natural deduction for intuitionist (NJ) and classical (NK) pure predicate calculus. He then proves the Hauptsatz ("Main Theorem"--cut-elimination) which implies that we can put every proof into a (not necessarily unique) normal form. In order to prove the Hauptsatz, he introduces two formal systems (sequent calculi) LJ and LK for which he proves the Hauptsatz and then proves the equivalence of LJ to NJ and LK to NK. (He also proves these equivalent to certain Hilbert-style formal systems.)
Gentzen begins by introducing the terminology. First, we have symbols: constants, functions, predicates, logical symbols, variables. Next, we have expressions: formulae, sequents (note there are no compound terms). The degree of a formula is the number of logical symbols. Formulas of degree 0 are called "elementary" [now called "atomic"]. The terminal symbol of a nonelementary [compound] formula is the root logical symbol. Sequents have an antecedent and succedent. Finally, we have figures (finite sets of symbols with some ordering): an inference figure, a proof figure (or "derivation") with initial formulae and an endformula.
Next, Gentzen introduces natural deduction using three small examples of theorems in predicate calculus. Previous (Hilbert-style) deduction systems started from basic logical propositions and derived theorems. Gentzen designed his natural deduction derivations to start from assumptions (which are later discharged) instead of basic propositions. He introduces the NJ-calculus (intuitionistic) by giving the introduction and elimination inference rules. The NK-calculus (classical) is obtained by allowing 'basic formulae' of the form "A or not A" (excluded middle--"tertium non datur").
Gentzen proves the Hauptsatz (cut-elimination) for deductive calculi LJ and LK. LJ- and LK-derivations are built from inference figures on sequents. These include structural figures (thinning, contraction, interchange, cut) and operational inference figures (and-IS, and-IA, or-IA, or-IS, forall-IS, exists-IA, forall-IA, not-IS, exists-IS, not-IA, implies-IS, implies-IA). An LJ-derivation does not allow the succedent of any sequent to contain more than one formula. The Hauptsatz states that every LJ- or LK-derivation can be transformed into one without cuts and with the same endsequent. A corollary is the "Subformula Property" that all formulae in the (cut-free) derivation are subformulae of the formulas in the endsequent.
He first proves the Hauptsatz for LK (classical logic). Actually, we modify the notion of such derivations to use a "mix" rule instead of cut. Then we prove the lemma that any derivation which ends with a mix (without containing any other mix) can be transformed into a mix-free derivation with the same endsequent. Given this lemma, the Hauptsatz follows easily by induction. The lemma itself is proven by induction on the degree and rank of the derivation. The degree of the derivation is the degree of the (number of logical symbols in) mix formula. The rank of the derivation is the sum of the left rank and right rank, where the left rank is the longest path which ends with the left-hand upper sequent of the mix and all the sequents on the path contain the mix formula in the succedent. The right rank is defined analogously: the longest path ending with the right-hand upper sequent of the mix and all the sequents on the path contain the mix formula in the antecedent. The smallest possible rank is 2. Before we begin the transformation, we can change the names of ("redesignate") free variables to ensure no conflicts arise.
If the rank of the mix is two, then either one of the mix formula is basic or is introduced by thinning (in both cases we can eliminate the mix) or both occurrences of the mix formula are principle formulas of introduction figures for the terminal symbol of the mix formula. In these cases we can transform the derivation to use mixes of smaller degree (but possibly larger rank). If the rank is greater than two, then we can, essentially, move the mix up one step so that the rank decreases by at least one and the degree remains the same (because the mix formula has not changed). So, given a derivation which only contains a mix as the final step, we can keep transforming until the rank is two, transform to decrease the degree, transform again until the rank is two, transform to decrease the degree, and so on until the mix has been eliminated. This is a bit oversimplified because the transformation may yield a derivation with more than one mix (of smaller degree or rank). In fact, (consider the case with rank two and terminal symbol "implies") we may transform the derivation into a derivation with nested mixes. Nevertheless, the basic idea above works, modulo these details.
The same proof works for LJ-derivations if we check that each step in the transformation yields a sequent with no more than one formula in the succedent if the original derivation was an LJ-derivation.
The Hauptsatz implies a number of results. Classical and intuitionistic predicate logic are consistent, because the empty sequent can only be the conclusion of a cut. (This was already known.) It can be used to build a decision procedure for intuitionist propositional logic. (If there is a proof, then there must be a proof in which no sequent contains the same formula more than three times. We can use this with the subformula property to restrict the set of possible proofs of a sequent [or an equivalent sequent not containing the same formula more than three times] to a finite number of proofs.) We can prove that excluded middle cannot be derived in intuitionistic logic (by simply considering that any cut-free proof of "A or not A" must end with the "or-succedent" rule and noting that this would imply we had a proof of "A" or of "not A" already).
The sharpened Hauptsatz states that LK-derivations of sequents of prenex formulas can be transformed into a cut-free derivation with a quantifier-free "midsequent" so that the only inference figures below the midsequent are quantifier introduction figures and structural inference figures. So, the transformed derivation is divided into a propositional part and a quantification part. The transformation is performed by first applying the Hauptsatz to obtain a cut-free proof. Then, we remove quantifiers from basic sequents of the form "Qr F(r) -> Qr F(r)" by transforming them into the derivation from "F(a) -> F(a)" to "Qr F(r) -> Qr F(r)." The rest of the proof is transformed by a reduction of the "order" of the derivation. For each inference figure we can count the number of propositional inference figures on the path from it to the endsequent. The "order" of the derivation is the sum of these numbers for the quantification inference rules. We can reduce the order by pushing the quantification inference rules below the propositional inference rules.
Gentzen used the sharpened Hauptsatz to show the consistency of arithmetic without induction. The idea is that if the theory were inconsistent, then we could prove the sequent with the axioms of the theory in the antecedent and an empty succedent. The sharpened Hauptsatz allows us to transform such a proof into a cut-free proof with a quantifier-free midsequent. We replace all the free variables which are not the eigenvariable of exists-IA by 1. Then we replace each eigenvariable of exists-IA by an appropriate number. The resulting midsequent has an empty succedent and every formula in its antecedent is true. Such a sequent clearly cannot be derived.
Finally, Gentzen proves the equivalence of his natural deduction calculi and sequent calculi with Hilbert-style calculi. First, we consider an equivalence relation on the union of the set of formulae and the set of sequents. For example, the sequent "A1, . . ., Am -> B1, . . ., Bn" is equivalent to the formula "(A1 & . . . & Am) implies (Bn or . . . or B1)". Next we consider two proofs (from any two calculi under consideration) to be equivalent if their endsequents/endformulae are equivalent.
The Hilbert-style calculi LHJ and LHK are given axiomatically (with basic propositional and quantifier axioms) along with the inference rules modus ponens, 'implies-forall' (analogous to forall-IS), and 'exists-implies' (analogous of to exists-IA). LHK is LHJ with the law of the excluded middle included as an axiom schema.
The goal is to prove that "every LHJ-derivation can be transformed into an equivalent NJ-derivation, every NJ-derivation can be transformed into an equivalent LJ-derivation, and every LJ-derivation can be transformed into an equivalent LHJ-derivation." The classical calculi are dealt with analogously.
Transforming an LHJ-derivation into an equivalent NJ-derivation is analogous to taking a combinator to a closed lambda-term. We can derive any axiom of LHJ in system NJ (just as we can define each combinator in lambda-calculus), so we replace each occurrence of an axiom with the derivation of the axiom to obtain an NJ-derivation (just as we can replace combinators by their definitions to obtain a closed lambda-term). Note that this process also works in the classical case.
Transforming an NJ-derivation into an equivalent LJ-derivation involves replacing each occurrence of a formula B with the sequent "A1, . . ., Am -> B" where the Ai's are the assumptions above B listed from left to right. (Also, NJ-derivations may use a symbol for "false" which should be converted into "A & not A".) The inference figures of the LJ-calculus provides the tools to fill in any gaps between sequents in the resulting derivation. (Note that in the LJ-calculus we cannot have more than one formula in the antecedent. This transformation satisfies this restriction.) The classical calculus can be dealt with analogously because we can derive excluded middle in the LK-calculus (and append this derivation to any initial sequent which was transformed from a basic formula of the form "A or not A").
The most difficult transformation is from an LJ-derivation to an equivalent LHJ-derivation. The transformation is analogous to going from lambda-terms (in context--the context corresponds to the antecedent of the sequents) to combinators with variables. The full LJ-derivation corresponds to a closed lambda-term, so that the transformation will correspond to a combinator (without variables). First, most of the operational inference figures are replaced by structural inference figures (such as cut) by introducing new basic sequents (which will ultimately correspond to axioms of LHJ). Then we replace the structural inference rules by figures which can be justified by LHJ axioms. These replacements take place in a number of steps. In the end, we replace each sequent "A1, . . ., Am -> B" with the formula "(A1 & . . . & Am) implies B" and use the tools of the LHJ-calculus to fill in the gaps. This procedure can be modified (with a little more work than in the other two cases) to apply to the classical case.