[FOM] R: R: Preprint: "The unification of Mathematics via Topos Theory"

[Olivia Caramello]

Dear Vaughan,

Thanks for your further comments on my paper; please find my answers below.

> -----Messaggio originale-----
> Da: fom-bounces at cs.nyu.edu [mailto:fom-bounces at cs.nyu.edu] Per conto di
> Vaughan Pratt
> Inviato: venerdì 16 luglio 2010 7.30
> A: Foundations of Mathematics
> Oggetto: Re: [FOM] R: Preprint: "The unification of Mathematics via
> Topos Theory"
> 
> In my initial response to Olivia Caramello's post I only brought up one
> point, about the need for a more representative example of Morita
> equivalence.  I was embarrassed that this was so minor a point, so I
> thought I should try to engage better with the paper.  Here are some
> more points, hopefully none as minor as the first.
> 
> On 7/10/2010 3:55 PM, Olivia Caramello wrote:
> > So whatever happens at the
> > level of toposes has 'uniform' ramifications into Mathematics as a
> whole;
> > for example, the fact that the subtoposes of a given topos form a
> lattice L
> > implies that for any theory classified by that topos (and notice that
> there
> > are in general many different such theories), the quotients of that
> theory
> > (considered up to syntactic equivalence) form a lattice which is
> isomorphic
> > to L (cfr. section 8 of my paper).
> 
> This seems like a nice point.  Let me attempt to translate it into
> algebra, noting that theories vary according to whether any given sort
> definable as the sort of fixpoints of an idempotent (such as the
> operation of taking one endpoint of a graph) is given as an explicit
> sort or is left implicit on the assumption that it could be
> reconstructed if necessary.
> 
> The claim here seems to be that, given any selection of choices as to
> whether to make such a sort explicit or implicit, when all the
> quotients
> of the resulting theory are formed, the same choices are made in the
> quotient as in the original.  The identifications implied by the
> quotients may make some of those choices vacuous by collapsing the
> choices together, but the distinctions drawn between the subtoposes of
> T
> will remain distinctions between the corresponding quotients of this
> choice of theory classified by T.
> 
> At least for concrete toposes T, understood as presheaf categories, is
> this a fair statement?
> 
> Presumably this result should be straightforward in the case of
> concrete
> toposes, and that the nontrivial contribution here lies in extending it
> to abstract toposes.

The 'duality theorem' is intuitively clear for cartesian (in particular,
finitary algebraic) theories, but already non-straightforward for the more
general class of theories of presheaf type (i.e. theories classified by a
presheaf topos), since it is not a priori clear that every finitely
presentable model of such a theory should be finitely presented (this is a
theorem that I proved in my paper "One topos, many sites",
http://front.math.ucdavis.edu/0907.2361). 

> This would be a sort of counterpart to the
> theorem
> for Boolean algebras, that every Boolean algebra is isomorphic to a
> subalgebra of a powerset algebra, which is true by definition for
> concrete Boolean algebras but requires (nearly) the axiom of choice for
> the abstract case, a point of interest for Foundations of Mathematics.
> 
> Any such complications in passing from concrete to abstract toposes for
> your result would presumably be of similar foundational interest,
> particularly for those who view toposes as foundationally important in
> the way Boolean algebras are (if not for the same reasons).  Are there
> such complications, and how delicate are they?

The proof of the general case goes through the geometric syntactic site of
definition of the classifying topos of the theory; specifically, the
subtoposes of the classifying topos correspond bijectively with the
Grothendieck topologies J on the syntactic category of the theory which
contain the syntactic topology, and these topologies J are in turn seen to
correspond bijectively with the syntactic-equivalence classes of quotients
of the theory. One essential point here is that, since every geometric
category is well-powered (i.e. it has only a *set* of subobjects of a given
object), one can convert every J-covering sieve into an infinitary axiom for
a quotient of the theory.  

>  > It is also worth to note that the
> > transfer of knowledge between two theories which are Morita-
> equivalent to
> > each other is not carried out - as it normally happens - by using the
> > explicit description of the equivalence, but rather by going through
> the
> > classifying topos, which acts as a 'bridge' connecting the two
> theories and
> > enabling us to transfer invariants across them (in fact, for
> transferring
> > 'global' invariants of toposes one can well ignore the actual
> description of
> > the equivalence).
> 
> Does this mean that the crutch of idempotents is unavailable in the
> abstract case?  And if so, is there at least a "ghost of departed
> idempotents" to support intuition, or is intuition out the window in
> this case?

The splitting of idempotents has a natural behavior with respect to
Grothendieck topologies; indeed, a Grothendieck topology J on a small
category C naturally corresponds to a Grothendieck topology J' on the Cauchy
completion C' of C such that the two toposes Sh(C,J) and Sh(C',J') are
equivalent (see my paper "Yoneda representations of flat functors and
classifying toposes" http://front.math.ucdavis.edu/0805.2187 for more
details). Of course, the syntactic category of a geometric theory always has
equalizers and hence is Cauchy-complete, so one can avoid caring about the
splitting of idempotents when dealing with syntactic sites.

Anyway, the point here is that any 'global' invariant of toposes (by this I
mean any property of toposes which is invariant under categorical
equivalence, such as the property of a topos to be Boolean, De Morgan,
atomic, connected etc.) is, by definition, invariant with respect to *any*
categorical equivalence of toposes and hence one does not need to know the
explicit description of the equivalence to apply the machinery described in
the paper. Note that this is an approach to transferring information between
Morita-equivalent theories which is radically different from the 'classical'
one; the inspiration for it comes from the observation (cfr. page 15 of my
paper) that 

"...a given mathematical property can manifest itself in several different
forms in the context of mathematical theories which have a common
‘semantical core’ but a different linguistic presentation; the remarkable
fact is that if the property is formulated as a topos-theoretic invariant on
some topos then the expression of it in terms of the different theories
classified by the topos is determined to a great extent by the technical
relationship between the topos and the different sites of definition for it
(cfr. section 6)."

> > I realize that this might sound unbelievable, but this machinery has
> really
> > the potential to 'automatically generate' results (a careful reading
> the
> > paper is necessary to fully understand the precise meaning of this
> claim);
> > on the other hand, the sensitivity and experience of an educated
> > mathematician are necessary in order to 'program the machine' to
> yield
> > results of current mathematical interest.
> 
> Was there anything in your paper concerning algorithms or decision
> methods for generating results?  Without a clear statement of the
> problem and some sort of computational complexity bound on it, it is
> difficult to evaluate claims of potential to generate results
> automatically, which would lend support to your concern about
> believability.

In the paper, I limited myself to suggesting the abstract possibility of
'automatizing' the method 'toposes as bridges', without going into the
details of a possible concrete implementation:

"We emphasize that there is an strong element of automatism in the
techniques just explained; by means of these methods, one can generate new
mathematical results without really making any conscious effort: indeed, in
most cases one can just readily apply the well-known general
characterizations connecting properties of sites and topos-theoretic
invariants (such as for example the above-mentioned ones for the property of
Boolean and two-valuedness) to the particular case of interest. On the other
hand, the range of applicability of these methods is boundless within
Mathematics, by the very generality of the notion of topos."

Let me try to explain this in more detail. Starting with two
Morita-equivalent theories in the form of two different sites of definitions
(C,J) and (C',J') for a given topos (i.e. starting with an equivalence
between the toposes Sh(C,J) and Sh(C',J')), we can try to transfer
invariants between the two sites by using the topos Sh(C,J) (which is
equivalent to Sh(C',J')) as a 'bridge'. For many invariants, including those
which express logical properties of the internal Heyting algebra given by
the subobject classifier of the topos (think for example of the property of
a topos to be Boolean or De Morgan), one has bijective characterizations of
the kind "Sh(C, J) satisfies the invariant if and only if the site (C, J)
satisfies a certain 'tractable' categorical property P", holding 'uniformly'
for any site (C,J). This allows a direct, 'automatic', transfer of
information between two different sites of definition (C,J) and (C',J') of a
given topos; indeed, one gets an equivalence between the property P of the
site (C,J) and the property P of the site (C',J'). So the 'machine' takes as
input a Morita-equivalence (in terms of a pair of different sites of
definition of a given topos) and a topos-theoretic invariant and generates
equivalences between properties of the two different sites. For example,
imagine having an 'algebra-geometry' Morita-equivalence leading to two sites
of definition of the same topos, one of 'algebraic nature' and the other one
of 'geometric nature'; this technique produces, for any invariant of the
above-mentioned kind, an equivalence between an 'algebraic' property and a
'geometrical' one. For other kinds of invariants, for which one does not
have uniform bijective characterizations as above, the same game can be
played, but some ad hoc (i.e. non-automatic) arguments might be necessary
(cfr. my paper for some examples of arguments of this latter kind).
  
The results generated in this way are *not* necessarily trivial; in some
cases they can be rather 'weird' according to the usual mathematical
standards (although they might still be quite deep) but, with a careful
choice of Morita-equivalences and invariants, one can easily get interesting
and non-trivial results, as shown in the paper. Also, a lot of information
that is not visible with the usual 'glasses' is revealed by the application
of this machinery (the paper contains various instances of this phenomenon).
 
It is worth to note that, compared with the classical methods, this
technique is fairly non-standard; these methodologies define a new way of
doing Mathematics which is 'upside-down' compared with the 'usual' one.
Instead of starting with simple ingredients and combining them to build more
complicated structures, one assumes as primitive ingredients rich and
sophisticated mathematical entities, namely Morita-equivalences and
topos-theoretic invariants (note however that the fact that these
mathematical objects are intrinsically complex does not imply that it is
difficult to obtain such objects from the current mathematical practice -
the paper discusses various ways for 'generating' such 'ingredients') and
extracts from them a huge amount of information relevant for classical
mathematics. To have a more precise idea of this, one can compare my version
of Fraisse's theorem with the standard formulation of this result (as
available for example in W. Hodges's "Model Theory").