I consider locales as spaces with imaginary points where these imaginary points exist in larger set theoretic universes. In fact, locales should be thought of as spaces with imaginary points where in larger universes the points may still be imaginary, but there is eventually a large enough universe where the points will all appear as concrete objects. There are many examples of such spaces with imaginary points such as the space of all points in every dense open set, the space of all $\omega_{1}$-length branches on an Aronszajn tree or more generally the space of all threads in an empty inverse limit of sets, and the set of all generic ultrafilters on a poset. In all of these examples, one can associate a frame with these spaces with imaginary points. Furthermore, forcing can add the desired imaginary object, and forcing can also add points to locales without disrupting the locale too much. With that being said, extending a frames to a non-forcing extension can make all of the resulting frames homeomorphic and thus while these extensions add points, these extensions also collapse all of the differences between the frames.
Suppose that $M$ is a model definable with parameters in $V$. $M$ does not need to be a model of ZFC, ZF or much of anything for that matter. Furthermore, $M$ does not need to be well-founded. Suppose now that $$M\models\text{$L$ is a frame}.$$ Then $L$ will still be a distributive lattice in $V$.
We say that an ideal $I\subseteq L$ is an $M$-ideal if whenever $R\in M,R\subseteq I$, we have $\bigvee R\in I$. Let $L^{+V}$ be the set of all $M$-ideals $I\subseteq L$. Then $L^{+V}$ is a frame in $V$. The way to interpret this frame without resorting to ideals is to observe that $L^{+V}$ is the smallest frame in $V$ containing $L$ such that if $C\subseteq L,C\in M$, then $\bigvee^{L^{+V}}C=\bigvee^{L}C$.
The theory of extending frames to larger universes behaves remarkably well when we limit our scope to the forcing extensions. Since complete Boolean algebras are special kinds of frames and are essential to point-free topology, it makes most sense to study the interpretation of frames in forcing extensions using the Boolean-valued model approach to forcing. I call this theory Boolean-valued pointfree topology. The downside to Boolean-valued pointfree topology is that it only works with forcing extensions and not with other extensions.
Suppose that $L$ is a frame and $B$ is a complete Boolean algebra which is a subframe of $L$. Then $L$ can be considered as a $B$-valued structure where we
set $\|x\leq y\|$ to be the largest element $b\in B$ where $x\wedge b\leq y\wedge b$ and where we set $\|x=y\|$ to be the largest element $b\in B$ where
$x\wedge b=y\wedge b$. Since $L$ is a $B$-valued structure closed under complete mixing, we can consider $L$ as an object in the forcing extension
$V^{B}$ and $$V^{B}\models\text{$L$ is a frame}.$$
$\textbf{Theorem:}$ Suppose that $P$ is one of the properties:
regularity, complete regularity, paracompactness,
ultraparacompactness, zero-dimensionality. Then $L$ satisfies $P$ if
and only if $$V^{B}\models\text{$L$ satisfies $P$}.$$
Now, if $L$ is a frame and $B$ is a complete Boolean algebra, then $B$ is a subframe of the frame coproduct $L\oplus B$. Therefore,
$L\oplus B$ is a $B$-valued structure and $$V^{B}\models\text{$L\oplus B$ is a frame}.$$ It turns out that $L\oplus B$ is the correct way to interpret a frame $L$ as a frame in $V^{B}$ and the $L\oplus B$ is the Boolean-valued structure that corresponds to the $L^{+V[G]}$ construction. The following results illustrate the soundness of this construction.
$\textbf{Theorem:}$ Suppose that $P$ is one of the following
properties: Compactness, locally connected connectedness, compact
connectedness, regularity. Then $L$ satisfies property $P$ if and only
if $$V^{B}\models\text{$L\oplus B$ satisfies property $P$}.$$
Passing to forcing extensions improves the topological properties of the spaces.
$\textbf{Theorem:}$ Suppose that $P$ is one of the following
properties: Paracompactness, ultraparacompactness, complete
regularity, zero-dimensionality, second countability. If $L$ satisfies
property $P$, then $$V^{B}\models\text{$L\oplus B$ satisfies property
$P$ as well}.$$
Now, if $L$ is a frame, then the points in $L$ are the frame homomorphisms $\phi:L\rightarrow 2$. One can extend this definition of a point to Boolean-valued models
where we define a $B$-valued point to be a frame homomorphism $\phi:L\rightarrow B$. It turns out that the frame homomorphisms $\phi:L\rightarrow B$ form a $B$-valued
structure where we set $\|\phi=\theta\|$ to be the largest $b\in B$ where $\phi(x)\wedge b=\theta(x)\wedge b$ for each $b\in B$. This definition of a point is coherent with the theory that we have developed since the frame homomorphisms $\phi:L\rightarrow B$ correspond with the $\dot{x}\in V^{B}$ such that
$$V^{B}\models\text{$\dot{x}$ is a point in the frame $L\oplus B$}.$$
If $L$ is a frame, then let $B_{L}=\{x\in L|x^{**}=x\}$. Then $B_{L}$ is the smallest dense sublocale of the frame $L$, and $B_{L}$ is a complete Boolean algebra. The mapping $\phi:L\rightarrow B_{L}$ is a frame homomorphism. Therefore, forcing eventually adds points to every frame. For the regular frames, we can do much better than simply adding a few points using forcing just to satisfy the critics of point-free topology.
$\textbf{Theorem:}$ Suppose that $L$ is a regular frame. Then there is
a complete Boolean algebra $B$ such that $$V^{B}\models\text{$L\oplus
B$ is Polish space}.$$
Therefore, we should not think of point-free topology as just the study of spaces with imaginary points, but point-free topology is the study of spaces that will eventually become Polish spaces (unless you like lower separation axioms). Not only does Boolean-valued point-free topology justify point-free topology, but Boolean-valued point-free topology also justifies the separation axiom regularity since the regular frames will eventually become Polish spaces.
To be continued.
I am going to get back to this answer later with more details that describe what happens when the model $M$ is not a ground model of $V$ and in particular when $M$ is not well-founded in $V$. I will need more time to think about frames in these ill-founded models.
