Return to Answer

Depending on whether by ground model of ZFC already have "things" this locale can have points or not.

If this locale is non-empty, I can look at the category of sheaves over it. It is a topos, and hence it admits something called "internal logic" which makes into a new "set theoretical universe" in which you have a canonical "thing". I refer you to classical books on topos theory for that notion (Moerdijk & MacLane "sheaves in geometry and logics, The volume 3 of Borceux's "Handbook of categorical algebra" are both very classical and very good. Chapter three of Collin McLarty "Elementary categories, elementary toposes" is also very focused on categorical).

Depending on whether your ground model of ZFC already have "things" this locale can have points or not. (of course the most interesting case is when it does not)

If this locale is non-empty, I can look at the category of sheaves over it. It is a topos, and hence it admits something called "internal logic" which makes into a new "set theoretical universe" in which you have a canonical "thing". I refer you to classical books on topos theory for that notion (Moerdijk & MacLane "sheaves in geometry and logics, The volume 3 of Borceux's "Handbook of categorical algebra" are both very classical and very good. Chapter three of Collin McLarty "Elementary categories, elementary toposes" is also very focused on categorical logic so give a shorter introduction to the topic).

Here is a very brief sketches of the connection between this and forcing. I'll describe you how I understand forcing, this is quite different from how it is generally described by logician, but this how peoples in topos theory/categorical logic understand it. And it makes the connection with those "locales of imaginary points" very clear.

It should be equivalent to the classical description..

Let say I want to construct some forcing extension that add one "thing" where "thing" can be for example "a random real number", "a generic real", "a surjection $\mathbb{N} \twoheadrightarrow X$" for some fixed set $X$, "a non-principal ultrafilter", a "generic filter"...

The first step is to look at the "space of all thing", i.e. the classifying locales of the theory of "thing". So "thing" has to be a nice (geometric) notion so that such a classyfing space exists.

Depending on whether by ground model of ZFC already have "things" this locale can have points or not.

Then I need to check that this classifying locale of 'things' is non trivial. There are a lots of way to do that, and it really depends on the type of 'thing' you consider, though a very common technics to do that is the "Localic Bair category theorem" which says that an arbitrary intersection of dense sublocales is a dense sublocales. Of course this can fail. This happen for example if "things" are surjection $F \twoheadrightarrow \mathbb{N}$ with $F$ a fixed finite set.

If this locale is non-empty, I can look at the category of sheaves over it. It is a topos, and hence it admits something called "internal logic" which makes into a new "set theoretical universe" in which you have a canonical "thing". I refer you to classical books on topos theory for that notion (Moerdijk & MacLane "sheaves in geometry and logics, The volume 3 of Borceux's "Handbook of categorical algebra" are both very classical and very good. Chapter three of Collin McLarty "Elementary categories, elementary toposes" is also very focused on categorical).

This is not quite the end of the story because this new "mathematical universes" is not quite a model of ZF for two reasons:

• It corresponds to a "structural set theory" whereas ZF is a "material set theory" (to use the terminology of Mike Shulman's excellent paper that I recommend). This means that it is not based on the $\in$ relation, but rather on functions between sets. Fortunately the paper I just mention present some constructions (the "Cole-Mitchell-Osius" construction) that allow to go from a structural set theory to a material set theory, basically by looking at the class of all trees.

• It might not satisfies the axiome of chocie or the law of excluded middle. But fortunately there is a nice topos theoretic construction which given a locale $L$ (or a more general Grothendieck topos) produces a covering of $L$ by a boolean locale $B$. The internal logic of that boolean locale also has a "thing" and this times satisfies the law of excluded middle and, if your ground model satisfies choice, the axiom of choice.

So to sum up, the forcing extension adding a "thing" is obtained hes the Cole-Mitchell-Osius construction applied to the category of sheaves of a boolean cover of the classifying locale of things. Of course, if you are already doing topos theory or cartegorical logic, you don't really care about getting a model of ZFC exactly, so you tend to get ride of the Cole-Mitchell-Osius construction, and even often of the boolean cover, and so you remeber the slogan that "forcing = sheaves over classyfing spaces".

For example this $A \simeq_p B$ you are describing corresponds to the fact that the locale of isormorphisms between $A$ and $B$ is non-trivial.

Here is a very brief sketches of the connection between this and forcing. I'll describe you how I understand forcing, this is quite different from how it is generally described by logician, but this how peoples in topos theory/categorical logic understand it. And it makes the connection with those "locales of imaginary points" very clear.

It should be equivalent to the classical description..

Let say I want to construct some forcing extension that add one "thing" where "thing" can be for example "a random real number", "a generic real", "a surjection $\mathbb{N} \twoheadrightarrow X$" for some fixed set $X$, "a non-principal ultrafilter", a "generic filter"...

The first step is to look at the "space of all thing", i.e. the classifying locales of the theory of "thing". So "thing" has to be a nice (geometric) notion so that such a classyfing space exists.

Depending on whether by ground model of ZFC already have "things" this locale can have points or not.

Then I need to check that this classifying locale of 'things' is non trivial. There are a lots of way to do that, and it really depends on the type of 'thing' you consider, though a very common technics to do that is the "Localic Bair category theorem" which says that an arbitrary intersection of dense sublocales is a dense sublocales. Of course this can fail. This happen for example if "things" are surjection $F \twoheadrightarrow \mathbb{N}$ with $F$ a fixed finite set.

If this locale is non-empty, I can look at the category of sheaves over it. It is a topos, and hence it admits something called "internal logic" which makes into a new "set theoretical universe" in which you have a canonical "thing". I refer you to classical books on topos theory for that notion (Moerdijk & MacLane "sheaves in geometry and logics, The volume 3 of Borceux's "Handbook of categorical algebra" are both very classical and very good. Chapter three of Collin McLarty "Elementary categories, elementary toposes" is also very focused on categorical).

This is not quite the end of the story because this new "mathematical universes" is not quite a model of ZF for two reasons:

• It corresponds to a "structural set theory" whereas ZF is a "material set theory" (to use the terminology of Mike Shulman's excellent paper that I recommend). This means that it is not based on the $\in$ relation, but rather on functions between sets. Fortunately the paper I just mention present some constructions (the "Cole-Mitchell-Osius" construction) that allow to go from a structural set theory to a material set theory, basically by looking at the class of all trees.

• It might not satisfies the axiome of chocie or the law of excluded middle. But fortunately there is a nice topos theoretic construction which given a locale $L$ (or a more general Grothendieck topos) produces a covering of $L$ by a boolean locale $B$. The internal logic of that boolean locale also has a "thing" and this times satisfies the law of excluded middle and, if your ground model satisfies choice, the axiom of choice.

So to sum up, the forcing extension adding a "thing" is obtained hes the Cole-Mitchell-Osius construction applied to the category of sheaves of a boolean cover of the classifying locale of things. Of course, if you are already doing topos theory or cartegorical logic, you don't really care about getting a model of ZFC exactly, so you tend to get ride of the Cole-Mitchell-Osius construction, and even often of the boolean cover, and so you remeber the slogan that "forcing = sheaves over classyfing spaces".

For example for some structure $A$ and $B$, "being isomorphic in a forcing extention" is exactly the same as saying that the locale of isormorphisms between $A$ and $B$ is non-trivial.

Here is a very brief sketches of the connection between this and forcing. I'll describe you how I understand forcing, this is quite different from how it is generally described by logician, but this how peoples in topos theory/categorical logic understand it. And it makes the connection with those "locales of imaginary points" very clear.

It should be equivalent to the classical description..

Let say I want to construct some forcing extension that add one "thing" where "thing" can be for example "a random real number", "a generic real", "a surjection $\mathbb{N} \twoheadrightarrow X$" for some fixed set $X$, "a non-principal ultrafilter", a "generic filter"...

The first step is to look at the "space of all thing", i.e. the classifying locales of the theory of "thing". So "thing" has to be a nice (geometric) notion so that such a classyfing space exists.

Depending on whether by ground model of ZFC already have "things" this locale can have points or not.

Then I need to check that this classifying locale of 'things' is non trivial. There are a lots of way to do that, and it really depends on the type of 'thing' you consider, though a very common technics to do that is the "Localic Bair category theorem" which says that an arbitrary intersection of dense sublocales is a dense sublocales. Of course this can fail. This happen for example if "things" are surjection $F \twoheadrightarrow \mathbb{N}$ with $F$ a fixed finite set.

If this locale is non-empty, I can look at the category of sheaves over it. It is a topos, and hence it admits something called "internal logic" which makes into a new "set theoretical universe" in which you have a canonical "thing". I refer you to classical books on topos theory for that notion (Moerdijk & MacLane "sheaves in geometry and logics, The volume 3 of Borceux's "Handbook of categorical algebra" are both very classical and very good. Chapter three of Collin McLarty "Elementary categories, elementary toposes" is also very focused on categorical).

This is not quite the end of the story because this new "mathematical universes" is not quite a model of ZF for two reasons:

• It corresponds to a "structural set theory" whereas ZF is a "material set theory" (to use the terminology of Mike Shulman's excellent paper that I recommend). This means that it is not based on the $\in$ relation, but rather on functions between sets. Fortunately the paper I just mention present some constructions (the "Cole-Mitchell-Osius" construction) that allow to go from a structural set theory to a material set theory, basically by looking at the class of all trees.

• It might not satisfies the axiome of chocie or the law of excluded middle. But fortunately there is a nice topos theoretic construction which given a locale $L$ (or a more general Grothendieck topos) produces a covering of $L$ by a boolean locale $B$. The internal logic of that boolean locale also has a "thing" and this times satisfies the law of excluded middle and, if your ground model satisfies choice, the axiom of choice.

So to sum up, the forcing extension adding a "thing" is obtained hes the Cole-Mitchell-Osius construction applied to the category of sheaves of a boolean cover of the classifying locale of things.

For example this $A \simeq_p B$ you are describing corresponds to the fact that the locales of isormorphisms between $A$ and $B$ is non-trivial.

Here is a very brief sketches of the connection between this and forcing. I'll describe you how I understand forcing, this is quite different from how it is generally described by logician, but this how peoples in topos theory/categorical logic understand it. And it makes the connection with those "locales of imaginary points" very clear.

It should be equivalent to the classical description..

Let say I want to construct some forcing extension that add one "thing" where "thing" can be for example "a random real number", "a generic real", "a surjection $\mathbb{N} \twoheadrightarrow X$" for some fixed set $X$, "a non-principal ultrafilter", a "generic filter"...

The first step is to look at the "space of all thing", i.e. the classifying locales of the theory of "thing". So "thing" has to be a nice (geometric) notion so that such a classyfing space exists.

Depending on whether by ground model of ZFC already have "things" this locale can have points or not.

Then I need to check that this classifying locale of 'things' is non trivial. There are a lots of way to do that, and it really depends on the type of 'thing' you consider, though a very common technics to do that is the "Localic Bair category theorem" which says that an arbitrary intersection of dense sublocales is a dense sublocales. Of course this can fail. This happen for example if "things" are surjection $F \twoheadrightarrow \mathbb{N}$ with $F$ a fixed finite set.

If this locale is non-empty, I can look at the category of sheaves over it. It is a topos, and hence it admits something called "internal logic" which makes into a new "set theoretical universe" in which you have a canonical "thing". I refer you to classical books on topos theory for that notion (Moerdijk & MacLane "sheaves in geometry and logics, The volume 3 of Borceux's "Handbook of categorical algebra" are both very classical and very good. Chapter three of Collin McLarty "Elementary categories, elementary toposes" is also very focused on categorical).

This is not quite the end of the story because this new "mathematical universes" is not quite a model of ZF for two reasons:

• It corresponds to a "structural set theory" whereas ZF is a "material set theory" (to use the terminology of Mike Shulman's excellent paper that I recommend). This means that it is not based on the $\in$ relation, but rather on functions between sets. Fortunately the paper I just mention present some constructions (the "Cole-Mitchell-Osius" construction) that allow to go from a structural set theory to a material set theory, basically by looking at the class of all trees.

• It might not satisfies the axiome of chocie or the law of excluded middle. But fortunately there is a nice topos theoretic construction which given a locale $L$ (or a more general Grothendieck topos) produces a covering of $L$ by a boolean locale $B$. The internal logic of that boolean locale also has a "thing" and this times satisfies the law of excluded middle and, if your ground model satisfies choice, the axiom of choice.

So to sum up, the forcing extension adding a "thing" is obtained hes the Cole-Mitchell-Osius construction applied to the category of sheaves of a boolean cover of the classifying locale of things. Of course, if you are already doing topos theory or cartegorical logic, you don't really care about getting a model of ZFC exactly, so you tend to get ride of the Cole-Mitchell-Osius construction, and even often of the boolean cover, and so you remeber the slogan that "forcing = sheaves over classyfing spaces".

For example this $A \simeq_p B$ you are describing corresponds to the fact that the locale of isormorphisms between $A$ and $B$ is non-trivial.