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

[Vaughan Pratt]

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.  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?

 > 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?

> 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.

Best regards,
Vaughan