Geometric Logic

Clear all

# Geometric Logic

(@morgan-rogers)
Eminent Member
Joined: 9 months ago
Posts: 24
Topic starter

I'd like to kick off the discussion on L. Lafforgue's course on Classifying toposes of geometric theories.

If you haven't met geometric theories before, it can be helpful to see a lot of examples. Prof Lafforgue explained how to express the theories of groups and equivalence relations as geometric theories. What's your favourite kind of mathematical object? Can you work out how to express the axioms of those objects as a geometric theory?

[Beware: it's not always possible, and sometimes the axioms may need to be judiciously presented to produce a geometric theory!]

(@morgan-rogers)
Eminent Member
Joined: 9 months ago
Posts: 24
Topic starter

Personally, I like the theory of categories, since it is intuitively expressible as a two-sorted theory, but the most straightforward way to present composition is as a ternary (3-ary) relation, identifying triples of the form $(f,g,g \circ f)$ where composition is defined, equipped with axioms guaranteeing that the composite of two morphisms is unique.

This also opens the door to further questions: how can natural transformations be incorporated? (don't forget that the category of models of a geometric theory in a topos is a 1-category)

(@matthias-hutzler)
Active Member
Joined: 1 month ago
Posts: 5

One of my favorite geometric theories to play around with is the "theory of a surjection": take two sorts $A$ and $B$, a unary function symbol $f : A \to B$ and a single axiom: $\top \vdash_{y : B} \exists x : A. (f(x) = y)$.

It is Morita-equivalent but not biinterpretable (or syntactically equivalent as Lafforgue called it I think) to the "theory of an equivalence relation" with only one sort $A$, a binary relation symbol ${\sim} \subseteq A \times A$ and appropriate axioms.

(@morgan-rogers)
Eminent Member
Joined: 9 months ago
Posts: 24
Topic starter

@matthias-hutzler that's very interesting indeed! How does one demonstrate that Morita equivalence?

(@matthias-hutzler)
Active Member
Joined: 1 month ago
Posts: 5

Well, I the intuition is that in any (Grothendieck) topos $\mathcal{E}$, you can divide out an equivalence relation ${\sim} \subseteq A \times A$ to get an epimorphism $f : A \twoheadrightarrow B$ and you can also get back $\sim$ from $f$. This gives a category equivalence $\mathbb{T}_1{-}\mathrm{mod}(\mathcal{E}) \simeq \mathbb{T}_2{-}\mathrm{mod}(\mathcal{E})$ for every topos $\mathcal{E}$.

However, to get a full proof without worrying about naturality conditions, I think it might be easier to look at the "union" of $\mathbb{T}_1$ and $\mathbb{T}_2$ plus the extra axiom(s) $x \sim y \dashv\vdash_{x, y : A} f(x) = f(y)$. We might call this theory $\mathbb{T}_3$ the "theory of an equivalence relation with specified quotient". Then $\mathbb{T}_3$ is an extension both of $\mathbb{T}_1$ and of $\mathbb{T}_2$ and what we want to show is that in both ways, it is an equivalence extension (i.e. the induced geometric morphisms between classifying toposes are equivalences). For this it suffices to check that for every model of the base theory ($\mathbb{T}_1$ or $\mathbb{T}_2$) in a topos $\mathcal{E}$, there is exactly one "model extension" to a model of the extended theory ($\mathbb{T}_3$) up to isomorphism!

(@steve-vickers)
Active Member
Joined: 1 month ago
Posts: 9

It's useful to remember that the geometric techniques allow you to define maps (geometric morphisms), not just equivalences.

For each model of T_1 (surjective function) you can define a model of T_2 (equivalence relation), and the construction is geometric (colimits, finite limits). Applying this to the generic model in S[T_1] gives a model of T_2, hence (by the universal property of classifying toposes) a map [T_1] -> [T_2]. (I'm distinguishing the generalized space from the topos of sheaves by dropping S.)

Similarly we get a map [T_2] -> [T_1], take coequalizer of equivalence relation.

To show that these maps give an equivalence, we show the appropriate isomorphisms.

The gloss about generic objects here is not necessary in practice. You just go for an ordinary mathematical proof of the equivalence, but make sure it is all geometric.

Steve Vickers

(@ocaramello)
Joined: 4 years ago
Posts: 44

Posted by: @steve-vickers

It's useful to remember that the geometric techniques allow you to define maps (geometric morphisms), not just equivalences.

This is explained in detail in section 2.1.3 ("Interpretations and geometric morphisms") of my book "Theories, Sites, Toposes".

(@steve-vickers)
Active Member
Joined: 1 month ago
Posts: 9

Also in various papers of my own (all on my website) dating back to 1990 in [1] “Topical categories of domains”. [2] “Locales and toposes as spaces” describes it in the form of a reader’s guide to the “generalized space” understanding of Mac Lane and Moerdijk.

A key adjunct to the usefulness of geometric theories is to incorporate geometric constructions (colimits, finite limits) as sort constructors.

This doesn’t essentially change the descriptive power of geometric theories, but is very convenient in practice - see both [1] (which uses the Kuratowski finite powerset as geometric construction) and [2], where it was illustrated informally. My papers on arithmetic universes formalize the idea in the case where the colimits are free algebra constructions, which covers a wide range of cases without depending on set theory to say what infinitary coproducts are.

Steve

(@steve-vickers)
Active Member
Joined: 1 month ago
Posts: 9

Correction - “Topical categories of domains” was 1999 - Steve.

(@ocaramello)
Joined: 4 years ago
Posts: 44

@steve-vickers Indeed, your references emphasize the use of geometric constructions, while section 2.1.3 of my book provides a more formal logical treatment in terms of generalized forms of interpretations of geometric theories and internal models.

(@matthias-hutzler)
Active Member
Joined: 1 month ago
Posts: 5

tl;dr Is there a general theorem about geometric constructions or is it more of a slogan?

I think the reason I always felt a little bit uncomfortable about geometric constructions is simply that I had never seen an actual precise definition of this term. Sure, it means adding small colimits and/or finite limits; but adding colimits/limits of what (which objects and arrows are allowed), to what exactly, and what exactly is the statement that then follows automatically? To illustrate my point, here is a baby attempt at such a precise statement (assuming, as in my post above, that extensions of geometric theories (called "expansions" in Olivia's book) are a nice way to present geometric morphisms):

Baby Attempt. Let T be a geometric theory, let I be a small category, let A_i be one of the sorts of T for every i in I, let $f_{i \to j} : A_i \to A_j$ be a unary function symbol for every arrow $i \to j$ in I. Then the following extension of T is an equivalence extension: Add one sort (colim A_i), unary function symbols $\iota_j : (\mathrm{colim} A_i) \to A_j$ and certain axioms expressing that this is a colimit cocone. (And similarly for finite limits.)

I think we can agree that this is true but not very useful. Surely we want to be able to use the non-binary function symbols of T, and also maps given by relation symbols (such as the two projections of an equivalence relation). But also compositions of such maps? And maybe maps not directly corresponding to a symbol of the language, but given by a geometric formula (defining the graph of the map)? -- This feels more and more like we want to say: "First perform an arbitrary equivalence extension of the theory T and then do something as in the Baby Attempt." But this is no longer a stand-alone tool for proving the Morita equivalence of two theories.

(@steve-vickers)
Active Member
Joined: 1 month ago
Posts: 9

Interestingly, that’s pretty much the way I defined general maps in “Sketches for arithmetic universes”. If T and T’ are two theories (there they are in sketch form for the AU logic, but you might as well think of them as geometric, and “AUs and classifying toposes” explains the connection), then a map [T] -> [T’] is defined as a *theory homomorphism* from T’ to some equivalence extension T’’ of T. A theory homomorphism is purely syntactic - sorts to sorts, symbols to symbols, axioms to axioms; and equivalence extension is also defined in a syntactic way.

Defining the theory extension in the pure logic of geometric theories (eg colimit as new sort, colimit cocone maps and suitable axioms) would be laborious. However, we know that colimits are geometric, so we might as well add an ability to introduce them as derived sorts. That’s what the sketches do in my AU formalism, and of course it’s what you do in natural reasoning.

Steve.

(@ocaramello)
Joined: 4 years ago
Posts: 44

@matthias-hutzler Concerning (geometric) logical characterizations of geometric constructions, I suggest to check out this paper.

(@matthias-hutzler)
Active Member
Joined: 1 month ago
Posts: 5

Posted by: @ocaramello

check out this paper

Thanks, I didn't know this -- I was actually wondering whether such a result exists in the literature!

Share: