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

[Anthony Coulter]

In light of the recent discussion about whether N would be a subset of R 
in an good, standardized formalization of regular mathematics, I would 
like to ask a few related questions. In the below, the "Standard 
Library" is whatever ideal formal system the reader chooses to imagine.

1. Should the Standard Library make use of the extended real line?
     When analysis books discuss the limit supremum, the limit infimum, 
and measure theory, they treat positive and negative infinity as 
"physical objects." (Contrast with ordinary limits, where the infinities 
are usually abstracted away so they don't appear in the definition at 
all.) The trouble with these objects is that they are a bit nastier to 
construct---Cauchy sequences don't converge to infinity---and that might 
cause problems with some foundational systems.

2. What background set theory is needed to discuss topology and abstract 
algebra?
     Many different set theories exist (ZF, Kripke-Platek, New 
Foundations, etc.) but algebra and topology textbooks tend not to bring 
them up by name. The axiom of choice is the only axiom that tends to 
warrant special note in such books. Other variations (which seem to be 
designed to trim the constructable hierarchy) don't seem to matter to 
regular mathematicians. What set theory best captures this background 
that mathematicians use? (I personally think the answer to this is 
higher-order logic, but I raise the question anyway.)

3. How should the Standard Library deal with the category of all groups?
     Saunders MacLane only mentions ZFC in "Categories for the Working 
Mathematician" in an appendix, where he mentions it only to show that it 
isn't even necessary for the development of category theory. Meanwhile, 
it has been claimed that Mizar is based on Tarski-Grothendieck set 
theory rather than ZFC to provide arbitrarily large universes for 
category theory. How much set theory is actually needed here? (Questions 
2 and 3 could be merged, but I separate them because I've read so many 
articles bemoaning the restriction to small categories.)

4. Regarding many-sorted logic: How do mathematicians approach types in 
actual practice?
     Generally speaking, they seem to reject "3\in 5" as a meaningless 
ill-typed statement (unless they're dealing with von Neumann ordinals). 
But I think they're less likely to reject "1/0" as ill-typed---it's 
undefined, but most folks I've talked to consider it a well-formed 
expression. But then I wonder: 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")? [This question gets to the heart of the N\subset 
R debate from earlier.]

4. How do mathematicians who are *not* foundations of math people regard 
undefined terms and free logic?
     In actual practice, the most common approach is to refrain from 
proving theorems about 1/0. But the Standard Library needs a Standard 
Logic, so "(1+1)/0 = 2/0" and "1/0 + 2 = 2 + 1/0" must each either be 
provable or not provable. What conventions would be least offensive to 
mathematicians? (My answer: a = b -> f(a) = f(b) is logical but 
commutativity is mathematical [and doesn't even apply to all supersets 
of R, e.g. the quaternions] so the former is true and the latter is 
false.) Likewise, do non-FOM mathematicians think of explicit existence 
predicates as natural concepts or ugly hacks (the way we see setting 1/0 
= 0)? (I personally think existence predicates are fine.)

Regards,
Anthony