FOM: set/cat "foundations"

[Harvey Friedman]

Reply to Mossakowski 1:53PM 2/26/98.

>What about Lawvere's "category of categories"*? Isn't this an alternative
>f.o.m., or at least some starting point in the right direction?

Not an alternative as it stands; e.g., it is not based on an alternative
coherent intuitive conception. It can be viewed as a translation of set
theory in less useable notation.

>The category of sets comes in only at a very late stage, but
>indeed it is there, showing that this is powerful enough to do all needed
>mathematics. Of course, one is not forced to use the category of
>sets. One can directly work with categories. (However, I don't know how
>good this works in practice.)

A main point would be: how good working directly with categories, without
using standard set theoretic ideas, is in practice. You tell me.

>Would you call Lawvere's foundations a "slavish translation of set-theory"?

Why not?

>Perhaps a problem of categorical foundations is that the meta-theory
>of first-order logic is naive set theory. For categorical foundations,
>one might need a more category-based formalism, like sketches
>(but sketches themselves are definitely too weak). Hopefully, such a
>formalism would make Lawvere's axioms more concise.

You may well be putting your finger on an important aspect of what is
missing, and what needs to be done to make categorical foundations a
reality. I should add that I don't fully understand exactly what you are
saying here. What is a sketch?