#### 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 \(\bbN^*\) be the set of
all finite sequences of natural numbers including the empty sequence
\(\langle\rangle\). \(\bbN^*\) can be viewed as an infinite tree which
grows from the root \(\langle\rangle\) upwards. If \(s\in\bbN^*\),
\(m\in\bbN\) and \(s=\langle s_0,\ldots s_k\rangle\) then the
immediate successor nodes or children of *s* are of the form
\(s*\langle m\rangle\) defined as \(\langle s_0,\ldots,s_k,m\rangle\).
*t* is a node *above* *s* if *t* is of the form
\(s*\langle k_0\rangle*\ldots*\langle k_r\rangle\).

A bar of \(\bbN^*\) is a subclass *B* of \(\bbN^*\) such that
every infinite path through \(\bbN^*\) 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:\bbN\to \bbN\) and \(n\in\bbN\),
\(\bar{f}n\) denotes the sequence \(\langle f(0),\ldots, f(n-1)\rangle
(\bar{f}0= \langle\rangle)\). A *bar* *B* for \(\bbN^*\)
is a subclass of \(\bbN^*\) such that for all \(f:\bbN\to\bbN\) there
exists \(n\in\bbN\) such that \(\bar fn\in B\).

Bar induction is the following principle:

\[ \tag*{\(\BI_{\igen}\)} \textrm{Hyp 1}\land \textrm{Hyp 2}\land \textrm{Hyp 3}\land\textrm{Hyp 4} \to Q(\langle \rangle) \]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 \(Q(\langle \rangle)\). With hindsight, one could say that Brouwer is assuming that a canonical proof is something like a cut-free proof in \(\omega\)-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 \(\BI_{\igen}\) is
surprisingly strong when classical logic is assumed as shown by Howard (1963, section 2.3).

Theorem C.2 \(\BI_{\igen}\) implies full
second order comprehension \({\bCA}\) (actually \(\bAC\)) and is
conservative over \(\bZ_2\) for \(\Pi^1_4\)
sentences.^{[52]}
(Conservativity for \(\Pi^1_4\)
sentences is not shown in (Howard, 1963).)

On the other hand, when the ambient logic is intuitionist, \(\BI_{\igen}\) is much weaker than \(\bZ_2\). 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 \(\bZ_2\) by means of a functional interpretation. To find a class of functionals sufficient unto the task of lifting the D-interpretation to \(\bZ_2\), 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 \(\BI_{\igen}\), which by Theorem C.2 gives rise to an interpretation of \(\bZ_2\). For this he extended intuitionist \(\BI_{\igen}\) to all finite types. Bar induction for type \(\sigma\), \(\BI_{\sigma}\), is formulated similar to \(\BI_{\igen}\), the difference being that instead of just looking at the tree of all finite sequences of natural numbers \(\bbN^*\), one takes the full tree of finite sequences \(\langle F_1,\ldots,F_r\rangle\) of objects \(F_i\) of type \(\sigma\), \(\cT_{\sigma}\). A bar of the latter is defined in complete analogy to a bar of \(\bbN^*\).

Instead of \(\BI_{\sigma}\), Spector’s extension of **T** has
a scheme, \(\bBR_{\sigma}\) for defining functionals by *bar
recursion* on the tree \(\cT_{\sigma}\). The first step is to
interpret the theory \(\bHA^{\sharp}+\BI_{\sigma}\) in Spector’s
\(\bT+\bBR_{\sigma}\), where \(\bHA^{\sharp}\) is the theory
\(\bHA^{\omega}\) augmented by the axioms

with \(A^D\) being the Gödel Dialectica interpretation of
*A*. A functional interpretation of \(A\leftrightarrow A^D\)
follows from observing that \((A\leftrightarrow A^D)^D\) is identical
to \((A\leftrightarrow A)^D\). With this one can see that
\(\bHA^{\sharp}+\BI_{\sigma}\) has a functional interpretation in
\(\bT+ \bBR_{\sigma}\).

The next step, which furnishes the interpretation of classical \(\BI_{\igen}\) (and thereby of full \({\bCA}\)) is to look at the negative interpretation of some instances of \(\BI_{\sigma}\) in \(\bHA^{\sharp}+\BI_{\sigma}\). The main task is to verify the negative interpretation of (Hyp 1) of special forms of \(\BI_{\sigma}\),

\[\tag{c2}\label{h1} \forall f\exists n\,P(\bar{f}n) \]
with the predicate \(P(c)\) being of the form \(\exists Z\,B(Z,c)\)
where \(B(Z,c)\) is quantifier free and *c* is of type \(\sigma\)
(see Howard 1968, Lemma 4D). The negative translation of
\((\ref{h1})\) is

since \(B(Z,c)\) is quantifier free. The *D*-translation of the
latter formula is the same as that of \(\forall f\exists
n\neg\neg\exists Z\,B(Z,\bar{f}n)\). Note that a generalization of
Markov’s principle is a consequence of (\(\ref{D}\)). As a
result, \(\forall f\neg\neg\exists n\,P(\bar{f}n)^N\) is equivalent in
\(\bHA^{\sharp}\) to \(\forall f\exists n\,P(\bar{f}n)^N\), so (Hyp 1)
has been restored.

Spector was rather cautious not to claim that his theory \(T+\bBR\)
gives a constructive interpretation of \(\bZ_2\).

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,
\(\BI_{\igen}\) 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 \(\bID_1\) (which has the Bachmann-Howard
ordinal as its proof-theoretic ordinal; see
section 5.3.1).
So \(\BI_{\igen}\) 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 \(\BI_{\igen}\) 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):

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

Ever since the great successes with the \(\omega\)-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 \(C\to D\) 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:

- \((\tilde{\Omega})\)If
for every cut free
proof
^{[54]}\(\cD\) of \(\forall X A(X)\) we have \(\cT(\cD)\vdash\Theta\Rightarrow \Xi\), then \(\cT\) is considered to be a proof of \(\Theta,\forall XF(X)\Rightarrow \Xi\).

Since any cut free proof of \(\forall XA(X)\) can be transformed into a proof of \(A(F)\), just by the operation \(\cT\) of substituting \(F(t)\) for \(t\in X\) in \(A(X)\), this rule allows one to prove \((\forall^2\mbox{-E})\). However, \((\tilde{\Omega})\) 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

- \((\Omega)\)If for all finite sets of \(\Sigma^1_1\)-formulae \(\Gamma\) and \(\Pi^1_1\)-formulae \(\Delta\), every cut free proof \(\cD\) of \[\Gamma\Rightarrow \Delta, \forall X A(X)\] can be transformed into a proof \(\cT(\cD)\) of \(\Gamma,\Theta\Rightarrow \Delta,\Xi\), then \(\cT\) is considered to be a proof of \(\Theta,\forall XF(X)\Rightarrow \Xi\).

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.