Large sets in intuitionistic set theory (Q796524): Difference between revisions

We consider large cardinal properties in the context of intuitionistic set theory (ZFI). Inaccessibility, Mahloness, measurability, supercompactness, hugeness, and the Reinhardt axiom can be stated so that the corresponding extensions of ZFI have the following properties: 1) Gödel's negative interpretation works, hence the extension of ZF with the existence of the analogous large cardinal is an equiconsistent subsystem; 2) versions of Kleene's recursive realizability work, hence it is consistent to consider all numerical functions recursive, and every provable existential sentence asserting the existence of a natural number with a possibly set-theoretic property has a definable, numerical witness; 3) Goodman's forcing works, so dependent choice in finite types is conservative over arithmetic sentences; 4) the system is closed under Markov's rule, and hence it has the same provably recursive functions as the analogous classical system. Due to an editing error, the abstract of the paper claims that the consistency of some of these systems is shown to be equivalent to natural assertions of constructive analysis, but the result is never exhibited in the paper. It follows from the work of the first author on the necessary uses of abstract set theory in the classical setting [Am. Math. Soc., Notices 31, 563-566 (1984)] and the above mentioned property 4).