FOM: set/cat "foundations"

[Till Mossakowski]

Colin McLarty wrote:
>        Mossakowski suggested categorical foundations could use
>sketches instead of first order logic, and Friedman said he might
>be onto something. But oviously a formal metatheory of first order
>logic is easy to give in a weak intuitionistic third order
>arithmetic--thus in any topos with natural numbers, and in many
>weaker categories.
That misses the point. I did not speak about a formal meta-theory
for first-order logic, but about its informal meta-theory. And clearly,
first-order logic is based on informal set theory: its interpretation
(even if we do not consider model theory, we have some intuition about
this)
is based on a non-empty universe, which is a set of objects, and not
a category.
Foundations always are in some sense circular. First-order logic is
based on naive set theory, and formal set theory is formulated in
first-order logic. It is clear that you cannot avoid such a circle.
Moreover, I would call it a success of set-theoretic f.o.m. to have
established such a circle.
Now I just guessed if categorical foundations would be more successful
if they also tried to establish such a circle.
At least, I find the definition of a topos much more convincing when
given
in a categorical setting (as it is done in many text books) than when
pressed into the form of first-order axioms.

Till Mossakowski