FOM: Definition of f.o.m.

[John Mayberry]

Moshe' Machover's distinction between f.o.m. and ph.o.m. [Jan14] is of 
fundamental importance. But I believe that our discussion will benefit 
from a sharper formulation of what a f.o.m. must consist in. This will 
be of relevance to the controversy over whether topos theory can 
provide a foundation for mathematics.
	I start from the observation that mathematics is about *proof* 
and *definition*. This is what distinguishes mathematics proper from 
other disciplines, such as physics, economics, and engineering, which 
*use* mathematics. And it is because mathematics deals with proof and 
definition that it requires foundations in a way that other sciences do 
not. For mathematical proofs and definitions are intended to be 
complete, absolute, and final - that, in any case, is the ideal that 
mathematicians must strive for, even if it should never be perfectly 
attained.
	Mathematics, like a building, must stand upon its foundations. 
Therefore, to expound the f.o.m. is to present the basic presuppositions 
upon which mathematical proof and mathematical definition rest. These 
fall under three headings

1.) ELEMENTS. These are the basic notions of mathematics: the basic 
*concepts*, the *objects* that fall under them, and the basic 
*relations* and *operations* that apply to those objects. These basic 
notions neither require, nor admit of, proper mathematical definition, 
but all other mathematical notions are defined, ultimately, in terms of 
these basic ones.

2.) PRINCIPLES. These are the basic mathematical propositions that, 
although true, neither require, nor admit of proof, and that constitute 
the ultimate assumptions to which all mathematical proofs finally 
appeal. As such, they ought to be, at least in some sense, obviously 
and uncontroversially true.

3.) METHODS. These are the canons of definition and of argument that 
govern the introduction of new concepts and the construction of proofs.

This is, of course, a restricted, perhaps a minimal, notion of what 
counts as a f.o.m. But that makes it useful when we consider questions 
such as whether Theory X can provide a f.o.m.
	Martin Davis [Jan15] has called our attention to the true sense 
in which the foundations of present day mathematics are to be found in 
set theory:

"Look at almost any current graduate graduate textbook in whatever 
branch. It will begin with an introductory set-theoretical section on 
"notation". This represents a consensus that set theory is the proper 
foundation."

Exactly! And the scare quotes on "notation" remind us that in such 
introductory chapters the principles of set theory are typically put 
forward in the innocent seeming guise of mere definitions or notational 
conventions. ("The set of all subsets of a set S is called the *power 
set* of S and is denoted by P(S).", "Let N denote the set of natural 
numbers.", etc.)
	Notice that what Martin Davis calls "the proper foundation" 
here is not the formalized, first order axiomatic theory ZFC. Indeed, 
it could not, as a matter of logic, be a formalized first order theory 
of any sort, because the apparatus of set theory must already be in 
place before you can explain how formal axiomatics works. Surely it is 
obvious that no axiomatic theory, formal or informal, of first or 
higher order, could, on its own, constitute a foundation for 
mathematics. For it would be a central purpose of *any* foundational 
theory to give an explanation of, and justification for, the axiomatic 
method itself. Here when I speak of "axiomatic theories" and the 
"axiomatic method" I have in mind, not Euclid's, but the modern notion 
of axiomatics in accordance with which a system of axioms (e.g. the 
axioms for groups) is seen as *defining* the species of mathematical 
structures in which they hold true.
	The consensus set theory that provides the foundations of our 
mathematics is not, then, a formalized theory. To understand it you 
have to grasp what a set is, what membership means, etc. But it is a 
model of rigor nonetheless. And if you look carefully at the 
presuppositions underlying it, you will discover that the Principles of 
this consensus set theory - the basic assumptions that underlie 
mathematical proof - correspond to the formal axioms of first order 
ZFC. So if you do mathematics in the modern style you are working "in 
Zermelo-Fraenkel" whether you realize it or not. It is the 
non-formalized theory that is logically prior: formalized first order 
ZFC is parasitic on it.
	Now let me ask Colin McLarty: what are the Elements, 
Principles, and Methods that constitute the category-theoretic or 
topos-theoretic approach to f.o.m.? Give us a sketch of how *your* 
introductory chapter for a graduate textbook in functional analysis or 
topology might run. 
	 

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