FOM: Better terminology?

[Harvey Friedman]

Shipman writes:
>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).  ... Harvey, do you
>want to suggest an alternative term to "elementary" for this concept?

You seem to be looking for a one word adjective. I usually just refer to
the relevant spot in the canonical well ordered hierarchy of fundamental
systems of f.o.m., ranging from about EFA (exponential function
arithemtic), throught ZFC, all the way to ZF + elementary embeddings from V
into V, and somewhat beyond.

If I were to pick a one word adjective, I'd go for "self contained". E.g.,
Borel determinacy has no self contained proof. But I'd rather point to
"uncountably many iterations of the power set operation" or "uncountably
many uncountable cardinals", depending on the audience.