The equivalences between points in a locale in constructive mathematics

Question

I am currently following the definitions of the book Frames and Locales and those in the articles Pointfree topology and constructive mathematics and Topo-logie. There are at least three ways of talking about the points in a locale $E$:

1. As frame morphisms $E \to \Omega$, where $\Omega$ is the set of truth values.
2. As completely prime filters $F \subseteq E$.
3. As meet-irreducible elements of the frame $E$.

To proof that they are indeed equivalent we need to construct bijections between all of them but it looks like these bijections depend on non-constructive facts.

1. Given a frame morphism $f \colon E \to \Omega$, we can show that $f^{-1}[\{\top\}]$ have the following properties:
   • $1 \in f^{-1}[\{\top\}]$.
   • For $u,v \in f^{-1}[\{\top\}]$, $u \wedge v \in f^{-1}[\{\top\}]$.
   • If $u \in f^{-1}[\{\top\}]$ and $v \in E$ is such that $u \leq v$, then $v \in f^{-1}[\{\top\}]$.
   • If $\bigvee_{i \in I} u_i \in f^{-1}[\{\top\}]$, then $\neg ( \forall i \in I (f(u_i) = \bot) )$.

Here, it looks like we need $\neg (\forall x \in X. \phi(x)) \vdash \exists x \in X. \phi(x)$ and $b \in \Omega, \neg(b = \bot) \vdash b = \top$ to be valid, but in a constructive setting this may not be the case.

2. Given a completely prime filter $F \subseteq E$, we can show that $\bigvee (E \setminus F) = p$ satisfies:
   • $\neg ( p = 1)$.
   • If $u \wedge v \leq p$, then $\neg( u \in F \,\&\, v \in F )$.

To complete the proof that $p$ is a meet-irreducible element, we would neet to use $\neg( \phi \,\&\, \psi ) \vdash \neg\phi \vee \neg\psi$, and since it is a part of one constructive taboo, I am not sure if that is a valid inference in a constructive setting.

3. Given a meet-irreducible element $p \in E$, we can show that $F = E \setminus (\downarrow p)$ satisfies:
   • $1 \in F$.
   • If $u,v \in F$, then $\neg( u \leq p) \,\&\, \neg( v \leq p )$.
   • If $u \in F$ and $v \in E$ is such that $u \leq v$, then $v \in F$.
   • If $\bigvee_{i \in I} u_i \in F$, then $\neg( \forall i \in I (u_i \leq p) )$.

Again, we would need $\neg (\forall x \in X. \phi(x)) \vdash \exists x \in X. \phi(x)$ and also $\neg\phi \wedge \neg\psi \vdash \neg(\phi \vee \psi)$ to be valid inferences.

4. Given a frame morphism $f \colon E \to \Omega$, we can show that $p = \bigvee (f^{-1}[\{\bot\}])$ satisfies:
   • $\neg ( p = 1 )$.
   • If $u \wedge v \leq p$, then $f(u) \wedge f(v) = \bot$.

Here I am not really sure if we can conclude $f(u) = \bot$ or $f(v) = \bot$, but I would say we can't. The constructions of frame morphisms from completely prime filters or meet-irreducible elements involve using a characteristic function, but I don't think I undestand well how to work with this set of truth values $\Omega$, as in the article of Graham Manuell.

So the question is, are these equivalences valid in a constructive setting? If they are not, what would be a model where some equivalences fail? And what would be the definition of a point in a constructive setting?

Answer 1

The fourth bullet item in 1 should be $$ \bigvee_iu_i\in f^{-1}(\{\top\}) \iff f(\bigvee_iu_i)=\top\iff \bigvee_if(u_i)=\top, $$ because frame morphisms preserve joins. Remembering how elements of $\Omega$ correspond truth values of propositions ($x\iff(x=\top)$) and that joins in $\Omega$ correspond to existential quantification, we find that the computation above gives $\exists i\,(u_i=\top)$, as desired.

In other words, the source of your difficulty in 1 is that $\bot$ should never have entered the picture.

In 2, I think you should take $p$ to be $\bigwedge F$ rather than $\bigvee(E\setminus F)$. (And the inference you weren't sure about is, in fact, not constructively valid.)

Similarly in 3, I think you want $F$ to be the upward closure of $p$, not the complement of the downward closure.

And in 4, I think you want $F$ to be $f^{-1}(\{\top\})$.

Everything I've said here about 2, 3, and 4 can be viewed as "the same" as what I said about 1: Avoid negation, whether explicit as $\neg$ or implicit in $\bot$ or in the set-difference operation, whenever possible. Constructive mathematics is much happier without unnecessary negations.