Hostname: page-component-78c5997874-4rdpn Total loading time: 0 Render date: 2024-11-02T22:58:57.775Z Has data issue: false hasContentIssue false
  • English
  • Français

Note on the fan theorem

Published online by Cambridge University Press:  12 March 2014

A. S. Troelstra
A. S. Troelstra*
Affiliation:
Mathematical Institute, Oxford, England
Get access Rights & Permissions [Opens in a new window]

Extract

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:

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 39 , Issue 3 , September 1974 , pp. 584 - 596
Copyright
Copyright © Association for Symbolic Logic 1974

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

BIBLIOGRAPHY

[B]Bernays, P., On the original Gentzen consistency proof for number theory, Intuitionism and proof theory (Kino, A., Myhill, J., Vesley, R. E., Editors), North-Holland, Amsterdam, 1970, pp. 409–417.Google Scholar
[F]Friedman, H., König's lemma is weak, Mimeographed notes, Stanford University (unpublished).Google Scholar
[G]Goodman, N., Intuitionistic arithmetic as a theory of constructions, Thesis, Stanford University, 1968.Google Scholar
[K]Kleene, S. C., Recursive functionals and quantifiers of finite types. I, Transactions of the American Mathematical Society, vol. 91 (1959), pp. 1–52.Google Scholar
[Kr1]Kreisel, G., Preface to Volume II of Reports of the Seminar on Foundations of Analysis, Stanford University, 1963.Google Scholar
[Kr2]Kreisel, G., On weak completeness of intuitionistic predicate logic, this Journal, vol., 27 (1962), pp. 139–158.Google Scholar
[Kr3]Kreisel, G., Review of [K, V], this Journal, vol. 31 (1966), pp. 258–261.Google Scholar
[Kr4]Kreisel, G., Lawless sequences of natural numbers, Compositio Mathematica, vol. 20 (1968), pp. 222–248.Google Scholar
[Kr5]Kreisel, G., Constructive mathematics, Mimeographed notes of a course given at Stanford University, 1958–1959.Google Scholar
[K,T]Kreisel, G. and Troelstra, A. S., Formal systems for some branches of intuitionistic analysis, Annals of Mathematical Logic, vol. 1 (1970), pp. 229–387.CrossRefGoogle Scholar
[K,V]Kleene, S. C. and Vesley, R. E., Foundations of intuitionistic mathematics, especially in relation to recursive functions, North-Holland, Amsterdam, 1965.Google Scholar
[S]Scott, D. S., Algebras of sets binumerable in complete extensions of arithmetic, Recursive function theory, Proceedings of Symposia in Pure Mathematics, vol. 5 (Dekker, J. C. E., Editor), American Mathematical Society, Providence, R.I., 1962, pp. 117–121.Google Scholar
[T1 ]Troelstra, A. S. (Editor), Metamathematical investigation of intuitionistic arithmetic and analysis, Lecture Notes in Mathematics, vol. 344, Springer-Verlag, Berlin, 1973.CrossRefGoogle Scholar
[T2]Troelstra, A. S. (Editor), Notions of realizability for intuitionistic arithmetic and intuitionistic arithmetic in all finite types, Proceedings of the Second Scandinavian Logic Symposium (Fenstad, J. E., Editor), North-Holland, Amsterdam, 1971, pp. 369–405.Google Scholar
[T3]Troelstra, A. S. (Editor), An addendum, Annals of Mathematical Logic, vol. 3 (1971), pp. 437–439.CrossRefGoogle Scholar