[FOM] Why not this theory be the foundational theory of mathematics?

[Thomas Klimpel]

Colin McLarty wrote:
> I am curious to know what this means:
>
> Thomas Klimpel wrote
>
>> (The category of all sets is
>> specified by a sort of "last word quantification", but this is
>> troublesome for a foundational theory. A foundational theory should
>> lay down the first words, not insist on having the last word.)

My remarks about category theory were triggered by Muller's paper
(http://philsci-archive.pitt.edu/1372/1/SetClassCat.PDF), especially
by the following passage in the middle of page 11:

> When a category-theoretician talks about **Set**, *he means all sets, i.e. all sets available in the domain of discourse of mathematics*, which has now become V+, not V  \subset V+, because old V comprises less than a thee spoon of the sets in the indefinitely expanding cosmos V+. When a category-theoretician hears there are sets available of cardinality i1, 2^i1, i1^\omega, \alpha_i1, etc., he means to include *these too* in **Set**, because these are also sets according to these stronger set-theories, not mathematical objects distinct from sets.

This passage gave me the impression that foundations of category
theory could turn into a fight over words. Who has the last word, and
how can one define the words such that the last word reserved to
category theory will still fit with the foundations given before that
last word. This might be an interesting challenge, but this sort of
challenge seems unrelated to the role that should be played by a
foundational theory.


When I talked about category theory as too vague for a foundational
theory, I thought about the passage at the top of page 2:
> Lawvere [1966] proposed **CAT**, the category of all categories (save itself), as the domain of discourse of mathematics, and embarked on the endeavour to axiomatise **CAT** directly

Independent of whether Lawvere came up with a nice set of axioms for
**CAT** or not, this just feels too vague to me. It is one thing to
formalize category theory like group theory or lattice theory. If ten
people tried this independently, at least eight would probably come up
with equivalent formalizations. But if the same ten people tried to
formalize **CAT**, they would end up with ten different non-equivalent
formalizations.

(If ten people tried to formalize set theory, none would come up with
ZFC. Some would come up with inconsistent systems like Frege, some
with second order formalizations like Zermelo, some with systems
equiconsistent with finite order arithmetic like Russell and
Whitehead, some with even weaker systems. Yes, set theory is also
vague, but ZFC is not.)


When I say "last word quantification", I try to capture an interesting
property of the full semantics of second order quantification (which
is absent from Henkin semantics). The second order induction axiom
characterizes the natural numbers up to isomorphism. Initially,
neither addition, nor multiplication or exponentiation is defined,
only successor. But as soon as a symbol and axioms for an operation
like exponentiation is added, the second order induction axiom
includes it too (as a way to define properties). Since we know pretty
well what we mean by the natural numbers, having the last word might
not be bad in this case. However, a similar game could also be played
for the real numbers (defined as a complete ordered field), but that
does not mean that we know similarly well what we mean by the real
numbers.

Thomas