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 be the set of
all finite sequences of natural numbers including the empty sequence
. can be viewed as an infinite tree which
grows from the root upwards. If ,
and then the
immediate successor nodes or children of s are of the form
defined as .
t is a node above s if t is of the form
.
A bar of is a subclass B of such that
every infinite path through goes through B; in
Brouwer’s terminology, every infinite path is
“barred” by B. More formally this is defined as
follows. For a function and ,
denotes the sequence . A bar B for
is a subclass of such that for all there
exists such that .
Bar induction is the following principle:
where
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 .
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 is
surprisingly strong when classical logic is assumed as shown by Howard (1963, section 2.3).
Theorem C.2 implies full
second order comprehension (actually ) and is
conservative over for
sentences.[52]
(Conservativity for
sentences is not shown in (Howard, 1963).)
On the other hand, when the ambient logic is intuitionist,
is much weaker than . 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 by means of a functional
interpretation. To find a class of functionals sufficient unto the
task of lifting the D-interpretation to , 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 , which by
Theorem C.2
gives rise to an interpretation of . For this he extended
intuitionist to all finite types. Bar induction for
type , , is formulated similar to
, the difference being that instead of just looking at
the tree of all finite sequences of natural numbers , one
takes the full tree of finite sequences of objects of type ,
. A bar of the latter is defined in complete analogy
to a bar of .
Instead of , Spector’s extension of T has
a scheme, for defining functionals by bar
recursion on the tree . The first step is to
interpret the theory in Spector’s
, where is the theory
augmented by the axioms
with being the Gödel Dialectica interpretation of
A. A functional interpretation of
follows from observing that is identical
to . With this one can see that
has a functional interpretation in
.
The next step, which furnishes the interpretation of classical
(and thereby of full ) is to look at the
negative interpretation of some instances of in
. The main task is to verify the
negative interpretation of
(Hyp 1)
of special forms of ,
with the predicate being of the form
where is quantifier free and c is of type
(see Howard 1968, Lemma 4D). The negative translation of
is
since is quantifier free. The D-translation of the
latter formula is the same as that of . Note that a generalization of
Markov’s principle is a consequence of (). As a
result, is equivalent in
to , so (Hyp 1)
has been restored.
Spector was rather cautious not to claim that his theory
gives a constructive interpretation of .
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,
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 (which has the Bachmann-Howard
ordinal as its proof-theoretic ordinal; see
section 5.3.1).
So 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 is obtained by
requiring the bar B to be a set. This theory is usually denoted
by . An equivalent formalization of is given by the
schema of quantifier elimination (see Feferman 1970b):
for any arithmetical formula and arbitrary -formula
, where arises from by replacing all
occurrences of the form in the formula by .
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 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]
of we have
, then is considered to
be a proof of .
Since any cut free proof of can be transformed into
a proof of , just by the operation of substituting
for in , this rule allows one to prove
. 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 -formulae and
-formulae , every cut free proof of
can be transformed into a proof of
, then is considered to
be a proof of .
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.