Hi Joshua,

Thanks very much for your detailed reply! It's very insightful and helpful, and makes me to think about a couple of more points:

1. **The Exact Analogy between Grothendieck Topology and Inference**

From your reply I sort of understand more clearly why we need the information of a Grothendieck topology (in the case of a category) or a covering system (in the case of a poset). Here is the idea: if we start simply from the case of a poset, and as you suggest think it as a weird propositional logic, then the poset already gives us some information about the inference, viz. inference relation between **individuals**. As usually understood by logicians,

a \le b \Leftrightarrow a \vdash b

The same is also true in the general case of a syntactic category. As you've explained, in a relational theory an arrow \sigma : \{\vec x . \varphi \} \to \{\vec y. \psi\} is present iff we have \varphi \vdash_{\vec x} \psi . Vaguely speaking, inference relation between individuals are already given by the information contained in all the arrows of the category.

The precise information a Grothendieck topology gives is how to form inference between a set of individuals and an individual. However, it is kind of the "**dual**" version of the usual inference relation we get in logic. Speaking vaguely, the usual inference relation in logic is axiomatizing "intersection and inclusion relation", but Grothendieck topology is axiomatizing "union and covering". In logic, usually we care about inference of the following form

\Gamma \vdash \varphi

where \Gamma is a set of formulas and \varphi is a single formula. Speaking in model theoretic terms, this shows that such an inference relation requires us to make sense of the **intersection** of all individuals appearing in \Gamma , and the relation \vdash specifies when such an intersection is **included** in another individual. However, a Grothendieck topology is best understood as giving the inference relation of the following kind

\varphi \vdash \Gamma

where we need to make sense of the **union** of individuals in \Gamma , and specify when such a union **covers** another individual (or equivalently when an individual is included in such a union). In a syntactic site this is clear: given a family of arrows \theta_i : \{\vec y_i.\psi_i\} \to \{\vec x.\varphi\} , it is a cover iff

\varphi \vdash_{\vec x}\bigvee_i \exists \vec y_i \psi_i (\vec y_i) \wedge \theta_i(\vec x,\vec y_i)

which of course can be viewed as \varphi is covered by (included in) the union of the direct image of \{\vec y_i.\psi_i\} along the arrow \theta_i . Here the geometric infinite disjunction has replaced the usual logical way of writing

\varphi \vdash_{\vec x} \{\exists \vec y_i. \psi_i(\vec y_i) \wedge \theta_i(\vec x,\vec y_i)\}

where we treat the right hand as a set of individuals and understand it as implicitly taking the disjunction of all of them.

2. **The Axioms of Grothendieck Topology**

In the light of the above discussion, I should actually slightly change my original notation. We should understood as a sieve S covering an arrow f actually as f "implies" S , since inference relation is actually understood as inclusion! Hence, the axioms should now be as follows:

- (Reflexivity) f\in S \Rightarrow S \dashv f ;
- (Strengthening) S \dashv f \Rightarrow S \dashv f \circ g ;
- (Transitivity) S \dashv f \ \&\ \forall s\in S. R \dashv s \Rightarrow R \dashv f .

The only thing that changes conceptually as the original statement is the status of stability axiom. I originally say it is like weakening, but that's because I do not realize that Grothendieck topology is not axiomatizing inference relation (inclusion) but axiomatizing "coinference", which is covering. There the status of axiom 2 is clear, because the direct image of f \circ g is always contained in the direct image of f , hence it is a form of strengthening the axioms to make a smaller subobject. This intuitive understanding is compatible with your understanding of *generalized substitution*, by observing the usual adjunction between substitution (pullback) and direct image. These axioms of course should be understood as the structural axioms of the coinference relation.

3. **Philosophical Remarks**

It is not clear to me before your reply that there is a difference between inference relation between individuals and inference between a bunch of individuals and an individual, since in logic they always come side by side (usually logic consider inference relation between individuals as special cases of the more general inference relation). This solves a long standing puzzle of mine: when thinking the smaller than relation in a lattice as inference relation, we only get inference between individuals. In logic, we almost always take the canonical Grothendieck topology, using supremum in the lattice, to form the general inference relation between a collection of individuals and a single individual. However, in a general lattice that does not possessing enough meets or joins, this cannot be done, which is very frustrating because we already have an inference between individuals. But now I realize we can define a general inference using Grothendieck topology! (Thanks for your suggestion of looking at the exercise in *Sheaves in Geometry and Logic*!)

Furthermore, it seems to me that the comparison between Grothendieck topology and inference relation above also suggest another "completely dual theory" of topos theory (might call it cotopos theory). (This idea might not make sense at all due to my limited understanding of topos theory, but let me state it here anyway.) As generally understood, (first-order) logic is how we axiomatize and reason about subobjects, which corresponds to monomorphisms in a category. As we understood above, a Grothendieck topology is exactly how we axiomatize the operation of taking union and the covering relation (coinference), which is somehow what we lack in considering subobjects. However, is it possible for us to image the notion of a "cologic", which from scratch axiomatizes and reasons what an object covers (epimorphisms with domain being this object), and a coGrothendieck topology shows how we perform general intersections and how we axiomatize inclusion?

What we may expect from this cotopos theory is that it should replace the role played by subobjects by using (equivalence classes of) epimorphisms, pullbacks by pushouts, ... Theorems perhaps should include that every coslice category of a cotopos is again a cotopos, etc., etc.

I believe there must already be some mathematicians thinking along the same line. I have seen someone asking about why we take the free cocompletion but only free *finite* completion when forming a free topos; I think I have also seen discussions about the asymmetry of topos theory (the dual of a category is again a category, but the dual of a topos is very far from being a topos). I think knowing whether or not this idea works can advance our philosophical understanding of mathematics in general. Either it works and somehow we find perfect symmetry in mathematics, or it does not work but we understand the reason why it not works and this might greatly deepening our understanding of the difference between the two.

I am pleased to announce the following paper, written in collaboration with Axel Osmond (@axel-osmond):

This work introduces a new topos-theoretic construction, that of the over-topos at a model of a geometric theory in a Grothendieck topos, and investigates both its logical and geometric aspects. Here is the abstract:

*With a model of a geometric theory in an arbitrary topos, we associate a site obtained by endowing a category of generalized elements of the model with a Grothendieck topology, which we call the antecedent topology. Then we show that the associated sheaf topos, which we call the over-topos at the given model, admits a canonical totally connected morphism to the given base topos and satisfies a universal property generalizing that of the colocalization of a topos at a point. We first treat the case of the base topos of sets, where global elements are sufficient to describe our site of definition; in this context, we also introduce a geometric theory classified by the over-topos, whose models can be identified with the model homomorphisms towards the (internalizations of the) model. Then we formulate and prove the general statement over an arbitrary topos, which involves the stack of generalized elements of the model. Lastly, we investigate the geometric and 2-categorical aspects of the over-topos construction, exhibiting it as a bilimit in the bicategory of Grothendieck toposes.*

The construction of the over-topos can also be dualized, providing a wide generalization of Grothendieck-Verdier's notion of localization of a topos at a point.

This paper combines a variety fo techniques and touches several distinct themes, introducing new ideas or constructions in connection with each of them :

- Syntactic categories and classifying toposes
- Totally connected toposes and colocalizations
- Grothendieck topologies on fibrations
- Computation of Grothendieck topologies generated by different families of sieves
- Geometric morphisms and stacks associated with them
- Giraud's construction of the classifying topos of a stack
- 2-categorical constructions in the bicategory of Grothendieck toposes

In my forthcoming joint work with Riccardo Zanfa (@rzanfa) we shall introduce a whole new framework for developing relative topos theroy via stacks, thereby providing a broad context where the results of this paper can be understood. Stay tuned! ;-)

]]>Hi Lingyuan,

