FOM: essentially algebraic, open problems

[Harvey Friedman]

Reply to Mclarty 11:56AM 3/15/98:

Awodey 11:43PM 11/13/98 responded to Simpson saying:

>My point in bringing it (essentially algebraic) up was that it seems
>reasonable to regard
>the logical complexity of the axioms of a theory as a measure of simplicity
>that is at least as significant as the number of bytes occurring in those
>axioms, and so this is a sense in which the topos axioms are simpler than
>those for conventional elementary set theory.

I wrote in reply to Awodey:

>>Well, let's look at the logical complexity (in this sense) of the axioms
>>for topoi given by McLarty'posting of 9:21AM 2/6/98 Challenge axioms, final
>>draft.
>>
>>1. A
>>2. AE
>>3. A
>>4. AEA
>>5. A
>>6. AEA
>>7. A
>>8. axiom missing or nonexistent
>>9. AEA
>>10. AEA
>>11. AE
>>12. AEAEA
>>13. EAEA
>>14. AE
>>15. AEA

Mclarty writes:

>	These are not the topos axioms. They are axioms for a
>particular kind of topos specified in your challenge.

Since Awodey was writing in the context of measuring "logical complexity"
of axioms, in response to Simpson who was talking about Mclarty's
presentation, it was natural to assume that he was talking about
presentations of topoi axioms for the purpose of f.o.m. - and not some
algebraic construction. Remember, algebra is not logic, and logic is not
algebra. So I responded about the logical complexity of the only
presentation made on the fom of topoi axioms for the purpose of f.o.m. If
you have another version of the topoi axioms for the purpose of f.o.m. then
by all means present it. It is a standard tool of classical f.o.m. to use
workable versions of predicate calculus with introduction of new symbols by
abbreviation and with partially defined terms. It appears to me that in any
style of setup relevant to f.o.m., the axioms of topoi will be already
significantly more complicated than those of even ZFC (ZC and Z being
simpler still). This is independent of and in addition to the fact that
they are philosophically incoherent, relying on the prior notion of set for
their coherence. The only way out of this is to complain about the use of
schemes in standard f.o.m. As I indicated before on the fom, schemes are
already used in the formulation of the underlying logic.

In fact, the axioms you wrote down are not only very clumsy in comparison
to standard axioms for set theory, they also are unusable as formal f.o.m.
For example, as I have said on the fom, I do not believe that one can
actually conveniently formalize mathematics in any formal system without
schemes. This is because mathematicians routinely use mere expressibility
(by wffs) as a sufficient criterion for object formation (i.e., forms of
comprehension), and do not carefully break up the relevant wffs into their
componenents and successively build up terms or introduce symbols by
definition for the components. This feature of the formalization of
mathematics is well known to people who actually do formalization of
mathematics - e.g., the Mizar people.

Mclarty writes:

>	No, it is not [essentially algebraic]. You have to remember your
>own challenge, which
>was to write axioms in standard first order logic. Standard first
>order logic does not use partially defined terms, while I suppose
>everyone knows that category theory is most simply presented using
>them, and an essentially algebraic presentation uses them.

The essential challenge is to write down any formal system of any kind that
serves as a foundation for mathematics, in the sense that one can actually
conveniently formalize actual mathematics, in a way that bears any serious
resemblance to the way basic textbooks are written and the vast majority of
mathematicians teach rigorous mathematics. I gave the challenge in more
constrained terms simply as a result of the frustration of not being able
to communicate the form of the challenge given in the previous sentence.
This challenge has been reasonably met by the usual formal set theories -
with qualifications - but appears to be completely out of the question for
any alternative scheme for the reasons I stated above.

I should remind everyone that there appears to be no book which
systematically develops a serious amount of standard basic mathematics in a
(even quasi) formal system of categorical foundations. The slavish
translation of set theory into Boolean topoi does not accomplish this
satisfactorily.

