Proof Theory: Second Edition

By Gaisi Takeuti

Focusing on Gentzen-type proof theory, this volume presents a detailed overview of creative works by author Gaisi Takeuti and other twentieth-century logicians. The text explores applications of proof theory to logic as well as other areas of mathematics. Suitable for advanced undergraduates and graduate students of mathematics, this long-out-of-print monograph forms a cornerstone for any library in mathematical logic and related topics.
The three-part treatment begins with an exploration of first order systems, including a treatment of predicate calculus involving Gentzen's cut-elimination theorem and the theory of natural numbers in terms of Gödel's incompleteness theorem and Gentzen's consistency proof. The second part, which considers second order and finite order systems, covers simple type theory and infinitary logic. The final chapters address consistency problems with an examination of consistency proofs and their applications.

• Language: English
• Publisher: Dover Publications
• Release date: Oct 10, 2013
• ISBN: 9780486320670

Book preview

Index

INTRODUCTION

Mathematics is a collection of proofs. This is true no matter what standpoint one assumes about mathematics—platonism, anti-platonism, intuitionism, formalism, nominalism, etc. Therefore, in investigating mathematics, a fruitful method is to formalize the proofs of mathematics and investigate the structure of these proofs. This is what proof theory is concerned with.

Proof theory was initiated by D. Hilbert in his attempt to prove the consistency of mathematics. Hilbert’s approach was later developed by the brilliant work of G. Gentzen. This textbook is devoted to the proof theory inspired by Gentzen’s work: so-called Gentzen-type proof theory.

Part I treats the proof theory of first order formal systems. Chapter 1 deals with the first order predicate calculus; Gentzen’s cut-elimination theorem plays a major role here. There are many consequences of this theorem as for example the various interpolation theorems.

We prove the completeness of the classical predicate calculus, by the use of reduction trees (following Schütte), and then we prove the completeness of the intuitionistic predicate calculus, by adapting this method to Kripke semantics.

Chapter 2 deals with the theory of natural numbers; the main topics are Gödel’s incompleteness theorem and Gentzen’s consistency proof. Since the author believes that the true significance of Gentzen’s consistency proof has not been well understood so far, a philosophical discussion is also presented in this chapter. The author believes that the Hilbert-Gentzen finitary standpoint, with Gedankenexperimenten involving finite (and concrete) operations on (sequences of) concretely given figures, is most important in the foundations of mathematics.

Part II concerns the finite order predicate calculi and infinitary languages. In Chapter 3, the semantics for finite order systems, and the cut-elimination theorem for them, due to Tait, Takahashi and Prawitz, are considered. Since the finite type calculus is not complete, and further, much of traditional mathematics can be formalized in it, we are anxious to see progress in investigating the significance of the cut-elimination theorem here. The significance of the systems with infinitary languages which are presented in Chapter 4 is that they are complete systems in which the cut-elimination theorem holds, while at the same time they are essentially second order systems. The situation is, however, quite uncertain for systems with heterogeneous quantifiers. Here we propose a basic system of heterogeneous quantifiers which seems reasonable and for which so-called weak completeness holds. It seems, however, that our system is far from complete. A system which is obtained from ours by a slight modification is closely related to the axiom of determinateness (AD). Therefore the problem of how to extend our system to a (sound and) complete system is related to the justification of the axiom of determinateness.

Let M be a transitive model of ZF + DC (the axiom of dependent choices) which contains P(ω). It has been shown that the following two statements are equivalent: (1) AD holds in M; and (2) the cut-elimination theorem holds for any M-definable determinate logic. This suggests an interesting direction for the study of infinitary languages.

Part III is devoted to consistency proofs for stronger systems on which the author has worked.

We have tried to avoid overlapping of material with other textbooks. Thus, for example, we do not present the material in K. Schütte’s Beweistheorie, although much of it is Gentzen-type proof theory. Those who wish to learn other approaches to proof theory are advised to consult G. Kreisel’s Survey of Proof Theory I and II, Journal of Symbolic Logic (1968), and Proceedings of the Second Scandinavian Logic Symposium, ed. J. E. Fenstad (North-Holland, Amsterdam, 1971), respectively. We have made special efforts to clarify our position on foundational issues. Indeed, it is our view that in the study of the foundations of mathematics (which is not restricted to consistency problems), it is philosophically important to study and clarify the structures of mathematical proofs.

Concerning the impact of foundational studies on mathematics itself, we remark that while set theory, for example, has already contributed essentially to the development of modern mathematics, it remains to be seen what influence proof theory will have on mathematics.

No attempt has been made to make the references comprehensive although some names are attached to the theorems. In addition to those given above, a few references are recommended in the course of the book.

PART I

FIRST ORDER SYSTEMS

CHAPTER 1

FIRST ORDER PREDICATE CALCULUS

In this chapter we shall present Gentzen’s formulation of the first order predicate calculus LK (logistischer klassischer Kalkül), which is convenient for our purposes. We shall also include a formulation of intuitionistic logic, which is known as LJ (logistischer intuitionistischer Kalkül). We then proceed to the proofs of the cut-elimination theorems for LK and LJ, and their applications.

§1. Formalization of statements

The first step in the formulation of a logic is to make the formal language and the formal expressions and statements precise.

DEFINITION 1.1. A first order (formal) language consists of the following symbols.

1) Constants:

1.1) Individual constants: k0, k1, …, kj, … (j = 0, 1, 2, …).

1.2) Function constants with i argument-places (i (j = 0, 1, 2, …).

1.3) Predicate constants with i argument-places (i = 0, 1, 2, …): R , R ,…, R , …(j = 0, 1, 2, …).

2) Variables:

2.1) Free variables: a0, a1, …, aj, … (j = 0, 1, 2, …).

2.2) Bound variables: x0, x1, …, xj, … (j = 0, 1, 2, …).

3) Logical symbols:

¬(not), ∧ (and), ∨ (or), ⊃ (implies), ∀ (for all) and ∀ (there exists). The first four are called propositional connectives and the last two are called quantifiers.

4) Auxiliary symbols:

(,) and, (comma).

We say that a first order language L is given when all constants are given. In every argument, we assume that a language L is fixed, and hence we omit the phrase of L.

There is no reason why we should restrict the cardinalities of various kinds of symbols to exactly X0. It is, however, a standard approach in elementary logic to start with countably many symbols, which are ordered with order type ω. Therefore, for the time being, we shall assume that the language consists of the symbols as stated above, although we may consider various other types of language later on. In any case it is essential that each set of variables is infinite and there is at least one predicate symbol. The other sets of constants can have arbitrary cardinalities, even 0.

We shall use many notational conventions. For example, the superscripts in the symbols of 1.2) and 1.3) are mostly omitted and the symbols of 1) and 2) may be used as meta-symbols as well as formal symbols. Other letters such as g, h, … may be used as symbols for function constants, while a, b, c, … may be used for free variables and x, y, z, … for bound variables.

Any finite sequence of symbols (from a language L) is called an expression (of L).

DEFINITION 1.2. Terms are defined inductively (recursively) as follows:

1) Every individual constant is a term.

2) Every free variable is a term.

3) If ƒi is a function constant with i argument-places and t1, …, ti are terms, then ƒi(t1, …, ti) is a term.

4) Terms are only those expressions obtained by 1)–3). Terms are often denoted by ƒ,(t, s, t1, ….

Since in proof theory inductive (recursive) definitions such as Definition 1.2 often appear, we shall not mention it each time. We shall normally omit the last clause which states that the objects which are being defined are only those given by the preceding clauses.

DEFINITION 1.3. If Ri is a predicate constant with i argument-places and t1, …, ti are terms, then Ri(t1, …, ti) is called an atomic formula. Formulas and their outermost logical symbols are defined inductively as follows:

1) Every atomic formula is a formula. It has no outermost logical symbol.

2) If A and B are formulas, then (¬A), (A ∧ B), (A ∨ B) and (A ⊃ B) are formulas. Their outermost logical symbols are ¬, ∧, ∨ and ⊃, respectively.

3) If A is a formula, a is a free variable and x is a bound variable not occurring in A, then ∀x A′ and ∃x A′ are formulas, where A′ is the expression obtained from A by writing x in place of a at each occurrence of a in A. Their outermost logical symbols are ∀ and ∃, respectively.

4) Formulas are only those expressions obtained by 1)–3).

Henceforth, A, B, C, …, F, G, … will be metavariables ranging over formulas. A formula without free variables is called a closed formula or a sentence. A formula which is defined without the use of clause 3) is called quantifier-free. In 3) above, A′ is called the scope of ∀x and ∃x, respectively.

When the language L is to be emphasized, a term or formula in the language L may be called an L-term or L-formula, respectively.

REMARK. Although the distinction between free and bound variables is not essential, and is made only for technical convenience, it is extremely useful and simplifies arguments a great deal. This distinction will, therefore, be maintained unless otherwise stated.

It should also be noticed that in clause 3) of Definition 1.3, x must be a variable which does not occur in A. This eliminates expressions such as ∀x (C(x) ∧ ∃x B(x)). This restriction does not essentially narrow the class of formulas, since e.g. this expression ∀x (C(x) ∧ ∃x B(x)) can be replaced by ∀y (C(y) ∧ ∃x B(x)), preserving the meaning. This restriction is useful in formulating formal systems, as will be seen later.

In the following we shall omit parentheses whenever the meaning is evident from the context. In particular the outermost parentheses will always be omitted. For the logical symbols, we observe the following convention of priority: the connective ¬ takes precedence over each of ∧ and ∨, and each of ∧ and ∨ takes precedence over ⊃. Thus ¬A ∧ B is short for (¬A) ∧ B, and A ∧ B ⊃ C ∨ D is short for (A ∧ B) ⊃ (C ∨ D). Parentheses are omitted also in the case of double negations: for example ¬¬A abbreviates ¬(¬A). A ≡ B will stand for (A ⊃ B) ∧ (B ⊃ A).

DEFINITION 1.4. Let A be an expression, let τ1, …, τn be distinct primitive symbols, and let σ1…, σn be any symbols. By

we mean the expression obtained from A by writing σ1 …, σn in place of τ1, …, τn, respectively, at each occurrence of τ1 …, τn (where these symbols are replaced simultaneously). Such an operation is called the (simultaneous) replacement of (τ1, …, τn) by (σ1, …, σn) in A. It is not required that τ1, …, τn actually occur in A.

PROPOSITION 1.5. (1) If A contains none of τ1, …, τn, then

is A itself.

(2) If σ1, …, σn are distinct primitive symbols, then

is identical with

DEFINITION 1.6. (1) Let A be a formula and t1, …, tn be terms. If there is a formula B and n distinct free variables b1, …, bn such that A is

then for each i i n) the occurrences of ti resulting from the above replacement are said to be indicated in A, and this fact is also expressed (less accurately) by writing B as B(b1, …, bn), and A as B(t1, …, tn). A may of course contain some other occurrences of ti; this happens if B contains ti.

(2) We say that a term t is fully indicated in A, or every occurrence of t in A is indicated, if every occurrence of t is obtained by such a replacement (from some formula B as above, with n = 1 and t = t1).

It should be noted that the formula B and the free variables from which A can be obtained by replacement are not unique; the indicated occurrences of some terms of A are specified relative to such a formula B and such free variables.

PROPOSITION 1.7. If A(a) is a formula (in which a is not necessarily fully indicated) and x is a bound variable not occurring in A(a), then ∀x A(x) and ∃x A(x) are formulas.

PROOF. By induction on the number of logical symbols in A(a).

