3
$\begingroup$

Work in ZF, if there are proper class many supercompact cardinals, then all grounds are uniformly definable. Hence under reasonable assumption, we can have choiceless set-theoretic geology.

But can we go further?

  1. Are all Without-$\sf LEM$ grounds of $V$ uniformly definable? (Suppose there are proper class many supercompact cardinals)
  2. What is the connection between Intuitionistic Set-theoretic Geology & Heyting-valued Models/presheaves?
  3. Can We have computational interpretation of Intuitionistic Set-theoretic Geology?
Improve this question
$\endgroup$
4
  • 6
    $\begingroup$ This is a nice question but given the state of knowledge about inner models in constructive set theory (i.e., there is at least no published resolution of whether $\neg \mathsf{LEM}$ implies $V=L$ over $\mathsf{IZF}$) and the state of research regarding large cardinals (i.e., Mahlos have been looked at and I believe some people are looking at measurables), I feel pretty confident in saying that we're nowhere near having the kind of clear picture that would be needed to address this question. $\endgroup$
    – James E Hanson
    Commented Aug 24 at 17:10
  • 2
    $\begingroup$ @JamesEHanson Richard Matthews proved in his thesis (Theorem 5.5.1) that $\mathsf{IZF}$ is consistent with $\mathrm{Ord}\neq \mathrm{Ord}\cap L$, so $\mathsf{IZF}+\lnot\mathsf{LEM}+V\neq L$ is consistent. $\endgroup$
    – Hanul Jeon
    Commented Aug 26 at 0:53
  • $\begingroup$ @HanulJeon Ah that's news to me. Thank you for letting me know. $\endgroup$
    – James E Hanson
    Commented Aug 26 at 0:56
  • $\begingroup$ I am unsure if the notion of ground makes sense in a constructive setting. A set-theoretic universe without LEM is quite wild: For example, ordinals need not be linearly ordered, and the powerset of 2 can be uncountable (in the sense that there is no onto function from $\omega$.) I also have not seen any materials considering a generic extension of a universe without LEM, even on materials considering intuitionistic forcing. $\endgroup$
    – Hanul Jeon
    Commented Aug 26 at 0:56

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .