FOM: Reply to Friedman -- what Tragesser means by "elementary"

[jshipman@bloomberg.net]

Harvey says Tragesser's distinction between elementary and nonelementary proofs
is nonstandard usage.  I understand the distinction as being between proofs
which do not use concepts from "outside the mathematical subject at hand" (in
particular where the theorem can be proved in any reasonable system in which it
can be stated), and proofs which use some sort of "higher machinery" (such as
complex analysis for the proof of the P.N.T., Aleph_omega1 for the proof of
Borel determinacy,  and so on).  This is an *informal* distinction but it is
*not* an unclear one.  The word "elementary" is a relative, not an absolute
term meaning you don't go beyond the system in which you are comtemplating the
proposition in order to prove it.  (Mathias has an interesting example in his
paper on strong systems of analysis (which he pointed us to the other
day)--determinacy for Turing-invariant Borel sets implies Borel determinacy
provably in ZC but the proof in some sense depends (not logically but in order
to be intelligible) on infinitely many uncountable cardinals.)  Harvey, do you
want to suggest an alternative term to "elementary" for this concept?--J Shipman