In the following, let Greek capital letters Γ, Δ, II, Λ, Γ0, Γ1, … denote finite (possibly empty) sequences of formulas separated by commas. In order to formulate the sequential calculus, we must first introduce an auxiliary symbol →.

DEFINITION 1.8. For arbitrary Γ and Δ in the above notation, Γ → Δ is called a sequent. Γ and Δ are called the antecedent and succedent, respectively, of the sequent and each formula in Γ and Δ is called a sequent-formula.

Intuitively, a sequent A1, …, Am → B1, …, Bn (where m, n 1) means: if A1 ∧ … ∧ Am, then B1 ∨ … ∨ Bn. For m 1, A1, …, Am → means that A1 ∧ … ∧ Am yields a contradiction. For n B1, …, Bn means that B1 ∨ ̷ ∨ Bn holds. The empty sequent → means there is a contradiction. Sequents will be denoted by the letter S, with or without subscripts.

§2. Formal proofs and related concepts

DEFINITION 2.1 . An inference is an expression of the form

where S1, S2 and S are sequents. S1 and S2 are called the upper sequents and S is called the lower sequent of the inference.

Intuitively this means that when S1 (S1 and S2) is (are) asserted, we can infer S from it (from them). We restrict ourselves to inferences obtained from the following rules of inference, in which A, B, C, D, F(a) denote formulas.

1) Structural rules:

1.1) Weakening:

D is called the weakening formula.

1.2) Contraction:

1.3) Exchange:

We will refer to these three kinds of inferences as weak inferences, while all others will be called strong inferences.

1.4) Cut:

D is called the cut formula of this inference.

2) Logical rules:

.

D and ¬D are called the auxiliary formula and the principal formula, respectively, of this inference.

.

.

C and D are called the auxiliary formulas and C ∧ D is called the principal formula of this inference.

.

.

C and D are called the auxiliary formulas and C ∨ D the principal formula of this inference.

;

.

C and D are called the auxiliary formulas and C ⊃ D the principal formula.

2.1)–2.4) are called propositional inferences.

,

where t is an arbitrary term, and a does not occur in the lower sequent. F(t) and F(a) are called the auxiliary formulas and ∀xF(x) the principal formula. The a in ∀: right is called the eigenvariable of this inference.

Note that in ∀: right all occurrences of a in F(a) are indicated. In ∀: left,

F(t) and F(x) are

respectively (for some free variable a), so not every t in F(t) is necessarily indicated.

,

where a does not occur in the lower sequent, and t is an arbitrary term.

F(a) and F(t) are called the auxiliary formulas and ∃x F(x) the principal formula. The a in ∃: left is called the eigenvariable of this inference.

Note that in ∃: left a is fully indicated, while in ∃: right not necessarily every t is indicated. (Again, F(t) is (F(a) for some a.)

2.5) and 2.6) are called quantifier inferences. The condition, that the eigenvariable must not occur in the lower sequent in ∀: right and ∃: left, is called the eigenvariable condition for these inferences.

A sequent of the form A → A is called an initial sequent, or axiom.

We now explain the notion of formal proof, i.e., proof in LK.

DEFINITION 2.2. A proof P (in LK), or LK-proof, is a tree of sequents satisfying the following conditions:

1) The topmost sequents of P are initial sequents.

2) Every sequent in P except the lowest one is an upper sequent of an inference whose lower sequent is also in P.

The following terminology and conventions will be used in discussing formal proofs in LK.

DEFINITION 2.3. From Definition 2.2, it follows that there is a unique lowest sequent in a proof P. This will be called the end-sequent of P. A proof with end-sequent S is called a proof ending with S or a proof of S. A sequent S is called provable in LK, or LK-provable, if there is an LK-proof of it. A formula A is called LK-provable (or a theorem of LK) if the sequent → A is LK-provable. The prefix "LK- will often be omitted from LK-proof and LK-provable".

A proof without the cut rule is called cut-free.

. Thus, for example,

denote a proof of S, and a proof of S from S1 and S2, respectively. Proofs are mostly denoted by letters P, Q,…. An expression such as P(a) means that all the occurrences of a in P are indicated. (Of course such notation is useful only when replacement of a by another term is being considered.) Then P(t) is the result of replacing all occurrences of a in P(a) by t.

Let us consider some slightly modified rules of inference, e.g.,

This is not a rule of inference of LK. However, from the two upper sequents we can infer the lower sequent in LK using several structural inferences and an ∧ : right:

Conversely, from the sequents Γ → Δ, A and Γ → Δ, B we can infer Γ → Δ, A, ∧ B using several structural inferences and an instance of the inference-schema J:

Thus we may regard J as an abbreviation of (*) above. In such a case we will use the notation

As in this example we often indicate abbreviation of several steps by double lines.

Another remark we wish to make here is that the restriction on bound variables (in the definition of formulas) prohibits an unwanted inference such as

In our system this can never happen, since ∃x ∃x (A(x) ∧ B(x)) is not a formula.

The quantifier-free part of LK, that is, the subsystem of LK which does not involve quantifiers, is called the propositional calculus.

EXAMPLE 2.4. The following are LK-proofs.

1)

2) Suppose that a is fully indicated in F(a).

It should be noted that the lower sequent of ∀ : right does not contain the eigenvariable a.

EXERCISE 2.5. Prove the following in LK.

1) A ∨ B = ¬(¬ A ∧ ¬B).

2) A ⊃ B ≡ ¬ A ∨ B.

3) ∃x F(x) ≡ ¬∀y ¬F(y).

4) ¬∀y F(y) ≡ ∃x ¬F(x).

5) ¬(A ∧ B) ≡ ¬A ∨ ¬B.

EXERCISE 2.6. Prove the following in LK.

1) ∃x (A ⊃ B(x)) ≡ A ⊃ ∃x B(x).

2) ∃x (A(x) ⊃ B) ≡ ∀x A(x) ⊃ B, where B does not contain x.