Thank you for the interesting question! I've been thinking about this insight for a while now, and I think I'm now in a position to give the beginnings of an answer.

**1. How does a Grothendieck topology behave like an inference relation on the syntactic category?**

I would argue that a Grothendieck topology is best understood as an inference relation when S covers f is replaced with \{\,\text{dom}(f) \mid f \in S \,\} covers \text{codom}(f) along the arrows of S. If we restrict to the syntactic category of a relational language (i.e. the signature has no function symbols) the provably functional formulae correspond to provability via a relabelling of variables, that is an arrow \{\,\vec{x}.\varphi\,\} \to \{\,\vec{y}.\psi\,\} is a function \sigma \colon \vec{y} \to \vec{x} that respects types and \varphi \vdash_{\vec{x}} \psi ( \psi denotes replacing each occurrence of the variable y_j \in \vec{y} in \psi with \sigma(y_j)). The Grothendieck topology for the syntactic category then becomes S \in J(\{\,\vec{x}.\varphi\,\}) \iff \varphi \vdash_{\vec{x}} \bigvee_{\sigma \in S} \exists \vec{y} \ \psi \land \sigma(\vec{y}) = \vec{x}. This can be understood with an abuse of formalism as "the set of things satisfying \varphi is the union of things satisfying \psi (under some relabelling of variables)" - this is precisely the description of what a covering family in the syntactic category entails in a set-based model.

This can be seen even more clearly when we restrict to sentences \{\,\emptyset.\varphi\,\}, since then there is at most one arrow between any two sentences given by syntactic implication \{\,\emptyset.\varphi\,\} \xrightarrow{\varphi \vdash_{\emptyset} \psi} \{\,\emptyset.\psi\,\}, and the sieve \langle \Gamma \rangle generated by a collection of such arrows \Gamma is covering if and only if \varphi \vdash_{\emptyset} \bigvee_{\psi \in \Gamma} \psi . Compare this to the covering system given to a Lindenbaum algebra of a propositional theory (where all the formulae are sentences) and one can appreciate how the Grothendieck topology is the first order analogue of a propositional phenomenon.

**2. What are the axioms of a Grothendieck topology under such an interpretation?**

a. Reflexivity becomes \varphi \vdash_{\vec{x}} \varphi (the identity is given by the trivial relabelling of variables).

b. Transitivity becomes transitivity of inference: if \varphi \vdash_{\vec{x}} \bigvee \exists \vec{y}_\gamma \ \psi_\gamma \land \vec{x} = \sigma_\gamma (\vec{y}) and \psi_\gamma \vdash_{\vec{y}} \bigvee \exists \vec{z}_{i_\gamma} \ \chi \land \vec{y} = \tau_{i_\gamma}(\vec{z}_{i_\gamma}) for each \gamma, then \varphi \vdash_{\vec{x}} \bigvee \exists \vec{z}_{i_\gamma} \ \chi \land \vec{x}=\sigma_\gamma \circ \tau_{i_\gamma}( \vec{z}_{i_\gamma}).

c. Stability, as you observed, is a little more complicated: if \varphi \vdash_{\vec{x}} \psi and \psi \vdash_{\vec{y}} \bigvee_{i \in I} \exists \vec{z}_i \ \chi_i \land \vec{y} ={\tau_i}( \vec{z}_i), then \varphi \vdash_{\vec{x}} \bigvee_{i \in J} \exists \vec{z}_i \ \chi_i \land \vec{x} ={\tau'_i} (\vec{z}_i) where J is the subset \{\, i \in I \mid \vec{y} \xrightarrow{\tau_i} \vec{z}_i \text{ factors as } \vec{y} \xrightarrow{\sigma} \vec{x} \xrightarrow{\tau'_i} \vec{z} \text{ and } \chi_i \vdash_{\vec{z}_i} \varphi \,\} \subseteq I.