>	Challenges are generally not a helpful way to discuss an
>issue, because they tend to constrain the discussion to the
>challenger's own way of looking at it. But they are especially
>unhelpful when the challenger then forgets what the challenge was
>and complains that the response does not ALSO answer some quite
>different question.

We don't need your false righteous indignation over my response to Awodey,
because you don't want to or can't or haven't yet produced an "essentially
algebraic" system that has any relevance to categorical foundations of
mathematics. Why don't you simply say: "there are other axiomatizations of
topoi theory which are for various algebraic purposes that are essentially
algebraic" rather than make up a wholly artificial disagreement?

Mclarty 10:12AM 3/10/98 writes:

>       	Here is a point of kinship between categorical foundations
>and ZF (or ZF descendents such as Feferman's theory): Neither of us
>need claim credit for Aristotle, Frege, Cantor, Cauchy, Hilbert, or
>Russell. We are both heirs to all of them--though I'd have included
>Dedekind in that list and might not have thought of Russell. I will
>mention that Aristotle, Cauchy, and Hilbert are all notoriously
>"list 2" types. Goedel's incompleteness theorems too have no closer
>tie with set theory than with any other first order foundations.

Kinship, bullship. The reaction of any of these eminent people to
categorical pseudo foundations would be the same as mine is. This is
particularly clear of Cantor. All of these people were involved in
axiomatization in one sense or another, (let's add, e.g., Dedekind and
Zermelo, Godel, von Neumann), and one thing that they had in common was
philosophical coherence. In categorical pseudo foundations there is no
philosophical coherence. And since the role of predicate calculus is
severely minimized in categorical pseudo foundations, it is ridiculous to
claim the Godel incompleteness theorem as part of your "heritage."

Mclarty continues:

>THREE OPEN PROBLEMS IN CATEGORICAL FOUNDATIONS:
>
>    	The most prestigious is on-going axiomatizations in
>homology. This includes describing "motives", a kind of universal
>(co-)homology which involves hard technical problems. ...

Appears not to be a problem in global f.o.m., but a much more specialized
matter. I'll look into this, starting with writing to my colleagues here to
see what they have to say. By the way, your remarks a long time ago on the
fom about justifying categorical foundations via Wiles' proof of FLT was
received by several people here as bullship. The impression was that you
piggyback on some fashionable avenues in core mathematics where categorical
foundations is a minor side issue.

>    	More traditional foundations: Is there a reasonable
>"category of all categories" which includes itself among its
>objects? Every set theory with a universal set gives categories
>which include themseves as objects, by the usual definition of
>categories and functors in terms of sets. But these categories
>are never cartesian closed and so are not reasonable versions of
>a "category of all categories". And this set theoretic approach
>construes "object of" in an unnecessarily narrow way.

This is a reasonable question, which, I think, Feferman has stated
previously on the fom in his own terms. You would do a great service to the
fom if you stated a precise open question in this regard.

>    	Third (the most clearly manageable): Can the adjoint
>lifting theorem for triposes (from Andy Pitts's dissertation)
>be gracefully transported to regular categories (presumably
>with some supplemental conditions)? If so, the theory of
>realizability toposes could be radically simplified,
>among other things (see Japp van Oosten's dissertation).

Looks like it is for specialists.

As I expected, you have not presented any fundamental open problems that
look attractive from any general intellectual point of view, with the
possible exception of number 2. Even here, there is the need to say more
about what one would like; e.g., present some precise form of this. Left as
it is, number 2 seems to be covered under much older questions such as
building appropriate set theories with a universal set, new ways out of the
Russell paradox, etc. I have worked on this, and do have some specific nice
axioms that I don't yet know are consistent. I come to this armed with the
huge technical development of classical f.o.m. which, as I said above, is
as strong as it is partly as a consequence of its philosophical coherence.

Of course, there is the classical NF stuff which I don't endorse - but this
also did not come from categorical foundationalists.