3) ∃x (A(x) ⊃ B(x)) ≡ ∀x A(x) ⊃ ∃x B(x).

4) ¬A ⊃ B → ¬B ⊃ A.

5) ¬A ⊃ ¬B → B ⊃ A.

EXERCISE 2.7. Construct a cut-free proof of ∀x A(x) ⊃ B → ∃x (A(x) ⊃ B), where A(a) and B are atomic and distinct.

DEFINITION 2.8. (1) When we consider a formula, term or logical symbol together with the place that it occupies in a proof, sequent or formula respectively, we refer to it as a formula, term or logical symbol in the proof, sequent or formula, respectively.

(2) A sequence of sequents in a proof P is called a thread (of P) if the following conditions are satisfied:

2.1) The sequence begins with an initial sequent and ends with the end-sequent.

2.2) Every sequent in the sequence except the last is an upper sequent of an inference, and is immediately followed by the lower sequent of this inference.

(3) Let S1, S2 and S3 be sequents in a proof P. We say S1 is above S2 or S2 is below S1 (in P) if there is a thread containing both S1 and S2 in which S1 appears before S2. If S1 is above S2 and S2 is above S3, we say S2 is between S1 and S3.

(4) An inference in P is said to be below a sequent S (in P) if its lower sequent is below S.

(5) Let P be a proof. A part of P which itself is a proof is called a subproof of P. This can also be described as follows. For any sequent S in P, that part of P which consists of all sequents which are either S itself or which occur above S, is called a subproof of P (with end-sequent S).

(6) Let P0 be a proof of the form

where (*) denotes the part of P0 under Γ → Θ, and let Q be a proof ending with Γ, D → Θ. By a copy of P0 from Q we mean a proof P of the form

where (**) differs from (*) only in that for each sequent in (*), say II → Λ, the corresponding sequent in (**) has the form II, D → Λ. That is to say, P is obtained from P0 by replacing the subproof ending with Γ → Θ by Q, and adding an extra formula D to the antecedent of each sequent in (*). Likewise, a copy can be defined for the case of an extra formula in the succedent. We can also extend the definition to the case where there are several of these formulas.

The precise definition can be carried out by induction on the number of inferences in (*). However this notion is intuitive, simple, and will appear often in this book.

(7) Let S(a), or Γ(a) → Δ(a), denote a sequent of the form A1 (a),…, Am (a) → B(a),…, Bn(a). Then S(t), or Γ(t)→ Δ(t), denotes the sequent A1(t),…, Am(t)→ B1(t),…, Bn(t).

We can define: t is fully indicated in S(t), or Γ(t) → Γ(t), by analogy with Definition 1.6.

In order to prove a basic property of provability, i.e., that provability is preserved under substitution of terms for free variables, we shall first list some lemmas, which themselves assert basic properties of proofs. We first define an important concept.

DEFINITION 2.9. A proof in LK is called regular if it satisfies the condition that firstly, all eigenvariables are distinct from one another, and secondly, if a free variable a occurs as an eigenvariable in a sequent S of the proof, then a occurs only in sequents above S.

LEMMA 2.10. (1) Let Γ(a) → Δ(a) be an (LK-) provable sequent in which a is fully indicated, and let P(a) be a proof of Γ(a) → Δ(a). Let b be a free variable not occurring in P(a). Then the tree P(b), obtained from P(a) by replacing a by b at each occurrence of a in P(a), is also a proof and its end-sequent is Γ(b) → Δ(b).

(2) For an arbitrary LK-proof there exists a regular proof of the same end-sequent. Moreover, the required proof is obtained from the original proof simply by replacing free variables (in a suitable way).

PROOF. (1) By induction on the number of inferences in P(a). If P(a) consists of simply an initial sequent A(a) → A(a), then P(b) consists of the sequent A(b)→ A(b), which is also an initial sequent. Let us suppose that our proposition holds for proofs containing at most n inferences and suppose that P(a) contains n + 1 inferences. We treat the possible cases according to the last inferences in P(a). Since other cases can be treated similarly, we consider only the case where the last inference, say J, is a ∀: right. Suppose the eigenvariable of J is a, and P(a) is of the form

where Q(a) is the subproof of P(a) ending with Γ → Λ, A(a). It should be remembered that a does not occur in Γ, Λ or A(x). By the induction hypotheses the result of replacing all a’s in Q(a) by b is a proof whose end-sequent is Γ→ Λ, A(b). Γ and Λ contain no b’s. Thus we can apply a ∀ : right to this sequent using b as its eigenvariable:

and so P(b) is a proof ending with Γ → Λ, ∀x A(x). If a is not the eigenvariable of J, P(a) is of the form

By the induction hypothesis the result of replacing all a’s in Q(a) by b is a proof and its end-sequent is Γ(b)→ Λ(b), A(b, c).

Since by assumption b does not occur in P(a), b is not c, and so we can apply a ∀ : right to this sequent, with c as its eigenvariable, and obtain a proof P(b) whose end-sequent is Γ(b)→ Λ(b), ∀x A(b, x).

(2) By mathematical induction on the number l of applications of ∀ : right and ∃ : left in a given proof P. If l = 0, then take P itself. Otherwise, P can be represented in the form:

where Pi is a subproof of P of the form

and Ii is a lowermost ∀ : right or ∀ : left in P (i = 1,…, k), i.e., there is no ∀ : right or ∃ : left in the part of P denoted by (*).

