8
$\begingroup$

I searched on the internet, but I could not find anything useful about applications of forcing in constructive set theories. Are there any developments of forcing in CZF or IZF?

Thanks in advance.

Improve this question
$\endgroup$
3
  • 2
    $\begingroup$ I think John L Bell introduces at the end of Set theory - Boolean Valued models and independence proofs a sort of forcing theory in IZF, where instead of creating a Boolean valued model, one creates a Heyting-valued model. You may want to take a look at it $\endgroup$
    – Maxime Ramzi
    Commented Mar 3, 2017 at 13:44
  • 2
    $\begingroup$ I think that most of the forcing in constructive settings is done via toposes and whatnot in a more categorical setting. I know that David Roberts has done some work on the topic. Not sure if you'll find it useful or not. $\endgroup$
    – Asaf Karagila ♦
    Commented Mar 3, 2017 at 14:24
  • $\begingroup$ @AsafKaragila: Actually I could not find anything at all by searching subjects like forcing in constructive set theory. Thank you for your comment. $\endgroup$
    – Erfan Khaniki
    Commented Mar 3, 2017 at 14:28

1 Answer 1

Reset to default
8
$\begingroup$

See

Forcing for IZF in sheaf toposes

Also

Toposes from Forcing for Intuitionistic ZF with Atoms.

Edit:

Maybe more references:

Heyting-valued models for intuitionistic set theory

The book "Intuitionistic logic, model theory and forcing" by Fitting.

see also the following web-page where some references are also given:

Constructive Set Theory: Forcing, Large Sets, and Mathematics

Topological forcing semantics with settling.

Improve this answer
$\endgroup$
5
  • $\begingroup$ Thank you very much. Is there any work using Kripke models instead of toposes? $\endgroup$
    – Erfan Khaniki
    Commented Mar 3, 2017 at 17:14
  • 3
    $\begingroup$ In Gambino's thesis he does sheaf interpretation in two steps: first for presheaves and then for a local operator, so the first step is like Kripke models. It is not very topos-theoretic. The work is also interesting as it works for CZF. cs.le.ac.uk/people/ngambino/Publications/thesis.pdf $\endgroup$
    – Ulrik Buchholtz
    Commented Mar 3, 2017 at 18:12
  • $\begingroup$ @UlrikBuchholtz: Thank you very much for the link. $\endgroup$
    – Erfan Khaniki
    Commented Mar 3, 2017 at 18:35
  • 2
    $\begingroup$ @ErfanKhaniki It may be a too late answer, but works by Robert Lubarsky heavily use a (variant of) Kripke model. $\endgroup$
    – Hanul Jeon
    Commented Nov 23, 2019 at 2:21
  • $\begingroup$ @HanulJeon, thanks a lot for the comment. $\endgroup$
    – Erfan Khaniki
    Commented Nov 23, 2019 at 13:02

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .