ncatlab, in its entry for $SEAR$ (<https://www.ncatlab.org/nlab/show/SEAR>), states that



> 
> $SEARC$ ($SEAR$ augmented by an axiom of choice)...is strongly equivalent to $ZFC$.
> 
> 
> 


Since for $SEAR$ (and $SEARC$, according to the ncatlab entry),



> 
> The elements of a set have no "internal structure"; they are merely featureless points,
> 
> 
> 


I would be interested in finding out how one would define notions of forcing in $SEARC$ and how one would (for example) add a Cohen real, or a
Random real.


Also, any references to forcing in SEARC would be greatly appreciated.


Thanks in advance. 



Forcing in $SEARC$
Sheaves work in any structural set theory, because they work using any base topos. Note that SEAR-sets form a well-pointed boolean topos $\mathbf{Set}\_{SEAR}$ ([this](https://www.ncatlab.org/nlab/show/SEAR#heyting) Theorem and [this](https://www.ncatlab.org/nlab/show/SEAR#topos) Theorem on the nLab page on SEAR), and SEARC-sets form a well-pointed boolean topos $\mathbf{Set}\_{SEARC}$ satisfying the axiom of choice in the form "all surjections have a section". By [Axiom 4](https://www.ncatlab.org/nlab/show/SEAR#infinity) both these variants have natural number objects, denoted $\mathbb{N}$.


The poset $P$ used to add an $A$-indexed collection of Cohen reals is just the set of partial functions $\mathbb{N}\times A \rightharpoonup 1 \amalg 1 =: 2$ (which is in fact definable in any topos with NNO) together with the usual partial ordering. Note that once one has a well-pointed topos with NNO then any "structural" construction one might undertake in ZFC that doesn't rely on Replacement can be done. By this I mean anything not referring to elements of elements of sets and so on, or in other words, things invariant under bijections. 


One can define the topos of sheaves on $P$ considered as a site with the double negation topology (which is a special case of the [dense topology](https://ncatlab.org/nlab/show/dense+topology) on a small category) in a way that only uses the topos-theoretic machinery that $\mathbf{Set}\_{SEAR(C)}$ being a topos affords.


In fact the construction in [this section](https://ncatlab.org/nlab/show/continuum+hypothesis#unprovability), illustrating the method of forcing as applied to showing CH is not provable from the axioms for a well-pointed boolean topos, works verbatim in SEAR with some minor syntactic sugar for the topos structure (one could unwind it back to the language of SEAR if desired).


Alternatively, the notion of Lawvere-Tierney topology makes no references to coverages and sieves, and one can define the [double negation topology](https://ncatlab.org/nlab/show/double+negation#in_topos_theory) (which you need for forcing in classical logic) using an LT topology. This means one can consider the category of presheaves on $P$, which is nice to consider as [a construction using internal diagrams](https://ncatlab.org/nlab/show/internal+diagram), and then carve out the subtopos of double negation sheaves.


A good reference is either Tierney's classic paper [Sheaf theory and the continuum hypothesis](https://scholar.google.com/citations?view_op=view_citation&hl=en&user=WwmuvwoAAAAJ&citation_for_view=WwmuvwoAAAAJ:u-x6o8ySG0sC), or if you can get access to it, Mac Lane and Moerdijk's book [Sheaves in Geometry and Logic](https://ncatlab.org/nlab/show/Sheaves+in+Geometry+and+Logic), the chapter on forcing there is pretty good.


Regarding forcing a random real, one can define the poset of Borel subsets of positive measure in $\mathbb{R}$, because one can define all the relevant machinery in a well-pointed boolean topos with NNO and Choice, and then consider the topos of sheaves with the double-negation topology as before. The point about forcing in ZFC is that it is secretly taking sheaves on a poset and then translating back to ZFC in the internal logic of the sheaf topos using the standard Mitchell-Cole-Osius construction.




---


Regarding Lawvere's comments (in [Foundations and Applications: Axiomatization and Education](http://www.jstor.org/stable/3094791)\_) on $L$-sets (for the constructible universe $L$), I'm not sure I agree with that. I think the sets in $L$ are in fact highly structured (even more so than those in the cumulative hierarchy of material set theory generally!). The quote I think you mean is this



> 
> Now Gödel's "constructible" sets L in themselves have a tremendous amount of structure, but the relevant category derived from them is, remarkably, in general much more constant (structureless!) than that devised from an original ambient model V. [page 223]
> 
> 
> 


Note that this follows after Lawvere's reformulation of Cantor's continuum hypothesis as



> 
> for a topos $\mathcal{E}$ of sufficiently structureless sets, CH is true in $\mathcal{E}$ [page 220]
> 
> 
> 


But I don't see that just because CH holds in $L$, we must have that $L$-sets are sufficiently structureless. One could consider that the universe of sets is of the form $L[G]$ (or rather, the topos of sheaves over $L$-sets), but this is a rather specific set-theoretic axiom and I don't know if there are results that say $V$ is a class forcing of its $L$ (this would be very cool if it were the case!) All I can say is: I really don't know what he was on about there.


From where I stand, structural set theory so far lacks an analogue of [inner model theory](https://en.wikipedia.org/wiki/Inner_model_theory) of which $L$ is but one example. For a given topos $\mathcal{E}$ These would be toposes $\mathcal{L}$ equipped with a functor $\mathcal{L}\to \mathcal{E}$ (*not* a [geometric morphism](https://ncatlab.org/nlab/show/geometric+morphism#definition), *or* a [logical functor](https://ncatlab.org/nlab/show/logical+functor)), but presumably finite-limit-preserving, fully faithful, and probably a few other things (eg structural constructions in ZFC that are absolute). Note that these are *not* internal categories, since they should be as "tall" as the ambient topos. I have no idea how one would actually construct such a topos corresponding to $L$, except by constructing a model of ZFC from the (boolean etc) topos, forming $L$, and then taking its category of sets, and then relying on the [material-structural adjunction](https://ncatlab.org/nlab/show/material-structural%20adjunction) to get the faithful functor of interest.