Let us deal with the case where Ii is ∀ : right. Pi has fewer applications of ∀ : right or ∃ : left than Pof Γi→ Δi, Fi(bi). Note that no free variable in Γi→ Δi, F(bi) (including bi. Suppose c1,…, cm are all the eigenvariables in all the Pi’S which occur in P above Γi → Δi, ∀yi Fi(yi), i = 1,…, k. Then change c1,…, cm to d1,…, dm, respectively, where d1, …, dm are the first m variables which occur neither in P , i = 1,…, k. If bi occurs in P below Γi → Δi, ∀yi, Fi(yi), then change it to dm + i.

be the proof which is obtained from P are each regular. P′ is defined to be

where (*) is the same as in P, except for the replacement of bi by dm + i. This completes the proof.

From now on we will assume that we are dealing with regular proofs whenever convenient, and will not mention it on each occasion.

By a method similar to that in Lemma 2.10 we can prove the following.

LEMMA 2.11. Let t be an arbitrary term. Let Γ(a) Δ(a) be a provable (in LK) sequent in which a is fully indicated, and let P(a) be a proof ending with Γ(a)→ Δ(a) in which every eigenvariable is different from a and not contained in t. Then P(t) (the result of replacing all a’s in P(a) by t) is a proof whose end-sequent is Γ(t)→ Δ(t).

LEMMA 2.12. Let t be an arbitrary term, Γ(a)→ Δ(a) a provable (in LK) sequent in which a is fully indicated, and P(a) a proof of Γ(a)→ Δ(a). Let P′(a) be a proof obtained from P(a) by changing eigenvariables (not necessarily replacing distinct ones by distinct ones) in such a way that in P′(a) every eigenvariable is different from a and not contained in t. Then P′(t) is a proof of Γ(t)→ Δ(t).

PROOF. By induction on the number of eigenvariables in P(a) which are either a or contained in t, using Lemmas 2.10 and 2.11.

We rewrite part of Lemma 2.11 as follows.

PROPOSITION 2.13. Let t be an arbitrary term and S(a) a provable (in LK) sequent in which a is fully indicated. The S(t) is also provable.

We will point out a simple, but useful fact about the formal proofs of our system, which will be used repeatedly.

PROPOSITION 2.14. If a sequent is provable, then it is provable with a proof in which all the initial sequents consist of atomic formulas. Furthermore, if a sequent is provable without cut, then it is provable without cut with a proof of the above sort.

PROOF. It suffices to show that for an arbitrary formula A, A→ A is provable without cut, starting with initial sequents consisting of atomic formulas. This, however, can be easily shown by induction on the complexity of A.

DEFINITION 2.15. We say that two formulas A and B are alphabetical variants (of one another) if for some x1, …, xn, y1,…, yn

is

where z1,…, zn are bound variables occurring neither in A nor in B: that is to say, if A and B are different, it is only because they have a different choice of bound variables. The fact that A and B are alphabetical variants will be expressed by A ∼ B.

One can easily prove that the relation A ∼ B is an equivalence relation. Intuitively it is obvious that changing bound variables in a formula does not change its meaning. We can prove by induction on the number of logical symbols in A that if A ∼ B, then A ≡ B is provable without cut (indeed in LJ, which is to be defined in the next section). Thus two alphabetical variants will often be identified without mention.

§3. A formulation of intuitionistic predicate calculus

DEFINITION 3.1. We can formalize the intuitionistic predicate calculus as a sub-system of LK, which we call LJ, following Gentzen. (J stands for intuitionistic.) LJ is obtained from LK by modifying it as follows (cf. Definitions 2.1 and 2.2 for LK):

1) A sequent in LJ is of the form Γ → Δ, where Δ consists of at most one formula.

2) Inferences in LJ are those obtained from those in LK by imposing the restriction that the succedent of each upper and lower sequent consists of at most one formula; thus there are no inferences in LJ corresponding to contraction : right or exchange : right.

The notions of proof, provable and other concepts for LJ are defined similarly to the corresponding notions for LK.

Every proof in LJ is obviously a proof in LK, but the converse is not true. Hence:

PROPOSITION 3.2. If a sequent S of LJ is provable in LJ, then it is also provable in LK.

Lemmas 2.10–2.12 and Propositions 2.13 and 2.14 hold, reading "LJ-provable in place of provable or provable (in LK)". We shall refer to these results (for LJ) as Lemma 3.3, Lemma 3.4, Lemma 3.5, Proposition 3.6 and Proposition 3.7, respectively. We omit the statements of these.)

EXAMPLE 3.8. The following are LJ-proofs.

1)

2) Suppose a is fully indicated in F(a).

EXERCISE 3.9. Prove the following in LJ.

1) ¬A ∨ B → A ⊃ B).

2) ∃x F(x) → ¬ ∀y ¬ F(y).

3) A ∧ B → A.

4) A → A ∧ B.

5) ¬A ∧ ¬B → ¬(A ∧ B).

6) ¬(A ∨ B) ≡ ¬A ∧ ¬B.

7) (A ∨ C) ∧ (B ∨ C) ≡ (A ∧ B) ∨ C.

8) ∃x ¬F(x) → ¬∀x F(x).

9) ∀x(F(x)∧ G(x))≡ ∀x F(x) ∧ ∀x G(x).

10) A⊃ ¬ B → B⊃ ¬A.

11) ∃x(A⊃B(x))→A⊃∃xB(x).

12) ∃x(A(x)⊃B)→∀x(x)⊃B.

13) ∃x(A(x)⊃B(x))→ ∀x A(x)⊃∃xB(x).

EXERCISE 3.10. Prove the following in LJ.

1) ¬ ¬(A⊃B), A→ ¬ ¬ B.

2) ¬ ¬ B ⊃B,¬ ¬ (A⊃B) → A ⊃B.

3) ¬ ¬ A ≡ ¬ A.

EXERCISE 3.11. Define LJ′ to be the system which is obtained from LJ by adding to it, as initial sequents, all sequents ¬ ¬ R→ R, where R is atomic. Let A be a formula which does not contain ∨ or ∃. Then ¬ ¬ A→ A is LJ′-provable. [Hint: By induction on the number of logical symbols in A; cf. Exercise 3.10.]

PROBLEM 3.12. For every formula A define A* as follows.

1) If A is atomic, then A* is ¬¬ A.

2) If A is one of the forms ¬ B, B ∧ C, B ∨ C or B ⊃ C, then A* is ¬B*, B* ∧ C*, ¬(¬B* ∧ ¬ C*) or B* ⊃ C*, respectively.

3) If A is of the form ∀xF(x) or ∃x F(x), then A* is ∀x F*(x) or ¬∀ x¬F*(x), respectively.

(Thus A* does not contain ∨ or ∃.) Prove that for any A, A is LK-provable if and only if A* is LJ-provable. [Hint: Follow the prescription given below.]

1) For any A, A= A* is LK-provable.

2) Let S be a sequent of the form Al …, Am→ Bl …, Bn. Let S′ be the sequent

Prove that S is LK-provable if and only if S′ is LK-provable.

3) A* = ¬¬A* in LJ, from Exercise 3.11.

4) Show that if S is LK-provable, then S′ is LJ-provable. (Use mathematical induction on the number of inferences in a proof of S.)

What must be proved is now a special case of 4).

§4. Axiom systems

DEFINITION 4.1. The basic system is LK.

of sentences is called an axiom system, and each of these sentences is called an axiom . Sometimes an axiom system is called a theory. (Of course this definition is only significant in certain contexts.)

is called an axiom sequence .

3) If there exists an axiom sequence Γ0 such that Γ0, Γ → Δ is LK-provable, then Γ→Δ is said to be provable from (in LK, Γ→Δ.

is inconsistent (with LK(in LK).

is not inconsistent (with LK), then it is said to be consistent (with LK).

, then A is said to be dependent on .

7) A sentence A is said to be consistent (inconsistent) if the axiom system {A} is consistent (inconsistent).

8) LK is the system obtained from LK .

9) LK is said to be inconsistent if → is LK -provable, otherwise it is consistent.

The following propositions, which are easily proved, will be used quite often.

PROPOSITION 4.2. Let be an axiom system. Then the following are equivalent:

is inconsistent (with LK) (as defined above);

(b) for every formula A (of the language), A is provable from ;

(c) for some formula A, A and ¬ A are both provable from .

PROPOSITION 4.3. Let be an axiom system. Then a sequent Γ→Δ is LK -provable if and only if Γ→Δ is provable from si (in LK).

COROLLARY 4.4. An axiom system si is consistent (with LK) if and only if LK is consistent.

These definitions and the propositions hold also for LJ.

§5. The cut-elimination theorem

A very important fact about LK is the cut-elimination theorem, also known as Gentzen’s Hauptsatz:

THEOREM 5.1 (the cut-elimination theorem: Gentzen). If a sequent is (LK)-provable, then it is (LK-) provable without a cut.

This means that any theorem in the predicate calculus can be proved without detours, so to speak. We shall come back to this point later. The purpose of the present section is to prove this theorem. We shall follow Gentzen’s original proof.

First we introduce a new rule of inference, the mix rule, and show that the mix rule and the cut rule are equivalent. Let A be a formula. An inference of the following form is called a mix (with respect to A):

where both Δ and Π contain the formula A, and Δ* and Π* are obtained from Δ and Π respectively by deleting all the occurrences of A in them. We call A the mix formula of this inference, and the mix formula of a mix is normally indicated in parentheses (as above).

Let us call the system which is obtained from LK by replacing the cut rule by the mix rule, LK*. The following is easily proved.

LEMMA 5.2. LK and LK* are equivalent, that is, a sequent S is LK-provable if and only if S is LK*-provable.

By virtue of the Lemma 5.2, it suffices to show that the mix rule is redundant in LK*, since a proof in LK* without a mix is at the same time a proof in LK without a cut.

THEOREM 5.3 (cf. Theorem 5.1). If a sequent is provable in LK*, then it is provable in LK* without a mix.

This theorem is an immediate consequence of the following lemma.

LEMMA 5.4. If P is a proof of S (in LK*) which contains (only) one mix, occurring as the last inference, then S is provable without a mix.

The proof of Theorem 5.3 from Lemma 5.4 is simply by induction on the number of mixes occurring in a proof of S.

The rest of this section is devoted to proving Lemma 5.4. We first define two scales for measuring the complexity of a proof. The grade of a formula A (denoted by g(A)) is the number of logical symbols contained in A. The grade of a mix is the grade of the mix formula. When a proof P has a mix (only) as the last inference, we define the grade of P (denoted by g(P)) to be the grade of this mix.

Let P be a proof which contains a mix only as the last inference:

We refer to the left and right upper sequents as S1 and S2, respectively, and to the lower sequent as S. We call a thread in P a left (right) thread if it contains the left (right) upper sequent of the mix J. The rank in P is the number of consecutive sequents, counting upward from the left (right) upper sequent of J, that contains the mix formula in its succedent (antecedent). Since the left (right) upper sequent always contains the mix formula, the rank of a thread in P in P ; P). We define

ranges over all the left threads in P, and

ranges over all the right threads in P. The rank of P, rank(P), is defined as

Notice that rank(P2.

PROOF OF LEMMA 5.4. We prove the Lemma by double induction on the grade g and rank r of the proof P (i.e., transfinite induction on ω · g + r). We divide the proof into two main cases, namely r = 2 and r > 2 (regardless of g).

Case 1: r = 2, viz. rankl(P) = rankr(P) = 1.

We distinguish cases according to the forms of the proofs of the upper sequents of the mix.

1.1) The left upper sequent S1 is an initial sequent. In this case we may assume P is of the form

We can then obtain the lower sequent without a mix:

1.2) The right upper sequent S2 is an initial sequent. Similarly:

1.3) Neither S1 nor S2 is an initial sequent, and S1 is the lower sequent of a structural inference J1. Since rankl(P) = 1, the formula A cannot appear in the succedent of the upper sequent of J1 i.e., J1 must be weakening: right, whose weakening formula is A:

where Δ1 does not contain A. We can eliminate the mix as follows:

1.4) None of 1.1)–1.3) holds but S2 is the lower sequent of a structural inference. Similarly:

