[FOM] Standardization of sets, sorts, and free logic

[Anthony Coulter]

So far all the discussion has been about 1/0, so I would like to answer
two of my other questions in the hope of providing some variety.

 > 1. Should the Standard Library make use of the extended real line?

Yes, it should. The Standard Library should follow standard textbooks,
and standard textbooks (e.g. Rudin and Apostol) use extended reals
unapologetically. By an extension of this reasoning, the Standard
Library should also provide the extended reals axiomatically, i.e. it
should postulate the existence of two objects that satisfy certain
arithmetic laws without worrying about how to construct them. (To be
more specific, I think it would be silly to construct the infinities as
divergent sequences by analogy to the Cauchy construction of R itself.)

 > 4. Regarding many-sorted logic: How do mathematicians approach types
 > in actual practice?
 > ... Would a regular mathematician regard "the  sum of 1/n^2 as n goes
 > from e to pi" as ill-typed (like "3\in 5") or undefined (like "1/0")?

I already posted an argument elsewhere that "undefined" and "ill-typed"
need to be separate concepts, so here I will proceed as though there is
no contention on that issue. Then: I would say that my example above
is ill-typed rather than undefined, by the following slippery slope:

A.  n*(n+1)/2 is an integer whenever n is.
B.  n*(n+2)/2 is an integer for even n, and restricting a sum to even
     terms only is perfectly reasonable. (Number theorists often take
     sums over the divisors of a given number; taking a sum over even
     numbers isn't a big deal.
C.  (phi^n - (1 - phi)^(-n)) / sqrt(5) is an integer whenever n is, for
     phi = (1+sqrt(5))/2. (This formula gives the Fibonacci sequence.)

The examples above get progressively less plausible as upper bounds of
mathematically interesting sums, but my point is that it's unnatural to
legislate a line between "reasonable situations" like division by two
when the number is "obviously" even and "unreasonable ones" where the
proof of well-definedness is more involved.

I should also add that number theorists studying Diophantine equations
often make use of larger number fields. Most presentations of Pell's
equation (x^2 - n*y^2 = 1 for integer x, y, n) work in the quadratic
field Z[sqrt(n)]. Number theorists would be horrified if they had to
write extra "cast" functions to turn the integers into ther correspond-
ing reals and vice-versa in the recurrence formula for the solutions to
this equation. Diophantine analysts have more "integer pride" than
anyone else and they still make casual use of the fact that N is a
subset of R. So I think it's fair to say that mathematicians do *not*
typically think of the naturals as being fundamentally different from
the reals.

Regards,
Anthony