[FOM] R: Preprint: "The unification of Mathematics via Topos Theory"
pratt at cs.stanford.edu
Fri Jul 16 02:29:32 EDT 2010
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
> 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.
More information about the FOM