While reading Hyland's paper on the effective topos [retyped version here] in the L. E. J. Brouwer Centenary Symposium, specifically prop. 16.3, I realized that the following proposition is implicit:
Main proposition. Working in a constructive math setting, with $\Omega$ the set of truth values (partially ordered by implication), if $f\colon \Omega \to \Omega$ is order-preserving, then the smallest nucleus $j\colon \Omega \to \Omega$ such that $f \leq j$ is given by $$ p \; \mapsto \; \forall q:\Omega.\,((f(q)\Rightarrow q)\land(p\Rightarrow q)\;\Rightarrow\; q) $$ i.o.w. $$ p \; \mapsto \; \bigwedge\{q\in\Omega : f(q)\leq q\text{ and }p\leq q\} $$ Here we recall that a nucleus (in this context also known as a “Lawvere-Tierney topology” or “local operator”) is a map $j\colon\Omega\to\Omega$ satisfying ⓐ $j(p_1\land p_2) = j(p_1) \land j(p_2)$, ⓑ $p\leq j(p)$ and ⓒ $j(j(p)) = j(p)$.
Now Hyland doesn't give a proof (nor, indeed, an explicit statement) of the above proposition, so I worked one out by myself, which is rather straightforward but still a bit long (and possibly confusing due to the number of nested assumptions involved at various points). I am putting it at the bottom of this question. My questions concern the proposition and its proof, but also the following corollary:
Corollary (“external reformulation”). Let $L$ be a frame and $f\colon L\to L$ be an order-preserving map that also satisfies (★) $f(p\land q)\land q = f(p)\land q$ (in particular, this condition (★) holds if $f$ is a prenucleus, i.e., when $f$ satisfies ⓐ and ⓑ above). Then the smallest nucleus $j\colon L\to L$ such that $f\leq j$ is given by $p \; \mapsto \; \bigwedge\{q\in L : f(q)\leq q\text{ and }p\leq q\}$ as above.
Proof of the corollary: First, the fact that any prenucleus satisfies (★) is clear because $f(p\land q)\land q = f(p) \land f(q) \land q = f(p)\land q$. Now in the topos of sheaves over $L$, the subobject classifier is given by $\Omega(q) = \{p\in L : p\leq q\}$, we define a morphism of sheaves $\Omega \to \Omega$ which is given by $p \mapsto f(p)\land q$ on $\Omega(q)$: the condition (★) ensures that this gives a well-defined morphism of sheaves, which we can also call $f$ (we can say that $f$ “internalizes”). Applying the main proposition to $f$ gives the desired $j$ (we use the fact that any nucleus $L\to L$ is, in particular, a prenucleus, so it internalizes to $\Omega$). ∎
Now for the actual questions (I realize they are vague, but I'm trying to get a sense of what is going on and, while I understand the proof, I feel like I'm missing the forest for the trees):
I realize that the proposition (and its corollary) must be considered obvious by experts because Hyland doesn't bother to give a proof, nor, indeed to really state the statement (in his case $f(q)$ is “$\exists x:X.(a(x) \Rightarrow q)$” for some $a\colon X\to \Omega$, but this doesn't seem to matter). Still, is it considered a standard result? Does it have a name? Is there a written reference for it?
What is going on in the proof of the main proposition? I can't decide whether the way I wrote it is needlessly complicated or whether it's just long because I wrote down all the details. Is there a way to simplify it? A more fancy way of writing it? (There seems to be a kind of fixed point and/or inductive construction involved, but I can't put my finger on it. Note also that the proposition tells us that $f\colon\Omega\to\Omega$ is a nucleus iff it satisfies: $f(p) \; \Leftrightarrow\; \forall q:\Omega.\,((f(q)\Rightarrow q)\land(p\Rightarrow q)\,\Rightarrow\, q)$, which is a curious way of defining nuclei, and I can't decide if this is interesting.)
The construction “$\forall q:\Omega. ((\text{something}\Rightarrow q)\Rightarrow q)$” seems to come up a lot, e.g., in Girard's system F we can define $p_1\land p_2$ as $$ \forall q:\Omega. ((p_1\Rightarrow p_2\Rightarrow q)\Rightarrow q) $$ and $p_1\lor p_2$ as $$ \forall q:\Omega. ((p_1\Rightarrow q)\land(p_2 \Rightarrow q)\;\Rightarrow\; q) $$ which are very reminiscent of the definition above. So, is this part of a more general idea? What's the moral of the story here?
What about the proof of the corollary? Proving an “external” result about frames by reasoning internally in the topos of sheaves might be of bad taste. In principle I think I know how to convert the “internal” proof to an “external” one, but it seems like it will make things even more messy and unreadable. Is there a better way to do it?
Proof of the main proposition:
Because this proof involves a lot of nested assumption, I will use the symbols ‘‹’ and ‘›’ to mark where assumptions start and end (e.g.: “‹ assume $p$ (…) then $q$ › : thus $p \Rightarrow q$”): hopefully this will make things easier to read.
Define $k(p)$ be the statement “any truth value $q$ such that $f(q) \Rightarrow q$ and $p \Rightarrow q$ are true, is itself true”.
We are to show that $k$ is the smallest nucleus $j$ such that $f\leq j$. This follows from the following sub-points.
(1) We have $p \leq k(p)$. Indeed, ‹ assume $p$ holds; then any $q$ such that $p \Rightarrow q$ is true is itself true, so $k(p)$ holds › : this shows $p\Rightarrow k(p)$, i.e. $p \leq k(p)$. ∎
(2) If $p \leq p'$ then $k(p) \leq k(p')$. Indeed, ‹ assume $p \Rightarrow p'$. ‹ Now assume $k(p)$. ‹ If $q$ is such that $f(q) \Rightarrow q$ and $p' \Rightarrow q$, then also $p \Rightarrow q$ (since $p \Rightarrow p'$). So $q$ holds by $k(p)$. › This shows $k(p')$. › So $k(p) \Rightarrow k(p')$ › : this shows that $p \Rightarrow p'$ implies $k(p) \Rightarrow k(p')$, i.e. $p \leq p'$ implies $k(p) \leq k(p')$, as claimed. ∎
(3) We have $k(p_1\land p_2) \leq k(p_1)\land k(p_2)$. Indeed, $k(p_1\land p_2) \leq k(p_1)$ by (2), and also $k(p_1\land p_2) \leq k(p_2)$ for the same reason, which shows $k(p_1\land p_2) \leq k(p_1)\land k(p_2)$. ∎
(4) We have $k(p_1)\land k(p_2) \leq k(p_1\land p_2)$. Indeed, ‹ assume $k(p_1)$ and $k(p_2)$. ‹ Now assume $q$ is such that $f(q) \Rightarrow q$ and $p_1\land p_2 \Rightarrow q$, that is, $p_1 \Rightarrow p_2 \Rightarrow q$. Let $q'$ be the statement “$p_2 \Rightarrow q$”. ‹ Assume $f(q')$ holds. ‹ Assume that $p_2$ holds: then $q'$ equals $q$, so $f(q)$ equals $f(q')$, which holds. So $q$ holds since we have $f(q) \Rightarrow q$ › : this shows that $p_2 \Rightarrow q$, that is, $q'$. › So we have just shown $f(q') \Rightarrow q'$. But we also have $p_1 \Rightarrow q'$. So by $k(p_1)$, we get $q'$. So now we have $f(q) \Rightarrow q$ and $p_2 \Rightarrow q$. So by $k(p_2)$ we get $q$. › This shows $k(p_1\land p_2)$. › So $k(p_1)\land k(p_2) \Rightarrow k(p_1\land p_2)$, i.e. $k(p_1)\land k(p_2) \leq k(p_1\land p_2)$. ∎
(5) We have $k(k(p)) = k(p)$. Indeed, ‹ assume $k(k(p))$. ‹ Now assume $q$ is such that $f(q) \Rightarrow q$ and $p \Rightarrow q$. ‹ If $k(p)$ holds, then $q$ holds by the very definition of $k(p)$ › : this shows that $k(p) \Rightarrow q$. But now we have $f(q) \Rightarrow q$ and $k(p) \Rightarrow q$, so $q$ holds by $k(k(p))$. › This shows $k(p)$. › So we have shown $k(k(p)) \Rightarrow k(p)$, i.e. $k(k(p)) \leq k(p)$, and this is an equality by (1). ∎
(6) Statements (1), (3), (4) and (5) together tell us that $k$ is a nucleus.
(7) Furthermore, we have $f\leq k$. Indeed, ‹ asssume $f(p)$ holds. ‹ If $q$ is such that $f(q) \Rightarrow q$ and $p \Rightarrow q$, then $f(q)$ holds because $p \leq q$ and $f(p) = \top$ and $f$ is order-preserving, so $q$ also holds. › This shows $k(p)$. › So we have shown $f(p) \Rightarrow k(p)$, i.e., $f\leq k$. ∎
(8) If $j$ is a nucleus such that $f\leq j$ (that is, $f(q) \Rightarrow j(q)$ for all $q$), then we have $k\leq j$. Indeed, ‹ assume $k(p)$ holds. ‹ If $f(j(p))$ holds, then $j(j(p))$ holds by $f\leq j$; but this is just $j(p)$ as $j$ is a nucleus. › This shows $f(j(p)) \Rightarrow j(p)$. On the other hand, we also have $p \Rightarrow j(p)$ as $j$ is a nucleus. So, applying the definition of $k(p)$ to $q := j(p)$ we get see that $j(p)$ holds. › So $k(p) \Rightarrow j(p)$ for all $p$, i.e., $k\leq j$. ∎
(9) Statements (6), (7) and (9) together tell us that $k$ is the smallest nucleus $j$ such that $f\leq j$.
This concludes the proof of the main proposition. ∎
