Supplement to Proof Theory

C. Bar Induction, Spector’s Result, and the Ω-rule

Here we discuss the principle of bar induction, Spector’s proof and a relationship between bar induction and an infinitary proof rule devised by Buchholz.


C.1 Bar induction

The Bar Theorem is a theorem about trees. It occupies a prominent place in Brouwer’s development of intuitionist mathematics and has also played a central role in proof theory in the 1960s and 1970s. Here we will give a brief account of it since it is essential to Spector’s functional interpretation of second order arithmetic. Its proof-theoretic analysis provides a nice demonstration of Buchholz’ Ω-rule.

Definition C.1 Let N be the set of all finite sequences of natural numbers including the empty sequence . N can be viewed as an infinite tree which grows from the root upwards. If sN, mN and s=s0,sk then the immediate successor nodes or children of s are of the form sm defined as s0,,sk,m. t is a node above s if t is of the form sk0kr.

A bar of N is a subclass B of N such that every infinite path through N goes through B; in Brouwer’s terminology, every infinite path is “barred” by B. More formally this is defined as follows. For a function f:NN and nN, f¯n denotes the sequence f(0),,f(n1)(f¯0=). A bar B for N is a subclass of N such that for all f:NN there exists nN such that f¯nB.

Bar induction is the following principle:

BIgenHyp 1Hyp 2Hyp 3Hyp 4Q()

where

(Hyp 1)B is a bar(Hyp 2)sNnN(sBsnB)(Hyp 3)sN(sBsQ)(Hyp 4)sN[(kNskQ)sQ].

Clause (Hyp 4) asserts that the property of being in Q propagates to a node s if all its children belong to Q. Since all nodes in the bar belong to Q by (Hyp 3), the intuitive idea behind this principle is that the clauses (Hyp 1–4) guarantee that membership in Q “percolates” from the bar all the way down to the root.[51]

Brouwer’s justification for the Bar theorem (1927), that is, of the general validity of Bar Induction, rests on the idea that any canonical proof of (Hyp 1) in infinitary logic has a particular structure which allows one, when supplied with proofs of (Hyp 2–4), to transform it into a proof of Q(). With hindsight, one could say that Brouwer is assuming that a canonical proof is something like a cut-free proof in ω-logic.

The notions of Definition C.1 can be easily formalized in the language of second order arithmetic. If one doesn’t impose any restrictions on the complexity of the bar B and the predicate Q (i.e., allowing them to be expressed by any formula of the language), then BIgen is surprisingly strong when classical logic is assumed as shown by Howard (1963, section 2.3).

Theorem C.2 BIgen implies full second order comprehension CA (actually AC) and is conservative over Z2 for Π41 sentences.[52] (Conservativity for Π41 sentences is not shown in (Howard, 1963).)

On the other hand, when the ambient logic is intuitionist, BIgen is much weaker than Z2. To obtain an intuitionist theory of that strength based on the idea of Bar Induction one needs to consider Bar Induction on higher types.

C.2 An outline of Spector’s interpretation

In his 1960, Spector gave a consistency proof of Z2 by means of a functional interpretation. To find a class of functionals sufficient unto the task of lifting the D-interpretation to Z2, he defined the so-called bar recursive functionals. The crucial step in the interpretation is to furnish a functional interpretation of the negative translation of BIgen, which by Theorem C.2 gives rise to an interpretation of Z2. For this he extended intuitionist BIgen to all finite types. Bar induction for type σ, BIσ, is formulated similar to BIgen, the difference being that instead of just looking at the tree of all finite sequences of natural numbers N, one takes the full tree of finite sequences F1,,Fr of objects Fi of type σ, Tσ. A bar of the latter is defined in complete analogy to a bar of N.

Instead of BIσ, Spector’s extension of T has a scheme, BRσ for defining functionals by bar recursion on the tree Tσ. The first step is to interpret the theory HA+BIσ in Spector’s T+BRσ, where HA is the theory HAω augmented by the axioms

(c1)AAD

with AD being the Gödel Dialectica interpretation of A. A functional interpretation of AAD follows from observing that (AAD)D is identical to (AA)D. With this one can see that HA+BIσ has a functional interpretation in T+BRσ.

The next step, which furnishes the interpretation of classical BIgen (and thereby of full CA) is to look at the negative interpretation of some instances of BIσ in HA+BIσ. The main task is to verify the negative interpretation of (Hyp 1) of special forms of BIσ,

(c2)fnP(f¯n)

with the predicate P(c) being of the form ZB(Z,c) where B(Z,c) is quantifier free and c is of type σ (see Howard 1968, Lemma 4D). The negative translation of (c2) is

f¬¬nP(f¯n)N; i.e., f¬¬n¬¬ZB(Z,f¯n)

since B(Z,c) is quantifier free. The D-translation of the latter formula is the same as that of fn¬¬ZB(Z,f¯n). Note that a generalization of Markov’s principle is a consequence of (c1). As a result, f¬¬nP(f¯n)N is equivalent in HA to fnP(f¯n)N, so (Hyp 1) has been restored.
Spector was rather cautious not to claim that his theory T+BR gives a constructive interpretation of Z2.

The author believes that the bar theorem is itself questionable, and that until the bar theorem can be given a suitable foundation, the question of whether bar induction is intuitionistic is premature. (Spector 1962: 2)

The question of constructivity of bar recursion was also answered in the negative by Kreisel; cf. section 5.3. On closer inspection of the proof, one is left with the impression that logically complex comprehensions are traded in for inductions on highly complex higher type relations.[53] That notwithstanding, Spector’s result is quite remarkable and his interpretation has been applied to extract computational information from classical proofs (Kohlenbach 2007).

C.3 Bar induction and Buchholz’ Ω-rule

By Theorem C.2, BIgen with classical logic is very strong. If the background logic is assumed to be just intuitionist, then is a lot weaker, namely of the same strength as the theory of non-iterated inductive definitions ID1 (which has the Bachmann-Howard ordinal as its proof-theoretic ordinal; see section 5.3.1). So BIgen is an example of a theory where the law of excluded middle makes an enormous difference. A classical theory of the same strength as intuitionist BIgen is obtained by requiring the bar B to be a set. This theory is usually denoted by BI. An equivalent formalization of BI is given by the schema of quantifier elimination (see Feferman 1970b):

(2-E)XA(X)A(F)

for any arithmetical formula A(X) and arbitrary L2-formula F(u), where A(F) arises from A(X) by replacing all occurrences of the form tX in the formula by F(t).

Ever since the great successes with the ω-rule, which restored cut elimination in arithmetic, proof theorists were looking for stronger forms of infinitary proof rules that could bring about cut elimination for genuinely impredicative theories. Buchholz was the first who succeeded in finding such a rule. He introduced the Ω-rule in Buchholz 1977a, and extended versions of it are the central tool in Buchholz and Schütte 1988. A sequent calculus version of it was used in Rathjen and Weiermann 1993 to give a proof-theoretic bound on Kruskal’s theorem and this is the version we will briefly discuss. According to the intuitionist interpretation of an implication (called the Brouwer-Heyting-Kolmogorov (BHK) interpretation) the truth of an implication CD is explained in terms of a construction that transforms any proof of C into a proof of D. This idea may serve as a first approach to the Ω-rule:

  • (Ω~)If for every cut free proof[54] D of XA(X) we have T(D)ΘΞ, then T is considered to be a proof of Θ,XF(X)Ξ.

Since any cut free proof of XA(X) can be transformed into a proof of A(F), just by the operation T of substituting F(t) for tX in A(X), this rule allows one to prove (2-E). However, (Ω~) is just too naive an approach since this rule does not behave well with respect to cut elimination, particularly since side formulae (assumptions) are not taken into account. So the actual Ω-rule takes a rather more involved form:

Definition C.3

  • (Ω)If for all finite sets of Σ11-formulae Γ and Π11-formulae Δ, every cut free proof D of ΓΔ,XA(X) can be transformed into a proof T(D) of Γ,ΘΔ,Ξ, then T is considered to be a proof of Θ,XF(X)Ξ.

With the help of the Ω-rule one obtains an ordinal analysis of (BI.); see Buchholz and Schütte 1988 and Rathjen and Weiermann 1993. In view of Brouwer’s speculative justification of bar induction, it is perhaps gratifying to see that a proof-theoretic analysis of (BI) can be obtained via a rule that embodies transformations on infinite canonical proof trees.

Copyright © 2024 by
Michael Rathjen <rathjen@maths.leeds.ac.uk>
Wilfried Sieg <sieg@cmu.edu>

This is a file in the archives of the Stanford Encyclopedia of Philosophy.
Please note that some links may no longer be functional.