David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
Dialectica 62 (2):149–177 (2008)
Gödel's dialectica interpretation of Heyting arithmetic HA may be seen as expressing a lack of confidence in our understanding of unbounded quantification. Instead of formally proving an implication with an existential consequent or with a universal antecedent, the dialectica interpretation asks, under suitable conditions, for explicit 'interpreting' instances that make the implication valid. For proofs in constructive set theory CZF-, it may not always be possible to find just one such instance, but it must suffice to explicitly name a set consisting of such interpreting instances. The aim of eliminating unbounded quantification in favor of appropriate constructive functionals will still be obtained, as our ∧-interpretation theorem for constructive set theory in all finite types CZFω- shows. By changing to a hybrid interpretation ∧q, we show closure of CZFω- under rules that – in stronger forms – have already been studied in the context of Heyting arithmetic. In a similar spirit, we briefly survey modified realizability of CZFω- and its hybrids. Central results of this paper have been proved by Burr 2000a and Schulte 2006, however, for different translations. We use a simplified interpretation that goes back to Diller and Nahm 1974. A novel element is a lemma on absorption of bounds which is essential for the smooth operation of our translation.
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library|
References found in this work BETA
Joseph R. Shoenfield (1967). Mathematical Logic. Reading, Mass.,Addison-Wesley Pub. Co..
A. S. Troelstra (1988). Constructivism in Mathematics: An Introduction. Sole Distributors for the U.S.A. And Canada, Elsevier Science Pub. Co..
John Myhill (1975). Constructive Set Theory. Journal of Symbolic Logic 40 (3):347-382.
Von Kurt Gödel (1958). Über eine bisher noch nicht benützte erweiterung Des finiten standpunktes. Dialectica 12 (3‐4):280-287.
S. C. Kleene (1945). On the Interpretation of Intuitionistic Number Theory. Journal of Symbolic Logic 10 (4):109-124.
Citations of this work BETA
Michael Rathjen (2012). From the Weak to the Strong Existence Property. Annals of Pure and Applied Logic 163 (10):1400-1418.
Similar books and articles
John Bell (2008). The Axiom of Choice and the Law of Excluded Middle in Weak Set Theories. Mathematical Logic Quarterly 54 (2):194-201.
Bart Jacobs (1989). The Inconsistency of Higher Order Extensions of Martin-Löf's Type Theory. Journal of Philosophical Logic 18 (4):399 - 422.
Jeremy Avigad (2002). A Realizability Interpretation for Classical Arithmetic. Bulletin of Symbolic Logic 8 (3):439-440.
John L. Bell (1999). Frege's Theorem in a Constructive Setting. Journal of Symbolic Logic 64 (2):486-488.
Michael Rathjen (2005). The Disjunction and Related Properties for Constructive Zermelo-Fraenkel Set Theory. Journal of Symbolic Logic 70 (4):1233 - 1254.
J. Avigad & S. Feferman (1998). Godel's Functional Interpretation. In Samuel R. Buss (ed.), Handbook of Proof Theory. Elsevier
Robert S. Lubarsky & Michael Rathjen (2008). On the Constructive Dedekind Reals. Logic and Analysis 1 (2):131-152.
Nicola Gambino & Peter Aczel (2006). The Generalised Type-Theoretic Interpretation of Constructive Set Theory. Journal of Symbolic Logic 71 (1):67 - 103.
Richard Pettigrew (2009). On Interpretations of Bounded Arithmetic and Bounded Set Theory. Notre Dame Journal of Formal Logic 50 (2):141-152.
Added to index2009-01-28
Total downloads6 ( #322,537 of 1,725,624 )
Recent downloads (6 months)2 ( #268,736 of 1,725,624 )
How can I increase my downloads?