The finite axiom of choice doesn't suffer from paradoxes of infinity.

It's mostly intuitive to computer scientists that infinities don't exist ;)

And we are also in the habit of proving/realizing our choice-functions rather then assuming them axiomatically.

https://en.wikipedia.org/wiki/Nondeterministic_programming

Well, if one assumes finiteness all of these paradoxes go away and this discussion is not about anything anymore. I studied physics and am quite attached to infinities. That one constrains oneself to a finite state system mostly does not mean that one is not allowed to look out of the window towards the stars and marvel at infinity anymore.

From your comment above I am making the (admittedly presumptuous) inference that you didn't study Quantum physics.

https://en.wikipedia.org/wiki/Renormalization

If giving up infinities allows me to understand The Universe better, I don't see how that robs me of marveling at the stars - it only makes it more exciting!

I can't comprehend an infinite universe. Nobody with finite memory/time can.

Well, I did a PhD in quantum field theory and as part of that published a paper on renormalization..... Of course the infinite sets involved can be approximated using finite sets if one does not mind losing important symmetries. Still, these finite sets would still be frightingly and incomprehensibly large.... If one wants to comprehend anything one may be better off just ignoring quantum mechanics..... And I am not talking about the measurement problem. I am talking about the incredible vastness of the state space. The wave function of the universe is an incredible and completely untractable thing even if one assumes it is finite. It contains all possible histories of the universe for one thing and lets all of these possible histories interact with one another.

I hear you (and I obviously made a bad inference re: your background - apologies), but there is a distinction to be made between large-but-finite (computable? halting?) and infinite (non-computable? non-halting?) sets.

We can't comprehend the universe using numerical methods - it's too complex for our brains/computers.

But we can understand complexity using symbolic methods.

Symbolism/representationalism (religion) is rather inevitable part of the human condition.

∞

Infinite sets are a useful abstraction, but uncountable infinities can probably be avoided since the Löwenheim-Skolem[0] theorem says that any countable first-order theory has a countable model.

[0] https://en.wikipedia.org/wiki/Löwenheim-Skolem_theorem

Löwenheim-Skolem doesn't hold for higher order logics such as type theory/Lambda calculus.

Basically, it doesn't hold for any constructive logic.

It has little to do with the Hilbert Hotel. It is sufficient to decompose the original ball into 5 (!) pieces:

https://mathworld.wolfram.com/Banach-TarskiParadox.html

It is an existence proof that relies on the Axiom of Choice, of course there is no algorithm to actually construct those pieces.

This is one of the reasons that people distinguish between ZFC and ZF (Zermelo-Fraenkel with and without AC).

ZFC is not regarded as sound by some because of these Paradoxes.

> ZFC is not regarded as sound by some because of these Paradoxes.

Can you give relevant pointers? I'm curious because while I do know a couple of arguments for the inconsistency of ZFC, none of these are related to the Banach–Tarski paradox or similar nonintuitive results.

Also I'd like to stress that ZFC and ZF are exactly as consistent: If ZF is consistent, then so is ZFC (and vice versa). This meta-result is proven in a very weak finitary logical meta-system ("PRA"), hence can be trusted even if one is wary of set-theoretic infinities. The keyword is "Gödel's constructible hierarchy".

In this line, there are even more astonishing meta-theorems, all provable in PRA:

* From any ZFC-proof of a purely number-theoretical statement (a statement which refers only to natural numbers), any usage of the axiom of choice can be mechanically eliminated. That is, any ZFC-proof of such a result can be transformed into a ZF-proof.

* From any ZFC-proof of a statement of the form "for all numbers n, there exists a number m such that ...", where in "..." no more quantifiers ("for all", "there exist") appear, any usage of the law of excluded middle ("any statement is either true or not") can be mechanically eliminated. That is, any such ZFC-proof can be transformed into a proof in IZF ("Intuitionistic Zermelo–Fraenkel"). The keyword is "double negation translation".

These meta-theorems indicate that the axiom of choice and the law of excluded middle can be regarded as "mathematical phantoms". Just as the complex numbers work wonders for us but can be compiled away to pairs of real numbers, these set-theoretic principles promise to work wonders for us and their usage can be compiled away if we wish so.

The construction involves a rotation of an infnitely detailed object in a way which is analogous to Hilbert Hotel. (Rotating it makes it fill empty space)

B-T is Hilbert Hotel plus Axiom of Choice.

Perhaps it is unsurprising, but it remains relevant. In a set theory that allows infinite sets, but does not allow the axiom of choice, you can construct the Hilbert hotel, but not the Banach-Tarski paradox, if I understand correctly.

On the other hand, to me it sounds like the distinction may also come from the difference between countable infinities (which Hilbert's Grand Hotel is limited to), and uncountable infinities (which BT depends on).