There is a gamut of theorems along this spectrum and I view the sphere paradox as a place to avoid just as there are places on high mountains that I avoid. I do suspect that the Banach-Tarski theorem can be formally derived from any axioms that are now known to be adequate for Lesbegue measure theory which is the only foundation for the math that physicists and engineers use every day. It is not a pretty picture.

Benson Mates read a great deal of Greek math in the original and told me that the Greek’s notions of area was by no means like a set of points which is the modern notion of area.

While I believe there are infinitely many primes and computer science makes some use of primes, I suspect that most computer science could do well with an arithmetic with a finite number of integers, just like C. Such a theory of arithmetic would be somewhat more awkward, just as C is somewhat more awkward when we need bigger integers than the hardware provides. Sometimes we would would need to reason about tuples of these bounded integers just as we use tuples of integers in C when forced. In short I don’t think that most CS needs infinity. It may, however, be good engineering.

Two years of math courses at Berkeley viewing each course thru the perspective of formal logic convinced me that formal logic could carry the day, except in complex variables where the instructor kept drawing pictures in the complex plane. Actually I think that formal methods would do there too with just a few more notions and proofs.

All of the papers I have skimmed about applying formal methods to real computer problems seemed to address problems that seemed appropriate to me. Appropriate but perhaps not yet feasible. See this.