Movatterモバイル変換

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

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

• C.1 Bar induction
• C.2 An outline of Spector’s interpretation
• C.3 Bar induction and Buchholz’ Ω-rule

C.1 Bar induction

The Bar Theorem is a theorem about trees. It occupies a prominentplace in Brouwer’s development of intuitionist mathematics andhas 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 toSpector’s functional interpretation of second order arithmetic.Its proof-theoretic analysis provides a nice demonstration ofBuchholz’ Ω-rule.

Brouwer’s justification for the Bar theorem (1927), that is, ofthe general validity of Bar Induction, rests on the idea that anycanonical proof of (Hyp 1) in infinitary logic has a particularstructure which allows one, when supplied with proofs of (Hyp2–4), to transform it into a proof of \(Q(\langle \rangle)\).With hindsight, one could say that Brouwer is assuming that acanonical proof is something like a cut-free proof in\(\omega\)-logic.

The notions ofDefinition C.1 can be easily formalized in the language of second order arithmetic.If one doesn’t impose any restrictions on the complexity of thebarB and the predicateQ (i.e., allowing them to beexpressed by any formula of the language), then \(\BI_{\igen}\) issurprisingly strong when classical logic is assumed as shown by Howard (1963, section 2.3).

On the other hand, when the ambient logic is intuitionist,\(\BI_{\igen}\) is much weaker than \(\bZ_2\). To obtain anintuitionist theory of that strength based on the idea of BarInduction 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 functionalinterpretation. To find a class of functionals sufficient unto thetask of lifting the D-interpretation to \(\bZ_2\), he defined theso-called bar recursive functionals. The crucial step in theinterpretation is to furnish a functional interpretation of thenegative translation of \(\BI_{\igen}\), which byTheorem C.2 gives rise to an interpretation of \(\bZ_2\). For this he extendedintuitionist \(\BI_{\igen}\) to all finite types. Bar induction fortype \(\sigma\), \(\BI_{\sigma}\), is formulated similar to\(\BI_{\igen}\), the difference being that instead of just looking atthe tree of all finite sequences of natural numbers \(\bbN^*\), onetakes the full tree of finite sequences \(\langleF_1,\ldots,F_r\rangle\) of objects \(F_i\) of type \(\sigma\),\(\cT_{\sigma}\). A bar of the latter is defined in complete analogyto a bar of \(\bbN^*\).

Instead of \(\BI_{\sigma}\), Spector’s extension ofT hasa scheme, \(\bBR_{\sigma}\) for defining functionals bybarrecursion on the tree \(\cT_{\sigma}\). The first step is tointerpret 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 ofA. A functional interpretation of \(A\leftrightarrow A^D\)follows from observing that \((A\leftrightarrow A^D)^D\) is identicalto \((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 thenegative interpretation of some instances of \(\BI_{\sigma}\) in\(\bHA^{\sharp}+\BI_{\sigma}\). The main task is to verify thenegative interpretation of (Hyp 1) of special forms of \(\BI_{\sigma}\),

with the predicate \(P(c)\) being of the form \(\exists Z\,B(Z,c)\)where \(B(Z,c)\) is quantifier free andc is of type \(\sigma\)(see Howard 1968, Lemma 4D). The negative translation of\((\ref{h1})\) is

since \(B(Z,c)\) is quantifier free. TheD-translation of thelatter formula is the same as that of \(\forall f\existsn\neg\neg\exists Z\,B(Z,\bar{f}n)\). Note that a generalization ofMarkov’s principle is a consequence of (\(\ref{D}\)). As aresult, \(\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, andthat until the bar theorem can be given a suitable foundation, thequestion of whether bar induction is intuitionistic is premature.(Spector 1962: 2)

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

C.3 Bar induction and Buchholz’ Ω-rule

ByTheorem C.2, \(\BI_{\igen}\) with classical logic is very strong. If thebackground logic is assumed to be just intuitionist, then is a lotweaker, namely of the same strength as the theory of non-iteratedinductive definitions \(\bID_1\) (which has the Bachmann-Howardordinal as its proof-theoretic ordinal; seesection 5.3.1). So \(\BI_{\igen}\) is an example of a theory where the law ofexcluded middle makes an enormous difference. A classical theory ofthe same strength as intuitionist \(\BI_{\igen}\) is obtained byrequiring the barB to be a set. This theory is usually denotedby \(\BI\). An equivalent formalization of \(\BI\) is given by theschema 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 alloccurrences of the form \(t\in X\) in the formula by \(F(t)\).

Ever since the great successes with the \(\omega\)-rule, whichrestored cut elimination in arithmetic, proof theorists were lookingfor stronger forms of infinitary proof rules that could bring aboutcut elimination for genuinely impredicative theories. Buchholz was thefirst who succeeded in finding such a rule. He introduced theΩ-rule in Buchholz 1977a, and extended versions of it are the central tool inBuchholz and Schütte 1988. A sequent calculus version of it wasused in Rathjen and Weiermann 1993 to give a proof-theoretic boundon Kruskal’s theorem and this is the version we will brieflydiscuss. According to the intuitionist interpretation of animplication (called the Brouwer-Heyting-Kolmogorov (BHK)interpretation) the truth of an implication \(C\to D\) is explained interms of a construction that transforms any proof ofC into aproof ofD. This idea may serve as a first approach to theΩ-rule:

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

Since any cut free proof of \(\forall XA(X)\) can be transformed intoa 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 toonaive an approach since this rule does not behave well with respect tocut elimination, particularly since side formulae (assumptions) arenot taken into account. So the actual Ω-rule takes a rathermore involved form:

With the help of the Ω-rule one obtains an ordinal analysisof (BI.); see Buchholz and Schütte 1988 andRathjen and Weiermann 1993. In view of Brouwer’s speculativejustification of bar induction, it is perhaps gratifying to see that aproof-theoretic analysis of (BI) can be obtained viaa rule that embodies transformations on infinite canonical prooftrees.