FOM: Banach-Tarski/Borel/Elementary

[Harvey Friedman]

>From Steel:
>If you restrict your view
>to Borel sets, you can **see** neither a wellorder [of reals] nor a
>paradoxical
>decomposition, and if the **sight** of such offends you, then I suppose that's
>some advantage to you. Ross himself found the sight inoffensive.

(Asterisks mine). I've never seen one. John - have you ever seen one, and
if so, which one did you see? Or did you see all of them at once? But
that's too many to see at once. Which one or one's did you see first?

Obviously I'm playing games with the result that there is no provably
definable paradoxical decomposition. On Steel's view, is there a definable
paradoxical decomposition?; does this question make sense on Steel's view?

What is the relationship between there provably not being any Borel
paradoxical decomposition and there not being a provably definable
paradoxical decomposition? I hope to take this matter up at some point in
serious detail in my positive postings.

Do mathematicians regard paradoxical decompositions as objects worthy of
study today? If not, why not?

>From Steel:
>In any
>case, **you** have made no progress whatsoever in taming the geometrical
>complexity of R^3 coming out of the fact that F_2 embeds in its isometry
>group.

(Asterisks mine). Who is "you"? I guess "people who look exclusively at
Borel sets." By looking exclusively at (at most) Borel sets, one focuses
attention on aspects of R^3 other than the pathology of paradoxical
decompositions. Mathematicians view the geometrical complexity of R^3 as
not including the matter of paradoxical decompositions. On my view, the
real importance of paradoxical decompositions is that it adds an additional
striking reason to concentrate on (at most) Borel sets.

>From Steel:
>   There is a larger question here: how is TBU meant to be used? One
>can restrict one's attention to Borel sets in the contexts where it is
>appropriate to do so without having a formal theory like TBU around.
>People have been doing it for the last 100 years or so.

Throughout mathematics, it is almost always appropriate to - and one
usually does - restrict one's attention to Borel subsets of complete
separable metric spaces. However, I make a living discussing contexts in
which one must go well beyond Borel subsets of complete separable metric
spaces in order to prove things about Borel subsets of complete separable
metric spaces (or even about finite trees).

It is almost always appropriate to develop formal theories reflecting
mathematical reasoning that has a history of 100 years. This is the essence
of "logic." The development of predicate calculus is "logic." The
development of axiomatic set theory is "logic." Obviously, "logic" is not
strictly necessary; e.g., the development of formal set theory is not
necessary to do set theory. I assume you will join me in admiring Steve
Simpson for doing some relevant "logic" by formulating an interesting
(wholly provisional) formal theory of Borel mathematics.

Tragesser uses the term "elementary proof" in a completely different way
than it has been used in mathematics this Century. The way that it is
normally used, it is completely captured (as an upper bound) by tiny tiny
fragments of ZF. In discrete contexts, it is generally captured (as an
upper bound) by systems such as EFA - exponential function arithmetic. When
one deals with real numbers, there is perhaps more of an issue of what
elementary generally means, but one can use systems like ACA_0 as a working
upper bound. Tragesser could help by clarifying what he means by
"elementary proof."