1.5) Both S1 and S2 are the lower sequents of logical inferences. In this case, since rankl(P) = rankr(P) = 1, the mix formula on each side must be the principal formula of the logical inference. We use induction on the grade, distinguishing several cases according to the outermost logical symbol of A. We treat here two cases and leave the others to the reader.

(i) The outermost logical symbol of A is ∧ . In this case S1 and S2 must be the lower sequents of ∧ : right and ∧ : left, respectively:

where by assumption none of the proofs ending with Γ→Δ1, B; Γ→Δ1, C or B, Π1→Λ contain a mix. Consider the following:

and Δ are obtained from Π1 and Δ1 by omitting all occurrences of B. This proof contains only one mix, a mix that occurs as its last inference. Furthermore the grade of the mix formula B is less than g(A) (= g(B ∧ C)). So by the induction hypothesis we can obtain a proof which contains no mixes and whose end-sequent is Γ→ Δ , Λ. From this we can obtain a proof without a mix with end-sequent Γ, Π1 → Δ1, Λ.

(ii) The outermost logical symbol of A is ∀. So A is of the form ∀x F(x) and the last part of P has the form:

(a being fully indicated in F(a)). By the eigenvariable condition, a does not occur Γ,Δ1 or F(x). Since by assumption the proof ending with Γ→Δ1, F(a) contains no mix, we can obtain a proof without a mix, ending with Γ→Δ1, F(t) (cf. Lemma 2.12). Consider now

and Δ are obtained from Π1 and Δ1 by omitting all occurrences of F(t). This has only one mix. It occurs as the last inference and the grade of the mix formula is less than g(A). Thus by the induction hypothesis we can eliminate this mix and obtain a proof ending with Γ→ Δ , Λ,from which we can obtain a proof, without a mix, ending with Γ, Π1→Δ1, Λ.

Case 2. r > 2, i.e., rankl(P)> 1 and/or rankr(P) > 1.

The induction hypothesis is that from every proof Q which contains a mix only as the last inference, and which satisfies either g(Q) < g(P), or g(Q) = g(P) and rank(Q) < rank(P), we can eliminate the mix.

2.1) rankr(P) > 1.

2.1.1) Γor Δ (in S1) contains A. Construct a proof as follows.

2.1.2) S2 is the lower sequent of an inference J2, where J2 is not a logical inference whose principal formula is A. The last part of P looks like this:

where the proofs of Γ→Δ and Φ → Ψ contain no mixes and Φ contains at least one A. Consider the following proof P′:

In P′, the grade of the mix is equal to g(P), rankl(P′) = rankl(P) and rankr(P′) = rankr(P) – 1. Thus by the induction hypothesis, Γ, Φ* → Δ* Ψ is provable without a mix. Then we construct the proof

In case that the auxiliary formula in J2 in P is a mix in Φ, we need an additional weakening before J2 in the new proof.

2.1.3) Γ contains no A’s, and S2 is the lower sequent of a logical inference whose principal formula is A. Although there are several cases according to the outermost logical symbol of A, we treat only two examples here and leave the rest to the reader.

(i) A is B ⊃ C. The last part of P is of the form:

Consider the following proofs P1 and P2:

assuming that B ⊃ C is in Π1 and Π2. If B ⊃ C is not in Πi (i is Πi, and Pi is defined as follows.

Note that g(P1) = g(P2) = g(P), rankl(P1) = rankl(P2) = rankl(P) and rankr(P1) = rankr(P2) = rankr(P) – 1. Hence by the induction hypothesis, the end-sequents of P1 and P2 are provable without a mix (say by P and P ). Consider the following proof P′:

Then g(P′) = g(P), rankl(P′) = rankl(P), rankr(P′) = 1, for Γ contains no occurrences of B ⊃ C and rank(P′) < rank(P). Thus the end-sequent of P′ is provable without a mix by the induction hypothesis, and hence so is the end-sequent of P.

(ii) A is ∃x F(x). The last part of P looks like this:

Let b be a free variable not occurring in P. Then the result of replacing a by b throughout the proof ending with F(a), ∏1 → Λ is a proof, without a mix, ending with F(b), ∏1 → Λ since by the eigenvariable condition, a does not occur in Π1 or Λ (cf. Lemma 2.11).

Consider the following proof:

By the induction hypothesis, the end-sequent of this proof can be proved without a mix (say by P′). Now consider the proof

where b occurs in none of ∃x F(x), Γ, Π1, Δ, Λ. This mix can then also be eliminated, by the induction hypothesis.

2.2) rankr(P) = 1 (and rankl(P) > 1).

This case is proved in the same way as 2.1) above.

This completes the proof of Lemma 5.4 and hence of the cut-elimination theorem.

It should be emphasized that the proof is constructive, i.e., a new proof is effectively constructed from the given proof in Lemma 5.2 and again in Lemma 5.4, and hence in Theorem 5.1.

The cut-elimination theorem also holds for LJ. Actually the above proof is designed so that it goes through for LJ without essential changes: we only have to keep in mind that there can be at most one formula in each succedent. The details are left to the reader; we simply state the theorem.

THEOREM 5.5. The cut-elimination theorem holds for LJ.

§6. Some consequences of the cut-elimination theorem

There are numerous applications of the cut-elimination theorem, some of which will be listed in this section, others as exercises. In order to facilitate discussion of this valuable, productive and important theorem, we shall first define the notion of subformula, which will be used often.

DEFINITION 6.1. By a subformula of a formula A we mean a formula used in building up A. The set of subformulas of a formula is inductively defined as follows, by induction on the number of logical symbols in the formula.

(1) An atomic formula has exactly one subformula, viz. the formula itself. The subformulas of ¬ A are the subformulas of A and ¬A itself.The subformulas of A ∧ B or A ∨ B or A⊃ B are the subformulas of A and of B, and the formula itself. The subformulas of ∀xA(x) or ∃x A(x) are the subformulas of any formula of the form A(t), where t is an arbitrary term, and the formula itself.

