The n-Category Café

The quote probably makes more sense in context. Steve Vickers was replying to Vaughan Pratt, who had written:

I have had little luck absorbing the logic of Heyting algebras into my own mathematical thinking. I furthermore worry that if ever I were to succeed my insights might become even less penetrating than they already are.

My feeling about these recommended Brouwerian modes of thoughts is that they are something like locker room accounts of social and other conquests: great stories about things that never actually happened, but which with sufficient repetition convince one that they must surely have occurred.

[…]

The self-evident is merely an hypothesis that is so convenient, and that has been assumed for so long, that we can no longer imagine it false. This is just as true for Excluded Middle itself as for its negation. I happen to find Excluded Middle more convenient than its negation, but that’s just me and perhaps others have had the opposite experience.

Vickers replied:

Dear Vaughan,

Let me tell you how it really did occur for me - and I am happy to proclaim this as true love, not locker-room boasting.

As you know from my book, at the end of the 80s I had learned from Abramsky and Smyth, not to mention the topos-theorists, that frames and topological spaces could be used to represent observational theories (technically, propositional geometric theories). But all my thinking was classical, even though I knew that frames could embody non-classical logic. I assumed that one manipulated the frames within a classical world.

I was investigating how one might understand predicate geometric logic in a similar observational way, and this led me to my bagtopos construction in “Geometric Theories and Databases”. But even there, I was thinking of formal logical manipulations in a classical world. In particular, I was thinking of geometric morphisms as being defined by formal translations of symbols to geometric formulae, similar to the way I treated locale maps in my book.

It was Peter Johnstone who showed me a different way, with his paper “Partial products, bagdomains and hyperlocal toposes”. He generalized my bagtoposes and described a universal property of them. He also showed that his more general construction was, in the contexts where mine was defined, equivalent to it. This equivalence involved describing geometric morphisms between different classifying toposes, and at that point I was expecting to see formal logical transformations. But when I eventually understood his proof I saw that he was doing something different and much more natural: he used the internal mathematics of the toposes to show how models of the geometric theories transform. This only works if the reasoning is geometric, and from then on I have grown to love the geometric reasoning better as a route to better understanding of toposes (and locales too, for that matter). This is what I tried to explain in “Locales and Toposes as Spaces”, my chapter in the Handbook of Spatial Logics.

As a parable, I think of toposes as gorillas (rather that elephants). At first they look very fierce and hostile, and the locker-room boasting is all tales of how you overpower the creature and take it back to a zoo to live in a cage — if it’s lucky enough not to have been shot first. When it dies you stuff it, mount it in a threatening pose with its teeth bared and display it in a museum to frighten the children. But get to know them in the wild, and gain their trust, then you begin to appreciate their gentleness and can play with them.

The gorilla in the cage is the topos in the classical world.

Best regards,

Steve.

Here’s something that tickled me. A sign outside a monastery in Meteora, Greece, says

“O topos einai ieros”

(“The topos is holy”)

Vickers explains his attitude in a more elementary way on his webpage.