@godelian: For the Friedman translation with respect to a fixed formula $\alpha$, use the topology given by $\varphi \mapsto \varphi \vee \alpha$ (read this as a term in the internal language). Often, one needs to first apply the double negation translation and then the Friedman translation; this can be realized by the topology $\varphi \mapsto ((\varphi \Rightarrow \alpha) \Rightarrow \alpha)$. Fun fact: Let $X$ be a topological space and $x \in X$ be a point. Then, for suitable $\alpha$, this topology gives the subtopos Sh$(\{x\})$ of Sh$(X)$. This has useful consequences (see the notes).

@godelian: See very rough notes, still work in progress, on GitHub. Lots of explanations and references are still missing, also some proofs and a proper copyediting. The material you are interested in is in section 6 (Modalities), in particular section 6.6 (The $\Box$-translation). I'd be happy to discuss any questions regarding these notes!

@godelian: Such a development is indeed possible, using Lawvere-Tierney topologies. For instance, let $\varphi^{\neg\neg}$ denote the Gödel-Gentzen negative translation of a formula $\varphi$. Then $\mathcal{E} \models \varphi^{\neg\neg}$ is equivalent to $\mathrm{Sh}_{\neg\neg}(\mathcal{E}) \models \varphi$, where $\mathrm{Sh}_{\neg\neg}(\mathcal{E})$ denotes the subtopos of sheaves in $\mathcal{E}$ with respect to the double negation topology. The case for the Friedman translation is similar. I can make details available, if you are interested.

Working link.

A small correction: You write "For instance, probably 1 and 2 can be expressed in terms of some allowable syntax in topos theory, but 3 can't.". This is not true: In fact, a sheaf $F$ of $\mathcal{O}_X$-modules fulfils (3) if and only if from the point of view of the internal language of the sheaf topos $\mathrm{Sh}(X)$, $F$ is a coherent module (as usually defined in an ordinary course on commutative algebra with no sheaves in sight).

Thank you for the additional reference. But I think that these slides also target a general audience. For the moment, it appears that "Lokal" was academically only used in the linked seminar in Hannover.

Indeed, the terms "Örtlichkeit" and "Ort" do not allude to the algebraic underpinnings very well -- this is an important point, thank you. But I'd still prefer a proper German translation.

Thank you. Do you know references which are pitched at a higher level? (The notes you linked to are targeted at a general lay audience.) I only know of a single one, namely a seminar in Hannover of 2006.