Intuition for pseudo-points and the inductive step in Johnstone's proof of Deligne's completeness theorem

Question

In Johnstone's Topos Theory appears the following lemma.

7.41 Lemma. Let $P$ be a pseudo-point of $\mathsf C$, $X$ a $J$-sheaf on $\mathsf C$, and $x,y$ two distinct element of $P(X)$. Let $(V_j\to V)$ be a finite $J$-covering family in $\mathsf C$, and $v$ and element of $P(h_V)$. There there exists a refinement $Q$ of $P$ such that (a) the images of $x,y$ under the natural map $P(X)\to Q(X)$ are distinct, and (b) the image of $v$ in $Q(h_V)$ is in $\bigcup _j\; \operatorname{im}(Q(h_{V_j})\to Q(h_V))$.

So the refinement continues to "separate" $x,y$, which have to do with the sheaf $X$ (but not the covering family $(V_j\to V)$), but has the additional property (b), which seems to be only about representables associated to the covering family $(V_j\to V)$ (and not the sheaf $X$).

Questions.

1. What is a nice conceptual intuition for the notion of a pseudo-point? Is there a geometric intuition?
2. What's the idea behind property (b)?

This lemma seems to be topological in nature, but I just can't seem to unpack the content of property (b) of the refinement.

Answer 1

Johnstone's proof based on this lemma follows in fact the original proof of Deligne which can be found in the appendix "Criteria for the existence of points" to SGA 4, vol. VI. Both the original and a TeX reedition from 2015 can be found here.

The idea behind the notion of pseudo-point is very simple; it is just a description of a point using only the site. Since a point of a topos is by Diaconescu's theorem the same as a continuous flat functor from the site to $\mathcal{S}et$, when the site has finite limits this is the same as a filtered colimit of representable functors that in addition sends covering families to jointly surjective arrows in $\mathcal{S}et$. Therefore, one can identify the opint with a filtered diagram $(U_i)_{i \in I}$ in the site, which is precisely what Johnstone calls a pseudo-point.

As for property (b), it is just the inductive condition that ensures that in the end covering families are sent to jointly surjective arrows in $\mathcal{S}et$. Indeed, the continuous flat functor corresponding to the pseudo-point, evaluated in $C$, is precisely the filtered colimit $\lim [U_i, C]$, and condition (b) translates to a refinement of the filtered diagram to ensure the property above.

This way of proving Deligne's theorem follows closely Henkin's proof of Gödel's completeness theorem (which is why Deligne's theorem is referred to as a completeness theorem), since the inductive process of refining the pseudo-point is analogous to that of adding constants that witness existential statements. In both cases, one has to perform this addition countably many times since the introduction of new constants increases the set of formulas of the theory, which in Deligne's case boils down to applying lemma 9.4 repeatedly to produce a countable sequence of refinements of the pseudo-point. The analogy became evident with Joyal's proof of the completeness theorem for coherent logic, which is inspired by Deligne's proof and follows precisely this pattern.