A most artistic package of a jumble of ideas

Dialectica 62 (2):205–222 (2008)
  Copy   BIBTEX

Abstract

In the course of ten short sections, we comment on Gödel's seminal dialectica paper of fifty years ago and its aftermath. We start by suggesting that Gödel's use of functionals of finite type is yet another instance of the realistic attitude of Gödel towards mathematics, in tune with his defense of the postulation of ever increasing higher types in foundational studies. We also make some observations concerning Gödel's recasting of intuitionistic arithmetic via the dialectica interpretation, discuss the extra principles that the interpretation validates and comment on extensionality and higher order equality. The latter sections focus on the role of majorizability considerations within the dialectica and related interpretations for extracting computational information from ordinary proofs in mathematics.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 93,127

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Cartesian closed Dialectica categories.Bodil Biering - 2008 - Annals of Pure and Applied Logic 156 (2):290-307.
Predicative functionals and an interpretation of ⌢ID.Jeremy Avigad - 1998 - Annals of Pure and Applied Logic 92 (1):1-34.
Functional interpretation and inductive definitions.Jeremy Avigad & Henry Towsner - 2009 - Journal of Symbolic Logic 74 (4):1100-1120.
Godel's interpretation of intuitionism.William Tait - 2006 - Philosophia Mathematica 14 (2):208-228.
Shoenfield is Gödel after Krivine.Thomas Streicher & Ulrich Kohlenbach - 2007 - Mathematical Logic Quarterly 53 (2):176-179.

Analytics

Added to PP
2009-01-28

Downloads
54 (#304,015)

6 months
5 (#710,311)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

Injecting uniformities into Peano arithmetic.Fernando Ferreira - 2009 - Annals of Pure and Applied Logic 157 (2-3):122-129.
The bounded functional interpretation of bar induction.Patrícia Engrácia - 2012 - Annals of Pure and Applied Logic 163 (9):1183-1195.

Add more citations

References found in this work

Mathematical logic.Joseph R. Shoenfield - 1967 - Reading, Mass.,: Addison-Wesley.
Interpretation of analysis by means of constructive functionals of finite types.Georg Kreisel - 1959 - In A. Heyting (ed.), Constructivity in mathematics. Amsterdam,: North-Holland Pub. Co.. pp. 101--128.
Intensional interpretations of functionals of finite type I.W. W. Tait - 1967 - Journal of Symbolic Logic 32 (2):198-212.
On Brouwer.Mark van Atten - 2004 - Wadsworth Publishing Company.

View all 16 references / Add more references