Notifications

Clear all

[Solved] Grothendieck Topology and Inference

Basic questions

Last Post by Joshua Wrigley 3 years ago

6 Posts

3 Users

0 Likes

705 Views

RSS

Lingyuan Ye

(@lingyuan)

Active Member

Joined: 3 years ago

Posts: 8

Topic starter 25/03/2021 12:51 pm

My question comes from the following observation that the axioms of Grothendieck topology are structurally very similar to a general inference relation in logic.

Let $J$ be a family of sieves on a category $\mathcal C$ . We use a slightly different formulation of Grothendieck topology here. We say a sieve $S$ on an object $x$ covers $f : y \to x$ iff $f^* S \in J$ . Then for $J$ to be a Grothendieck topology it must satisfy the following three conditions:

for any $f \in S$ , $S$ covers $f$ ;
if $S$ covers $f$ then for any $g$ with codomain identical to domain of $f$ , $S$ covers $f \circ g$ ;
if $S$ covers $f$ , and $R$ covers any morphisms in $S$ , then $R$ covers $f$ .

It is easy to see such a formulation is identical to the usual conditions for $J$ to be a Grothendieck topology (e.g. see Sheaves in Geometry and Logic, p. 110).

Interesting things emerge if we now change our notation slightly: we use $S \vdash_J f$ to mean $S$ covers $f$ (in $J$ ). Then the above conditions look as follows:

(Reflexivity) $\forall f\in S.S\vdash_J f$ ;
(Weakening) $S \vdash_J f \Rightarrow S \vdash_J f \circ g$ ;
(Transitivity) $S \vdash_J f\ \&\ \forall s\in S. R \vdash_J s \Rightarrow R \vdash_J f$ .

1., 2., 3. are roughly reflexivity rule, weakening rule and transitivity rule of an abstract inference relation in logic, respectively.

If we view the cover relation $(-)\vdash_J(-)$ as a genuine inference relation, it leads to the following several questions:

In this interpretation, not objects but morphisms are treated as "syntactical object". In particular, it is not the same as how we understand the syntactic site of a theory; there the objects are of type $\{\vec x.\phi\}$ , which are formulas equipped with a context, and morphisms are provably functional formulas. Can we understand such a setting here in a logically meaningful way?
Related to the above question, we seem to have a composition operation on these syntactical object, and in the above formulation I suggest this composition should be understood as some kind of "weakening". Is this explanation morally correct, or perhaps a better way to ask is that is there a reasonable reading to make sense of this composition-as-weakening idea?
If we've developed an intuitive understanding of this, how it would influence on our understanding of an arbitrary site?

Sorry if this question seems a bit long and perhaps does not make sense at all, but it's no harm to ask it here to see if anyone have any sparks on this.

ReplyQuote

Topic Tags

Olivia Caramello

(@ocaramello)

Member Admin

Joined: 6 years ago

Posts: 92

26/03/2021 10:48 am

Hi @lingyuan-ye , welcome to the forum!

Concerning the relation between Grothendieck topologies and deductive systems, I suggest you look at these slides, which present some results on this topic from my book "Theories, Sites, Toposes". As you shall see, there is a proof-theoretic equivalence between the classical system of geometric logic over a given geometric theory $\mathbb T$ and a proof system over the geometric syntactic site of $\mathbb T$ whose inference rules correspond to the axioms of Grothendieck topologies; as explained in the slides, there are also variants of this equivalence involving similar proof systems corresponding to different representations of the classifying topos for $\mathbb T$. Note that in these proof systems the role of "syntactic objects" is played by sieves; indeed, (families of) such sieves naturally correspond to geometric sequents over the language of the theory.

ReplyQuote

Lingyuan Ye

(@lingyuan)

Active Member

Joined: 3 years ago

Posts: 8

Topic starter 26/03/2021 4:35 pm

@ocaramello

Thanks very much for your reply Prof. Caramello! The materials you sent are very helpful, and I also plan to start reading more of your book Theories, Sites, Toposes in the months ahead.

ReplyQuote

Joshua Wrigley

(@jwrigley)

Eminent Member

Joined: 3 years ago

Posts: 20

11/04/2021 3:39 pm

@lingyuan

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[\vec{x}/_\sigma \vec{y}]$ ( $\psi[\vec{x}/_\sigma \vec{y}]$ 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[\vec{x}/_\sigma \vec{y}]$ 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[\vec{z}_i/_{\tau'_i} \vec{x}] \,\} \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[\vec{x}'/_\sigma \vec{x}] \,\} \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[\vec{x}'/_\sigma \vec{x}] \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.

ReplyQuote

Lingyuan Ye

(@lingyuan)

Active Member

Joined: 3 years ago

Posts: 8

Topic starter 15/04/2021 4:57 am

@jwrigley

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[\vec x/_\sigma \vec y]$ . 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.

ReplyQuote

Joshua Wrigley

(@jwrigley)

Eminent Member

Joined: 3 years ago

Posts: 20

02/05/2021 11:05 pm

Hi,

I don't have much to add as you're post is very clear. I very much like the "union and covering" description - it points towards the very geometric nature of topos theory. And you're right that we can't yet meaningfully talk about "cotopos theory" since the only topos $\mathcal{E}$ such that $\mathcal{E}^{op}$ is also a topos is the degenerate one, but I fully endorse some contemplation on the deeper insights of this fact.

Other than the above, I update you to say that the presentation I gave in my previous post (which I claimed is valid for any relational language) is in fact a valid site for the classifying topos of any theory. Indeed, nLab gives it as their definition of the syntactic category. I've attached a proof that it is an alternative site for the classifying topos.

ReplyQuote

10 Forum
136 Topics
358 Posts
0 Online
242 Members

Forum Icons: Forum contains no unread posts Forum contains unread posts

Topic Icons: Not Replied Replied Active Hot Sticky Unapproved Solved Private Closed

Around toposes

A blog and forum about toposes, 'bridges' and the unification programme.

Forum

[Solved] Grothendieck Topology and Inference