(Correct?) notation for emphasizing an internal interpretation of a sentence

Question

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:

1. 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$

2. 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$$

Answer 1

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).

Answer 2

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.