2
$\begingroup$

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

$\endgroup$
  • $\begingroup$ Personally, I follow Mike Shulman (in his stack semantics paper) in using the corner quotes to denote that formalization is left to the reader. For instance, I'd write $\mathcal{E} \models \ulcorner\text{$f$ is surjective}\urcorner$ to mean $\mathcal{E} \models \forall y:Y. \exists x:X. f(x) = y$. $\endgroup$ – Ingo Blechschmidt Oct 25 '16 at 9:22
3
$\begingroup$

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

$\endgroup$
1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thanks for the answer! I'm a bit confused - it seems that both before and after the word "however" you essentially say what I write is fine. Then why the "however"? I think I'm missing something. $\endgroup$ – Arrow Oct 24 '16 at 23:50
  • $\begingroup$ Uh, before the "however" was supposed to read "What you're doing is not ideal, but not a problem", and after the "however" was supposed to read "If you have this particular convention, it is really not a problem at all". $\endgroup$ – Mees de Vries Oct 25 '16 at 0:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.