FOM: Categorical vs set-theoretical foundations

[John Mayberry]

	The idea that *any* formal axiomatic theory can serve as a 
foundation for mathematics is profoundly mistaken - I would go so far 
as to say that it is logically absurd. This applies as much to ZFC as 
to the theory of a topos with whatever additional axioms you like. Let 
me explain.
	When you employ the modern axiomatic method your axioms, 
whether formal or informal, together define the class of mathematical 
structures in which they all hold true: that is their *logical* 
function. Thus to say that a theory is a *formal* axiomatic theory is 
to identify the truths of that theory - its theorems - with the set 
composed of all those sentences in the language of that theory that 
hold in all structures that model the axioms of the theory.
	Thus the formal theory of real numbers (the theory of complete 
ordered fields) is a *second order* theory, and its truths are the 
second order logical consequences of the axioms for a complete ordered 
field. Similarly, the formal theory of groups is a *first order* 
theory whose truths are the first order logical consequences of the 
group axioms. The same applies to the first order theory of toposes (or 
of toposes with a natural number object, or whatever) and, indeed, to 
the first order theory of sets, ZFC.
	Now with second order axiomatic theories, and with non-formal 
ones, you have no choice but to talk about the structures that are 
their models, about morphisms between such structures, about 
isomorphism classes, etc.. And all this talk has to have real 
content: otherwise you can neither explain what you are doing or 
justify it. Indeed, you cannot even make sense of it, and if you try to 
formalize that discourse in a formal topos theory or set theory or 
whatever, you will simply be confronted with the problem of explaining 
how *that* theory works, and why it is justified, and that is a task of 
the same sort as your original one.
	Now it might be thought that in the case of 1st order axiomatic 
theories you could avoid talking about models since first order logical 
consequence can be defined syntactically in terms of formal proofs from 
the axioms rather than semantically in terms of truth in all models of 
the axioms. But such a view is intellectually incoherent, and the 
reason for this is simple and quite straightforward: you cannot 
*justify* a system of proof procedures without using the the general 
notion of a model.
	Surely it is obvious that you have to justify a system of 
formal logical proof. Why should logical consequence be *defined* to be 
"formally derivable in just *this* system of formal rules and logical 
axioms"? To be sure, each formal derivation clearly witnesses a logical 
consequence (because the rules are *sound*). But how can you be sure 
that nothing has been left out (that is to say, how do you know that 
your system of rules, taken as a whole, is *complete*)? Although we 
have intuitions of the *soundness* of individual rules and logical 
axioms, we clearly do not have intuitions of the completeness of whole 
*systems* of axioms and rules. Goedel's Completeness Theorem is, after, 
a deep and indispensable result in first order logic.
	So in order to make sense of what you are doing, even in first 
order logic, you must take the semantic notion of logical consequence 
as logically prior to, and more fundamental than, the definition of 
formal derivation. And this clearly means that any attempt to use a 
formal axiomatic theory as a logical foundation for the whole of 
mathematics will inevitably involve you in a gross and obvious vicious 
circle. For the chief requirement of such a theory would be to explain, 
and to justify, the axiomatic method itself.
	Of course it is possible to maintain that a particular first 
order theory (e.g.. ZFC) contains a formal analogue of any proof that 
mathematicians at large are likely to accept as valid. In those 
circumstances you can sometimes conclude that a proposition whose formal 
analogue is formally undecided by the axioms (e.g. CH) is beyond the 
reach of present day mathematics. But such conclusions are not always 
warranted (e.g the consistency of ZFC is independent of ZFC, but any 
one who accepts ZFC is highly likely to accept its formal consistency 
too). This, however, is a far cry from saying that the formal first 
order theory ZFC provides a foundation for mathematics.
	But that is how Vaughn Pratt understands "set-theoretical" 
foundations:

"To avoid misunderstanding it should be said that ZF itself does not 
start with a preconceived notion of collection and go from there. ZF 
assumes only the language of first order logic with equality and an 
uninterpreted binary relation (membership). In fact, there is no a 
priori assumption at all about the universe being described by the 
axioms, other than the traditional (but unnecessary) assumption that it 
is non-empty. ZF weaves the entire notion of set from the whole cloth 
of first order logic."

Apparently Harvey Friedman agrees with Pratt, at least on the 
foundational use of formal first order axiomatic theories. Why else 
should he produce a set of axioms and then challenge the category 
theorists to match them in point of elegance, economy, etc.?
	But if Pratt's description of ZF is intended to be an account 
of "set theoretical foundations" then he is just wrong. And Friedman's 
challenge is irrelevant to the point at issue.
	To provide a foundation for mathematics you must say:

1st - what are the basic *concepts* that must be understood without a 
proper mathematical definition, and in terms of which all other 
mathematical concepts are to be defined.

2nd - what are the basic *principles* (*axioms* in the old-fashioned 
Euclidean sense) that must be accepted as true without proof, and which 
are the propositions to which all mathematical proof ultimately appeals.

and 3rd - what methods of definition and proof are to be employed

	Surely it is manifestly obvious that you cannot lay down a 
genuine foundation for mathematics in this sense simply by presenting 
a formal first order theory, especially if you are going to claim the 
right to draw on all the facts that we have discovered about these 
theories over the past 80 years or so.
	We have not yet seen a "category-theoretic" account of the 
foundations mathematics that is anything other than a presentation of 
either a single first order theory, or a family of such theories. These 
theories, described by Colin McLarty and others, have been interesting, 
fundamental, important, well motivated (pace Friedman and Simpson). But 
they are NOT *foundational* theories, and cannot logically be regarded 
as such. And therefore they are NOT in competition with set theory as a 
foundation for mathematics. 


 

--------------------------
John Mayberry
Lecturer in Mathematics
School of Mathematics
University of Bristol
J.P.Mayberry at bristol.ac.uk
--------------------------