This description of stability isn't particularly satisfying yet. I will make a restriction that will hopefully illustrate why I think stability should be thought of as *generalised substitution*. Consider a relabelling \sigma \colon \vec{x} \to \vec{x}', which yields an arrow \{\vec{x}'.\varphi \,\} \to \{\,\vec{x}.\varphi\,\}. Stability, in this case, becomes: if \varphi \vdash_{\vec{x}} \bigvee \exists \vec{y} \ \psi \land \vec{x} =\tau (\vec{y}) then \varphi \vdash_{\vec{x'}} \bigvee \exists \vec{y} \ \psi \land \vec{x}' = \sigma \circ \tau(\vec{y}).

**3. Extra remarks**

So far I've discussed only a relational language. Obviously every language can be turned into a relational language in such a way that the semantics remain the same (replace \varphi(\vec{x},f(\vec{y})) by \varphi(\vec{x},\vec{z}) \land R(\vec{z},\vec{y}) where we define R(\vec{z},\vec{y}) \iff f(\vec{y})=\vec{z}). This was to make the idea of covering along arrows simpler to appreciate, but the intuition carries over to covering along provably functional formulae.

In Johnstone's Elephant Section D Proposition 3.1.7 an alternative characerisation of the syntactic topology is given: it is the smallest Grothendieck topology such that the sequents of the theory \varphi \vdash_{\vec{x}} \psi give covering arrows. This is nicer for what follows next as no reference is given to specifically geometric logical connectives (like existential quantification and infinitary disjunction) unlike in the previous characterisation.

**4. Some vague philosophical stuff...**

What benefit can we gain from this understanding of the Grothendieck topology? I'm going to draw an anology between Lindenbaum algebras and the syntactic site.

Every poset can be considered as the Lindenbaum algebra of some theory in some weird propositional logic, and similarly every suitably algebraizable propositional logic has a poset as its Lindenbaum algebra. We can take the *free join completion* - which is {\bf 2}^{P^{op}} \cong \text{Idl}(P), that is the monotone maps from the order dual into {\bf 2} and the ideals or down sets of the poset - which one can think of as adding all joins in free way, ignoring the extra information of the logic. This lost information can be added as a syntactic covering system J (see Exercise 5, Chapter IX Localic Topoi, Sheaves in Geometry and Logic) which is a particular example of a Grothendieck topology. The frame J\text{-Idl}(P) of *J*-ideals (that is those down-sets where S \in J(x), \, S \subseteq I \implies x \in I) then classifies models (i.e. valuations) of the theory in an arbitrary frame of truth-values L in the sense that these are simply frame homomorphisms J{\text{-Idl}}(P) \to L .

The above suggests we should think of categories as the first-order Lindenbaum algebras. The *free co-completion* is given by the pre-sheaf topos {\bf Sets}^{\mathcal{C}^{op}} and we add the extra information needed using the syntactic topology (using Johnstone's description whenever we lack the necessary syntax). The axioms for being a Grothendieck topology become requirements on the syntactic inference schema of the original logic. The topos {\bf Sh}(\mathcal{C},J) then classifies the models of the geometric logic generated by our original logic.

In some vague sense, this gives us a universal grasp of the semantics of the original logic with the syntax of our choice, namely geometric first order logic.

]]>I'm M djo k'naan, and I recently started to study category theory and topos as a autodidact.

I'm interested in their applications in the logic field.

]]>

Sorry for taking a while to see your reply. I've just been reading Z. Janelidze and A. Goswami's self-dual axiomatization, and I'm a little confused about the claims you made in the post above. They seem to have the goal of extracting the strongest categorical axioms A of the category of groups C such that both A and the dual of A hold once we equip C with the data of subobjects .

Certainly when it comes to toposes there aren't many self-dual axioms which apply; there are some finitary completeness/cocompleteness axioms, but the way in which limits and colimits interact is not self-dual. There is no quotient classifier (in the sense of a direct dual to the subobject classifier), either. So I'm curious how your self-dual subobject/quotient classifier works. Similarly, the "subobject functor" and "quotient functor" have various choices available regarding what they do to morphisms. Which do you choose, and what does taking the pullback of these achieve, exactly?

]]>Yes, i'm trying to figure out how that structure work, I still have issues with that so I can sound a bit unclear; your example work.

I'm going to have a look about what you said on the geometric morphisms, because that's what I was looking for.

Hopefully a topoi will suffice.

Thanks a lot for the help

]]>That being said, I'm very happy to accept that my proposed model for fuzzy set theory is not perfect.

As for your other question about whether there are more general structures than a topos: there's always something more general, although I'm not knowledgeable enough to suggest any with confidence. However, it seems topoi still suffice for your purposes: it is not the case, in an arbitrary Grothendieck topos \mathcal{E}, that two objects E,\, F are isomorphic if the Hom-sets {\rm Hom}_{\mathcal{E}}(1_{\mathcal{E}}, E) \cong {\rm Hom}_{\mathcal{E}}(1_{\mathcal{E}},F) are bijective, unlike in {\bf Sets}. This can clearly be seen even in presheaf topoi.

Let {\bf 2} be the category \bullet_0 \to \bullet_1 . The terminal object 1_{\bf Sets^2}\in {\bf Sets}^{\bf 2} is given by 1_{\bf Sets^2}(\bullet_0) = 1_{\bf Sets^2}(\bullet_1) = \{\ast\}; the initial object 0_{\bf Sets^2}\in {\bf Sets}^{\bf 2} is given by 0_{\bf Sets^2}(\bullet_0) = 0_{\bf Sets^2}(\bullet_1) = \emptyset. Now consider the functor P \colon {\bf 2} \to {\bf Sets} given by P(\bullet_0) = \emptyset, \, P(\bullet_1) = \{\ast\}. There's no arrow \{\ast\} = 1_{\bf Sets^2}(\bullet_0) \to P(\bullet_0) = \emptyset and so \emptyset = {\rm Hom}_{\bf Sets^2}(1_{\bf Sets^2},P) \cong {\rm Hom}_{\bf Sets^2}(1_{\bf Sets^2},0_{\bf Sets^2}) but also P \not \cong 0_{\bf Sets^2}.

In general, in an arbitrary topos, it is not sufficient to consider global elements (i.e. arrows 1_{\mathcal{E}} \to F) but generalised elements E \to F.

]]>

you take as the objects the natural number, you have a \in n iff a = p^\beta, \beta \geq 1 and a | n where p is a prime number, same thing here a map is \delta \colon n \to k with \delta \colon \{a \in n\} \to \{b \in k\}

]]>That is very interesting, as far as I'm learning topos theory i'm eventually going to come across those morita equivalences.

Actually I don't think there are some semantic equivalence between fuzzy set theory and the set theory, now if you can move from a classifying topos to another (I think that what you call an interpretation) this is exactly what i want.

Well for that i'll construct the fuzzy set category, I think this is a natural way to see it:

So you have f \colon E \to as a fuzzy set, what would be closest to a singleton in the fuzzy set theory is those type of functions,x_\alpha \colon E \to where x \in E, \alpha \in ]0,1] with x_\alpha(y) = \alpha iff y =x 0 otherwise.

In that case we say x_\alpha \in f if f(x) \neq 0 and \alpha = f(x).

So now the map are \delta \colon f \to g with \delta \colon \{x_\alpha \in f\} \to \{y_\beta \in g\}

This way you have a category with all your small limits (even exponentials) however when trying to get the natural isomorphism

\theta_f \colon -> Sub(f \times g) you'll have some issues. I don't even know that way if you get a topos.

That is why I asked if there are more general structure than topos, cause you might want to go from classical logics to more exotic one, and thats why I said that I have issues with the truth map being from the terminal to the subobject clasifyer because in more exotic logics you have also non terminal objects behaving like singleton object. In that case: f = g \iff (\forall x_\alpha, x_\alpha \in f \iff x_\alpha \in g)

I'm going to have a look on the geometric morphisms.

That's very helpful.