[FOM] Should mathematicians be explicit about what they are assuming?

[Joe Shipman]

Martin, I think it's a little unfair to say we have been ignoring the context. In the case of the Axiom of Choice, the biggest reason people stopped citing its explicit use in the 1940's was that metatheorems were proven showing, first that AC was consistent with ZF so that there was no fear a theorem proven using AC might be contradicted, and then that the use of AC could be eliminated from all theorems of sufficiently concrete logical type (in particular, practically all of mainstream mathematics after the more abstract theorems were specialized to separable spaces).

There is no other example of an axiom which used to be routine to state explicitly but is now commonly assumed without mention, except for the notorious case of the Grothendieck Universe axiom, where the failure to state it arose not from the broader mathematical community widely accepting the axiom, but rather from the narrower subcommunity which used it refusing either to defend its use or to take the effort to prove a metatheorem showing its eliminability. I regard this discussion forum as having made an important contribution to mathematics by raising this issue insistently and encouraging Colin McLarty to develop and supply the details that the algebraic geometers and number theorists would not.

The recent discussion here has not been about whether axioms going beyond ZFC needed to be stated when used in proofs, but about the more subtle issue of whether it was desirable to stating the logically simplest version of an axiom (i.e. consistency of a measurable cardinal, which is pi^0_1 in the language of number theory, rather than the existence of such a cardinal). 

(By the way, what is the logical complexity of the Real Valued Measurable Cardinal Axiom?)

-- JS

Sent from my iPhone

On Feb 26, 2013, at 11:40 AM, Martin Davis <martin at eipye.com> wrote:

The discussion of this matter has been ignoring the social and historical context in which mathematical work takes place.

You will rarely see a contemporary paper noting dependence of a particular theorem on the axiom of choice. As late as the 1940s it was standard practice to do so. Once in calculations that used complex numbers, it would be noted that these are "fictitious".

The statement that "ZF+ some large cardinal" is consistent is Pi-0-1. Hence if that system is inconsistent, there will be a numerical counterexample which in turn would imply that a specific polynomial equation has an integer root.

Martin

Martin Davis
Professor Emeritus, Courant-NYU
Visiting Scholar, UC Berkeley
eipye + 1 = 0

_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom