FOM: No foundations?

[Harvey Friedman]

Reply to John Mayberry 5:50PM 1/24/98

>	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.

The phrase "foundation for mathematics" has a long history.
Counterexample: ZFC (together with its standard
motivation). For the squeamish: use suitable fragments of ZFC; e.g., ZC.

>	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.

Trivial, but irrelevant. In the case of axiomatic set theory, the
axioms reflect evident facts about your conception. Godel and many others
discuss this.

>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.

Incoherent. The phrase "is to" conveys nothing.

>	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.

Conveys nothing. You should distinguish at least three formal
theories of real numbers. One if the first order theory of real closed
fields. THis is complete and decidable and has beautiful axiomatizations
and lots of direct connections with core mathematics. A second is the first
order theory of complete ordered fields, which also has beautiful
axiomatizations, but is not complete and is undecidable; however it's
logical consequences are r.e., and it is essentially the basis of a lot of
investigations in f.o.m. A third is the second order theory of complete
ordered fields, as a semantic object. This semantic object is complete but
is far far more undecidable. Once you make these distinctions, you can
begin to try to say what is really on your mind so that we can analyze it.

>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.

Trivial and empty.

>	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..

Incoherent. What exactly do you mean by a second order axiomatic
theory? As a semantic object, or a proof system, or what?

And who is "you" and what is "choice" and what is "talk"?

>And all this talk has to have real
>content: otherwise you can neither explain what you are doing or
>justify it.

The axioms of set theory, and of restricted set theory, and various
axiomatizations of complete ordered field have obvious real content. This
content has been explained and justified at various levels, in various
ways, with various thoroughness, by various authors. This is well known.

>Indeed, you cannot even make sense of it,

People obviously makes sense of it in the well known ways.

>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.

The set theory axioms and/or relevant fragments thereof follow immediately
from the clear conceptions at hand. Read Godel and many others. In
contrast, the axioms of formal topos theory do not follow from any clear
conception - and the zealots are very very proud of this because it
supports so much ambiguity, which they call flexibility.

>	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.

Of course you avoid talking about models. You talk about the objects
themselves. And in a totally coherent way. Sure, issues can be raised for
BIG set theory, but not for suitable fragments.

>But such a view is intellectually incoherent,

The usual view is completely coherent. Your objections are 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.

Sure you can. By induction. The axioms are obviously true, and the proof
procedures preserve truth.

>	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"?

You seem to be saying something like: if the axioms you write down are not
complete, then they are incoherent. If you are saying this, then what you
are saying is incoherent - and bizarre.

>To be sure, each formal derivation clearly witnesses a logical
>consequence (because the rules are *sound*).

Thank you. Soundness is by induction as I have indicated above.

> 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*)?

Nobody said anything about completeness. Godel says that it is an open
ended process.

>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.

We don't need such intuitions to have a suitable foundation.

>	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.

An amazing consequence!! This doesn't follow and is of course false. Who
says that you have to be complete in order to know what you are doing?

>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.

Another amazing deduction! I have
been talking on the fom for about a week using the phrase "practical
completeness." Did you notice?

>For the chief requirement of such a theory would be to explain,
>and to justify, the axiomatic method itself.

The axiomatic method is explained in a lot of textbooks.

>	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.

Not only is it possible, but this is the standard, correct, view.

> 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.

Ditto.

>This, however, is a far cry from saying that the formal first
>order theory ZFC provides a foundation for mathematics.

It is exactly (a major ingredient in) what is meant as a foundation for
mathematics.

Then Mayberry quotes Pratt as follows:

>"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."

ZF does start with a preconceived notion of collection (set) and does go
from there. One takes first order logic with equality and membership as
primitive. This comes for free given that we are engaged in exact thought.

>Apparently Harvey Friedman agrees with Pratt, at least on the
>foundational use of formal first order axiomatic theories.

I'm not sure.

>	But if Pratt's description of ZF is intended to be an account
>of "set theoretical foundations" then he is just wrong.

The usual motivation and presentation of ZFC is an account of "set
theoretical foundations."

>	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.

Set, membership, and optionally, equality.

>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.

The usual axioms of ZFC.

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

Those in standard treatments of first order predicate calculus with
equality. So ZFC and its usual motivation does provide a foundation of
matheamtics after all!

>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.

I just did.

>	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.

You haven't even seen that on the fom.

>These
>theories, described by Colin McLarty and others, have been interesting,
>fundamental, important, well motivated (pace Friedman and Simpson).

McLarty hasn't described anything in serious detail. My assessment:
Interesting only in applications to core matheamtics. Fundamental only
perhaps to certain limited aspects of core mathematics. Important only in
applications to core mathematics, and subordinate to the importance of the
relevant core mathematics. Well motivated only by applications to core
mathematics. Grossly ill motivated as foundations of mathematics.

>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.

Nice to see you end with something I am in total agreement with.