I am reading Awodey's paper Structure in Mathematics and Logic: A Categorical Perspective and he is currently (p. 228-9) talking about how propositions, that is, elements $1\rightarrow P$, correspond to subobjects of $1$. Thus he constructs conjunction by saying that the conjunction of two elements of $P$ corresponds to the product of the corresponding subobjects of $1$. I am playing this all back in my head with the only model I know, which is the topos $\textrm{Set}$. Here the subobjects of $1$ form the small category $2$, so the formalism lacks resolution. Can someone give me another topos with logical semantics to try these things out on where we can really see what is going on, e.g. where the product looks more like a product?

  • 3
    $\begingroup$ It's actually hard to find toposes that are like $\mathbf{Set}$. Pretty much any other example will produce more interesting behavior. In particular, sheaves (and more simply, presheaves) will produce an unlimited number of examples and almost all the ones of interest. $\endgroup$ – Derek Elkins left SE Jul 10 '18 at 20:42
  • 1
    $\begingroup$ I second Derek's suggestion. A further source of toposes are models of computation; every such model yields a corresponding "realizability topos", of which the "effective topos" is the most famous. Their internal language is easy to understand, but their construction is not entirely trivial. If you are interested in set theory, then you might enjoy that any model $M$ of ZF yields a topos -- the objects are the elements of $M$ and the morphisms are what $M$ believes to be maps. $\endgroup$ – Ingo Blechschmidt Jul 11 '18 at 14:47
  • $\begingroup$ Finally, let me remark that you can spice up the topos of sets a little if you don't subscribe to classical logic as your metatheory. In the absence of the law of excluded middle, the powerset of the singleton set might not be exhausted by .$\emptyset$ and $\{\heartsuit\}$. $\endgroup$ – Ingo Blechschmidt Jul 11 '18 at 14:52
  • $\begingroup$ I don't know what you you mean by the "formalism lacks resolution" and I don't understand why the other comments are suggesting that you need to look at toposes other than Set for examples. Awodey's statement works in (the skeleton of) Set: the truth table for conjunction looks just like the operation table for the product of subobjects of $1$: $\emptyset \times x = x \times \emptyset = \emptyset$ and $1 \times 1 \equiv 1$. $\endgroup$ – Rob Arthan Jul 15 '18 at 22:03
  • 4
    $\begingroup$ My favorite toy topos is the category of directed multigraphs. Its logic is intuitionistic, and the structure of the subobject classifier is simple enough to draw, but more interesting than two points. $\endgroup$ – Malice Vidrine Jul 17 '18 at 17:48

I'll admit I did not look at Awodey's paper, but you might be interested in the (Grothendieck) topoi that arise in first order categorical logic. A good place to read about these is

  • Victor Harnik - Model theory vs. categorical logic: two approaches to pretopos completion (a.k.a. $\mathrm{T}^{\mathrm{eq}}$)

