FOM: e intersect pi

[Harvey Friedman]

This post is inspired by Randall Holmes, 2:58PM 1/23/98.

A common fatuous objection to set theoretic foundations of mathematics is
that it picks ad hoc presentations of basic structures in mathematics and
saddles mathematics with ridiculous "theorems" like the intersection of e
and pi is e. Or some ad hoc definition of pairing like (x.y) = {{x},{x,y}}.

Fatuous objections like these are uniformly handled in the manner indicated
by my positive posting 5:42PM 11/15/97, 5:Constructions. Applied to here,
we use the standard set theoretic development to prove what might be called
"literal" R, say by Dedekind cuts, with its ordered field structure. This
is what is riddled with phenomenon like the intersection of e and pi. Then
we have proved "there exists a complete ordered field." Then we apply the
rule in the previous posting that asserts that we can introduce a constant
symbol for a complete ordered field. Then there is no more problem of the
kind the other side is complaining about. In practice, of course, one
introduces a complex of constants for the components of an ordered field.

One can do a similar thing with ordered pairing. Here one can introduce a
function symbol and postulate the important property. One proves as a
metatheorem that these moves are conservative extensions. So they can be
added as proof rules. These are, basically, "definitional extension"
theorems of logic.