> In what sense can a finite set exist and be finite when it is unfindable, unverifiable, and has unboundable size?
In the same sense that we could say that every computer program must either eventually terminate or never terminate without most people thinking there's a major philosophical problem here.
And by the way, the very same question can be (and has been) levelled at constructivism: in what sense does a result that would take longer than the lifetime of the universe to compute exist, as it is unfindable and unverifiable?
Look, I think that it is interesting to work with constructive axioms, but I don't think that humans philosophically reject non-constructive results. It's one thing to say that we can learn interesting things in constructive mathematics and another to say there's a fundamental problem with non-constructive mathematics.
> But formalism leads to having to accept conclusions that some of us don't like.
At least in Hilbert's sense, I don't think formalism says quite what you claim it says. He says that some mathematical statements or results apply to things we can see in the world and could be assigned meaning through, say, correspondence to physics. But other mathematical statements don't say anything about the physical world, and therefore the question of their "actual meaning" is not reason to reject them as long as they don't lead to "real" results (in the first class of statements) that contradict physical reality.
Formalism, therefore, doesn't require you to accept or reject any particular meaning that the second class of statements may or may not have. If a statement in the second class says that some set exists, you don't have to assign that "existence" any meaning beyond the formula itself.
In the same sense that we could say that every computer program must either eventually terminate or never terminate without most people thinking there's a major philosophical problem here.
And by the way, the very same question can be (and has been) levelled at constructivism: in what sense does a result that would take longer than the lifetime of the universe to compute exist, as it is unfindable and unverifiable?
Look, I think that it is interesting to work with constructive axioms, but I don't think that humans philosophically reject non-constructive results. It's one thing to say that we can learn interesting things in constructive mathematics and another to say there's a fundamental problem with non-constructive mathematics.
> But formalism leads to having to accept conclusions that some of us don't like.
At least in Hilbert's sense, I don't think formalism says quite what you claim it says. He says that some mathematical statements or results apply to things we can see in the world and could be assigned meaning through, say, correspondence to physics. But other mathematical statements don't say anything about the physical world, and therefore the question of their "actual meaning" is not reason to reject them as long as they don't lead to "real" results (in the first class of statements) that contradict physical reality.
Formalism, therefore, doesn't require you to accept or reject any particular meaning that the second class of statements may or may not have. If a statement in the second class says that some set exists, you don't have to assign that "existence" any meaning beyond the formula itself.