(Correct?) notation for emphasizing an internal interpretation of a sentence I'm writing some notes for myself and sometimes I write sentences which are meant for interpretation in the internal language of a topos. I'm looking for some kind of notation that I can put around the stuff I want to interpret - be it a sequence of formal symbols, or plain language, or a mixture of the two - that will mean "interpret this stuff in the internal language".
There are two pieces of notations which seem related to me:


*

*From Borceux vol III, Defintion 6.3.3:
Definition. Let $\mathcal E$ be a topos. The interpretation of the language of $\mathcal E$ consists in specifying, among other things, for each term $\tau$ of type $A$ with variables $x_1,\dots ,x_n$ of respective types $X_1,\dots ,X_n$, a realization $\ulcorner \tau \urcorner:X_1\times \cdots \times X_n\to A$, and for each formula $\phi$ with free variables $x_1,\dots ,x_n$ of types $X_1,\dots ,X_n$ a truth table $\ulcorner \phi \urcorner:X_1\times\cdots \times X_n\to \Omega$

*From Borceux vol III, final paragraph of proof of Proposition 6.5.5:
Definition. Let $\mathcal E$ be a topos. If $\phi$ is a formula, write $[\!\!|\;\phi\; |\!\!]$ for the subobject classified by its truth table.
I've never really studied logic, so I'm asking here just to be sure and get warned of dangerous mistakes - are corner quotes precisely what I'm looking for?
That is, suppose I want somebody to interpret the stuff below in the internal language of a topos which is clear from context.
$$U\in S\iff \exists f\in Y^X\text{ such that }U=f^{-1} Y$$
Should I simply write copy it with corner quotes? $$\ulcorner U\in S\iff \exists f\in Y^X\text{ such that }U=f^{-1} Y \urcorner$$
 A: There is no "standard" or even common conventions here.  What I typically do is use logic/type theory notation for internal constructions.  I only use set-theoretic notation, in particular $\in$, externally.  So for example I'd write $f \in \textrm{Hom}(A,B)$ versus $f : B^A$, the former being an unambiguously external statement and the latter being unambiguously internal.  (To be frank, though, I often use type theoretic notation externally as well, e.g. $f : \textrm{Hom}(A,B)$.)
In general logic/type theory has a decent story for keeping the object language and the meta-language separate so I tend to use those conventions.  What I would write for the situation you described is something like $$S : \Omega^{\Omega^X}, U:\Omega^X \vdash (U\in_{\Omega^X} S \Leftrightarrow \exists f:Y^X.U =_{\Omega^X} f^{-1}Y)$$
Admittedly, I'd probably drop the subscripts for concision, and I'd just use function application syntax rather than the $\in_{\Omega^X}$ relation, i.e.
$$S : \Omega^{\Omega^X}, U:\Omega^X \vdash (S(U) \Leftrightarrow \exists f:Y^X.U = f^{-1}Y)$$
I'd use the $\ulcorner\!\_\!\urcorner$ syntax (after defining it at least informally as the interpretation function) as follows:
$$\text{Let }f\in\textrm{Hom}(X,Y)\text{ then }x:A\vdash\ulcorner f\urcorner(x): B$$
In other words, the $\ulcorner\!\_\!\urcorner$ syntax is just a function mapping some external construct, e.g. an arrow, to a term in the object language, but it is not a judgement (the $\Gamma \vdash t :A$ things which can be read as "in context $\Gamma$, the term $t$ has type $B$").  Judgements are things which are true or false in the meta-language, terms are just pieces of syntax given meaning by judgements.  There may be several different judgements. Propositions in a topos are $\Omega$-valued terms. ($\Omega$ being the subobject classifier.)  For this reason, I prefer to consistently use the type theoretic approach rather than a more logical approach.  For the earlier examples, this may mean I consider judgements like $$S : \Omega^{\Omega^X}, U:\Omega^X \vdash t : \{1\ |\ S(U) \Leftrightarrow \exists f:Y^X.U = f^{-1}Y\}$$ or $$\vdash t' : \{S : \Omega^{\Omega^X}, U:\Omega^X\ |\ S(U) \Leftrightarrow \exists f:Y^X.U = f^{-1}Y\}$$  This helps emphasize that there may be some non-trivial structure to these propositions; they aren't just true or false. Sections 4 and 5 of this (future) book chapter provide a fairly comprehensive introduction to similar ideas leaning a bit more toward the "logic" side.
To summarize, the meta-logic (i.e. the external logic) talks about judgements, the judgements define the meaning of the object language (i.e. the internal type theory).
A: Typically, I would say that that is imprecise, but not terribly so. The operation $\phi \mapsto \ulcorner \phi \urcorner$ is an operation that takes a formula $\phi$ (an element of the set of formulas in whatever language you have defined) to some object in the topos (an arrow to the subobject classifier, or, equivalently, a subobject). Since your phrase contains the English words "such that", it is not a sentence in the formal language.
Assuming that $\in$ is a (possibly defined) relation in your language, and the symbol $(\cdot)^{-1}$ is a (possibly defined) function in your language, the phrase
$$
U \in S \leftrightarrow \exists f \in Y^X(U = f^{-1}Y).
$$
is a formula in your formal language, and hence is a valid argument to the $\ulcorner \cdot\urcorner$ function.
However, if you have established the abuse of notation that you will write a logical "formula" in the meta-language, where you take that meta-language phrase to be the logical language formula which "ordinarily" means what you have written in the meta-language -- which is not a weird abuse of notation -- then this is fine.
Really, the point is to be understood more than to be exactly correct with your notation at all times.
