Set existence property for intuitionistic theories with dependent choice
type: Item
instance of: scholarly article
title: Set existence property for intuitionistic theories with dependent choice
zbMATH Open document ID: 0539.03039
DOI: 10.1016/0168-0072(83)90011-8
author: Harvey M. Friedman
author: Andre Scedrov
published in: Annals of Pure and Applied Logic
publication date: 1983-01-01T00:00:00Z
review text: It is known that many intuitionistic theories have the existence property (EP): if a sentence \(\exists x.A(x)\) is provable, then so is A(t) for some closed term t. In the presence of countable choice (CAC) or relativized dependent choice (RDC), however, only fragment of EP regarding the existence of natural numbers (numerical EP) was established [\textit{J. Myhill}, J. Symb. Logic 40, 347-382 (1975; Zbl 0314.02045)]. The authors first show EP for second order intuitionistic arithmetic with CAC. The proof involves Friedman's extension of the Kleene slash, not in the classical metatheory, but in the 1945-realizability model. Numerical EP is then used. The method readily extends to intuitionistic type theory (resp. intuitionistic Zermelo set theory) with RDC. A modification of the argument establishes the following for intuitionistic ZF set theory formulated with replacement, and with RDC \((ZFI_ R\)+RDC). Let TI be the schema of transfinite induction over all (true) primitive recursive well founded binary relations on natural numbers. Let T\(I^-\) be the fragment of TI referring to such relations provably well founded in intuitionistic ZF with collection and RDC. Let a sentence \(\exists x.A(x)\) be provable in ZF\(I_ R\)+RDC (in ZF\(I_ R\)+RDC+TI, resp.). Then there is a formula \(B(y)\) with exactly y free, such that \(\exists x(A(x)\wedge \forall y(y\in x\leftrightarrow B(y)))\) is provable in ZF\(I_ R\)+RDC+T\(I^-\) (in ZF\(I_ R\)+RDC+TI, resp.).
Mathematics Subject Classification ID: 03F50
zbMATH DE Number: 3857099
zbMATH Keywords: Friedman slash
zbMATH Keywords: recursive realizability
zbMATH Keywords: intuitionistic theories
zbMATH Keywords: existence property
zbMATH Keywords: countable choice
zbMATH Keywords: relativized dependent choice
zbMATH Keywords: second order intuitionistic arithmetic
zbMATH Keywords: intuitionistic type theory
zbMATH Keywords: intuitionistic Zermelo set theory
zbMATH Keywords: intuitionistic ZF
MaRDI profile type: Publication
full work available at URL: 0168-0072(83)90011-8
OpenAlex ID: W2074713441
cites work: Q3214890
cites work: Reflection Principles and their Use for Establishing the Complexity of Axiomatic Systems
cites work: Q3214891
cites work: Constructive set theory
cites work: Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
description: scientific article; zbMATH DE number 3857099