(2) Two formulas A and B are said to be equivalent in LK if A ≡ B is provable in LK.

(3) We shall say that in a formula A , is in the scope of an occurrence of a logical symbol, say #, if in the construction of A is the outermost logical symbol precedes the stage where # is the outermost logical symbol (cf. Definition 1.3). Further, a symbol # is said to be in the left scope of a ⊃ if ⊃ occurs in the form B ⊃ C and # occurs in B.

(4) A formula is called prenex (in prenex form) if no quantifier in it is in the scope of a propositional connective. It can easily be seen that any formula is equivalent (in LK) to a prenex formula, i.e., for every formula A there is a prenex formula B such that A ≡ B is LK-provable.

One can easily see that in any rule of inference except a cut, the lower sequent is no less complicated than the upper sequent(s); more precisely, every formula occurring in an upper sequent is a subformula of some formula occurring in the lower sequent (but not necessarily conversely). Hence a proof without a cut contains only subformulas of the formulas occurring in the end-sequent (the subformula property). So the cut-elimination theorem tells us that if a formula is provable in LK (or LJ) at all, it is provable by use of its subformulas only. (This is what we meant by saying that a theorem in the predicate calculus could be proved without detours.)

From this observation, we can convince ourselves that the empty sequent → is not LK- (or LJ-) provable. This leads us to the consistency proof of LK and LJ.

THEOREM 6.2 (consistency). LK and LJ are consistent.

PROOF. Suppose → were provable in LK (or LJ). Then, by the cut-elimination theorem, it would be provable in LK (or LJ) without a cut. But this is impossible, by the subformula property of cut-free proofs.

An examination of the proof of this theorem (including the cutelimination theorem) shows that the consistency of LK (and LJ) was proved by quantifier-free induction on the ordinal ω². We shall not, however, go into the details of the consistency problem at this stage.

For convenience, we re-state the subformula property of cut-free proofs as a theorem.

THEOREM 6.3. In a cut-free proof in LK (or LJ) all the formulas which occur in it are subformulas of the formulas in the end-sequent.

PROOF. By mathematical induction on the number of inferences in the cut-free proof.

In the rest of this section, we shall list some typical consequences of the cut-elimination theorem. Although some of the results are stated for LJ as well as LK, we shall give proofs only for LK; those for LJ are left to the reader.

THEOREM 6.4 (1) (Gentzen’s midsequent theorem for LK). Let S be a sequent which consists of prenex formulas only and is provable in LK. Then there is a cut-free proof of S which contains a sequent (called a midsequent), say S′, which satisfies the following:

1. S′ is quantifier-free.

2. Every inference above S′ is either structural or propositional.

3. Every inference below S′ is either structural or a quantifier inference.

Thus a midsequent splits the proof into an upper part, which contains the propositional inferences, and a lower part, which contains the quantifier inferences.

(2) (The midsequent theorem for LJ without ∨ : left.) The above holds reading "LJ without ∨ : left" in place of "LK".

PROOF (outline). Combining Proposition 2.14 and the cut-elimination theorem, we may assume that there is a cut-free proof of S, say P, in which all the initial sequents consist of atomic formulas only. Let I be a quantifier inference in P. The number of propositional inferences under I is called the order of I. The sum of the orders for all the quantifier inferences in P is called the order of P. (The term order is used only temporarily here.) The proof is carried out by induction on the order of P.

Case 1: The order of a proof P is 0. If there is a propositional inference, take the lowermost such, and call its lower sequent S0. Above this sequent there is no quantifier inference. Therefore, if there is a quantifier in or above S0, then it is introduced by weakenings. Since the proof is cut-free, the weakening formula is a subformula of one of the formulas in the end-sequent. Hence no propositional inferences apply to it. We can thus eliminate these weakenings and obtain a sequent S corresponding to S0. By adding some weakenings under S (if necessary), we derive S, and S serves as the mid-sequent.

If there is no propositional inference in P, then take the uppermost quantifier inference. Its upper sequent serves as a midsequent.

Case 2: The order of P is not 0. Then there is at least one propositional inference which is below a quantifier inference. Moreover, there is a quantifier inference I with the following property: the uppermost logical inference under I is a propositional inference. Call it I′. We can lower the order by interchanging the positions of I and I′. Here we present just one example: say I is ∀ : right.

where the (*)-part of P contains only structural inferences and Λ contains ∀xF(x) as a sequent-formula. Transform P into the following proof P′:

It is obvious that the order of P′ is less than that of P.

Prior to the next theorem, Craig’s interpolation theorem*, we shall first state and prove a lemma which itself can be regarded as an interpolation theorem for provable sequents and from which the original form of the interpolation theorem follows immediately. We shall present the argument for LK only, although everything goes through for LJ as well.

For technical reasons we introduce the predicate symbol T, with 0 argument places, and admit → T as an additional initial sequent. (T stands for true.) The system which is obtained from LK thus extended is denoted by LK#.

LEMMA 6.5. Let Γ → Δ be LK-provable, and let (Γ1, Γ2) and (Δ1, Δ2) be arbitrary partitions of Γ and Δ, respectively (including the cases that one or more of Γ1 Γ2 Δ1, Δ2, are empty). We denote such a partition by [{Γ1; Δ1, {{Γ2; Δ2}] and call it a partition of the sequent Γ → Δ. Then there exists a formula C of LK # (called an interpolant of [{Γ1; Δ1}, {Γ2; Δ2}] such that:

(i) Γ1→ Δ1, C and C, Γ2→ Δ2 are both LK# - provable;

(ii) All free variables and individual and predicate constants in C (apart from T) occur both in Γ1 ∪ Δ1 and Γ2 ∪ Δ2.

We will first prove the theorem (from this lemma) and then prove the lemma.

THEOREM 6.6