Let me just sketch the main construction, and why it seems to relate to your question. Fix a first order theory $\mathbb{T}$ in some language $\mathcal{L}$, and define $\mathcal{S}(\mathbb{T})$ to be the category with

  • Objects: $[\phi]$, where $\phi$ is a formula in $\mathcal{L}$ in some free variables $x_1,\ldots,x_n$,

  • Morphisms: a morphism $[\phi]\rightarrow[\psi]$, where $\phi$ is a formula in free variables $x_1,\ldots,x_n$ and $\psi$ is a formula in free variables $y_1,\ldots,y_m$, is an equivalence class of formulas $\chi$ in free variables $x_1,\ldots,x_n,y_1,\ldots,y_m$ which $\mathbb{T}$ proves is a map from $\phi$ to $\psi$; explicitly, $\mathbb{T}\vdash (\forall \vec{x},\vec{y}.(\chi(\vec{x},\vec{y})\rightarrow \phi(\vec{x})\wedge \psi(\vec{y}))\wedge(\forall \vec{x}(\phi(\vec{x})\rightarrow \exists ! \vec{y}. \chi(\vec{x},\vec{y}))$. Here, two formulas are equivalent if $\mathbb{T}$ proves that they define the same function.

Here are some features of $\mathcal{S}(\mathbb{T})$:

  • $\mathcal{S}(\mathbb{T})$ has finite limits,

  • Every map $X\rightarrow Z$ factors as $X\xrightarrow{g}Y\xrightarrow{f}Z$ where $g$ is an effective epimorphism and $f$ is a monomorphism. (Here, $Y$ is the image of $g$, which is definable).

  • For every $X\in\mathcal{S}(\mathbb{T})$, the poset $\mathrm{Sub}(X)$ is a distribute lattice; and for every $f\colon X\rightarrow Y$, the pullback map $f^\ast\colon \mathrm{Sub}(Y)\rightarrow\mathrm{Sub}(X)$ is a map of distributive lattices.

These facts are true also of the category of sets (they are the axioms of a coherent category), and the subcategory of $\mathrm{Fun}(\mathcal{S}(\mathbb{T}),\mathrm{Set})$ of functors preserving this structure is equivalent to the category of models of $\mathbb{T}$ and elementary embeddings.

The terminal object of $\mathcal{S}(\mathbb{T})$ is $[\top]$ (no free variables), and a subobject of the terminal object is a sentence $[\phi]$. The logical semantics are quite clear here: in the poset $\mathrm{Sub}([\top])$, we have $[\phi]\vee [\psi] \cong [\phi\vee\psi]$ and $[\phi] \wedge [\psi] \cong [\phi\wedge \psi]$. For example, $[\phi] \cong [\bot]$ precisely when $\mathbb{T}\vdash \neg \phi$.

You might object, because $\mathcal{S}(\mathbb{T})$ is not a topos. However, $\mathcal{S}(\mathbb{T})$ admits a Grothendieck topology generated by the effective epimorphisms. (Concretely, $\{X_i\rightarrow Z\}_{i\in I}$ is a cover when there exists a finite subset $F\subset I$ such that if we factor $X_i\rightarrow Y_i\rightarrow Z$ with $Y_i\rightarrow Z$ monic, then $\bigvee_{i\in F}Y_i \cong Z$). If $\mathcal{C}(\mathbb{T}) = \mathrm{Shv}(\mathcal{S}(\mathbb{T}))$, then:

  • The Yoneda embedding $\mathcal{S}(\mathbb{T})\rightarrow\mathcal{C}(\mathbb{T})$ induces an isomorphism $\mathrm{Sub}([\top])\cong \mathrm{Sub}(1)$,

  • A model of $\mathbb{T}$ is a point of $\mathcal{C}(\mathbb{T})$, i.e. a functor $F\colon \mathcal{C}(\mathbb{T})\rightarrow\mathrm{Set}$ which preserves colimits and finite limits.

So $\mathcal{C}(\mathbb{T})$ retains the logical semantics of $\mathcal{S}(\mathbb{T})$.

| cite | improve this answer | |
  • $\begingroup$ How can $[\top]$ be a terminal object in general? It corresponds to the entire universe, and if $\mathbb T$ is PA, for example, then by your definition there are many different morphisms for any class into $[\top]$ -- at least all of the functions that map everything to a constant numeral. $\endgroup$ – hmakholm left over Monica Jul 17 '18 at 18:07
  • $\begingroup$ If $\phi$ is a formula in $n$ free variables, then you should think of $[\phi]$ as corresponding to the definable subsets $M[\phi] = \{x\in M^{\times n} : M \models \phi(x)\}$ for every model $M$ of $\mathbb{T}$. In particular (if $\mathbb{T}$ is consistent then) $[\top]$ corresponds to the nonempty subsets of $M^{\times 0} = \{\ast\}$. I'll edit my answer to make this more explicit. $\endgroup$ – ne- Jul 17 '18 at 18:13
  • $\begingroup$ x @ne-:: How does that match your definition of morphism? Specifically, with $\mathbb T=PA$, we have that $\chi_1(x,y)\equiv y=0$ and $\chi_2(x,y)\equiv y=x$ both qualify as morphisms $[\top]\to[\top]$ by your definition, and PA does not prove that they define the same function (unless PA is inconsistent). Then you'd have a "terminal object" with two different self-morphisms. $\endgroup$ – hmakholm left over Monica Jul 17 '18 at 18:17
  • $\begingroup$ @HenningMakholm Sorry, by "I'll edit my answer to make this more explicit", I really meant "I'll edit my answer to make it actually correct". Hopefully I was less sloppy this time and it is correct now. $\endgroup$ – ne- Jul 17 '18 at 18:19
  • $\begingroup$ Okay, then. ${}$ $\endgroup$ – hmakholm left over Monica Jul 17 '18 at 18:20

One source of toposes with easily understandable internal logic is to take a complete Heyting algebra $H$ and form a topos in the following way:

  • The objects are pairs $\langle X,\sim\rangle$ where $\sim$ is a function $X\times X\to H$ such that for any $x,y\in X$, $x\sim y=y\sim x$ and $x\sim y\wedge y\sim z\leq x\sim z$ (where "$\wedge$" is the meet operation of $H$). That is, the objects are sets with $H$-valued partial equivalence relations.
  • The morphisms $\langle X,\sim\rangle\to\langle Y,\approx\rangle$ are equivalence classes of functions $F:X\times Y\to H$ such that the following hold:
    • $F(x,y)\wedge x\sim x'\wedge y\approx y'\leq F(x',y')$
    • $F(x,y)\leq x\sim x\wedge y\approx y$ (these first two just make sure $F$ plays nicely with equality)
    • $F(x,y)\wedge F(x,y')\leq y\approx y'$ ($F$ is functional)
    • $x\sim x\leq \bigvee_{y\in Y}F(x,y)$ ($F$ is defined everywhere on its domain)

That this is a topos is proved in Borceux's Handbook of Categorical Algebra, vol 3 (there called $\Omega$-sets), and in a more general form in Ch. 6 of Jacobs's Categorical Logic and Type Theory. As it happens, the topos resulting from the construction above is equivalent to the category of sheaves on $H$; but this construction is neat because it puts the logic first.

Subobjects of $\langle X,\sim\rangle$ correspond to functions $P:X\to H$ such that $P(x)\leq x\sim x$ and $x\sim x'\wedge P(x)\leq P(x')$ (such a $P$ is usually called a "strict predicate"), and the subobject classifier is the object $\langle H,\Leftrightarrow\rangle$ together with the strict predicate $-\Leftrightarrow\top$. In fact, for any $h\in H$, the strict predicate $-\Leftrightarrow h$ is the same as a morphism $1\to\langle H,\Leftrightarrow\rangle$, and for distinct elements of $H$, the associated predicate will be distinct. So the "propositions" of this topos, in the sense referred to in the original post, are essentially just the elements of $H$. Finally, operations on subobjects, and hence on propositions, come from the Heyting operations of $H$.

So the point of that is that if you want a richer propositional structure, you can pick the open sets of any topological space that seems reasonably transparent, and there is a topos that will have those as its lattice of propositions. On the other hand, for any topos $\hom(1,\Omega)$ will have the structure of a Heyting algebra (the proof of this is lengthy and standard, so I omit it), so when it comes merely to propositions in the sense of morphisms $1\to\Omega$, there's not much more to say in general than there is to say about Heyting algebras in general.

It's worth noting, though, that in a topos that is not well-pointed, there may be more to say about $\Omega$ than the Heyting structure of the propositions. For example, in the category of directed multigraphs, the terminal object is the graph with one vertex and one looped edge, so there are only three morphisms $1\to\Omega$. But in this category $\Omega$ actually has two vertices and five edges, which is structure you'd never see only looking at points.

| cite | improve this answer | |

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.