Note on the fan theorem

Publisher Website
Google Scholar
Abstract
The principal aim of this paper is to establish a theorem stating, roughly, that the addition of the fan theorem and the. continuity schema to an intuitionistic system of elementary analysis results in a conservative extension with respect to arithmetical statements.The result implies that the consistency of first order arithmetic cannot be proved by use of the fan theorem, in addition to standard elementary methods—although it was the opposite assumption which led Gentzen to withdraw the first version of his consistency proof for arithmetic (see [B]).We must presuppose acquaintance with notation and principal results of [K, T], and with §1.6, Chapter II, and Chapter III, §4-6 of [T1]. In one respect we shall deviate from the notation in [K, T]: We shall use (n)x (instead of g(n, x)) to indicate the xth component of the sequence coded by n, if x < lth(n), 0 otherwise.We also introduce abbreviations n ≤* m, a ≤ b which will be used frequently below:

This publication has 5 references indexed in Scilit: