A short note on spector's proof of consistency of analysis

Abstract

In 1962, Clifford Spector gave a consistency proof of analysis using so-called bar recursors. His paper extends an interpretation of arithmetic given by Kurt Gödel in 1958. Spector's proof relies crucially on the interpretation of the so-called numerical double negation shift principle. The argument for the interpretation is ad hoc. On the other hand, William Howard gave in 1968 a very natural interpretation of bar induction by bar recursion. We show directly that, within the framework of Gödel's interpretation, numerical double negation shift is a consequence of bar induction. © 2012 Springer-Verlag.