FOM: The logical, the set-theoretical, and the mathematical

[Harvey Friedman]

Reply to Shipman 5:54PM 9/11/00:

>My position is as follows.  Comprehension axioms are "logical".

I am perfectly willing to go along with this kind of distinction, but at
some point one would like to get a handle on the "logical" versus
"mathematical". That becomes interesting to me only when I see a payoff in
doing the very hard work necessary to get clear about it. There is another
kind of distinction that does have obvious payoffs, but which is different
than what you are talking about - self evident axiom, or fundamental axiom,
or simple axiom, versus axioms proposed for extrinsic reasons like coherent
pragmatism. The payoff here: CONJECTURE: ZFC captures all such axioms. But
where is the comparable payoff for what you are talking about?

>I agree
>with Harvey that Set Theory is a branch of mathematics,

I said "originally" (or meant it).

> and therefore
>regard the axioms of set theory as "mathematical",

That doesn't follow, but I am willing to go along.

>though much closer to
>being purely "logical" than axioms about other mathematical structures.

I am willing to go along.

>HOL (using a deductive calculus with a Comprehension rule as in
>Manzano's book)  is indeed enough to develop "Ordinary Mathematics".

Only badly, in comparison to ZC = Zermelo set theory + AxC. Having untyped
variables makes a huge difference in the smooth formalization of
mathematics. (In various computer science situations, people prefer to have
types of various kinds). And where is the axiom of infinity?

>(Mossakowski insists on an axiom of Infinity as well, but Jones argues
>that this axiom is purely ontological and is only necessary in a
>metaphysical sense.   However, I am willing to accept a modified
>logicist thesis that (ordinary) mathematics = logic plus Infinity.)

Without infinity, what you say is on the surface false.

>The Axiom of Choice has a special status.  It is not necessary for the
>development of number theory, but is certainly an essential part of
>ordinary mathematical practice for analysis and algebra.

Essential? Certainly not essential under many readings of the word. Nothing
contemporary analysts and algebraists say they really care about would be
lost by being somewhat more explicit in hypotheses in order to avoid its
use.

>Various forms
>of AC are more or less "logical" in flavor but I want to research these
>some more before saying whether I think it can properly be considered a
>"logical" axiom.

Once you question the logical character of full AxC, you are down the
slippery slope of starting to realize that you are going to want to really
understand what "logical" means in a way that no one has ever made clear.

>Harvey's insistence that ZFC captures the intuition about sets that
>mathematicians had all along (presumably from Cantor c. 1880 to 1930)
>seems ahistorical.

At least ZC, not ZFC. This still seems right to me. Just look at the
foundations of the real number system and elementary analysis, all the way
from the integers (take them as urelements) through rationals (as ordered
pairs) through Dedekind cuts (sets of rationals) through sets of reals. The
real line is an application of power set. Remember, there is no axiom of
foundation in ZC.

>There were several unsuccessful or incomplete
>attempts to formalize sets and classes, and Type Theory must still have
>been considered an important alternative (to set theory) foundation of
>mathematics as late as 1930 (otherwise, why didn't Godel refer to
>Zermelo's system rather than Russell's in the title of his
>"Incompleteness" paper)?

You are talking about logicians trying to set up formal systems, not
mathematicians trying to develop mathematics.
There are several experts in the history of such matters on the FOM. I am
not one of them.