[FOM] Wittgenstein Inspired Skepticism

[Thomas Klimpel]

Tim Chow wrote:
> I would instead say that ZFC is what is commonly cited when people are *not*
> in "retreat mode."  Retreat mode is triggered if someone questions the axiom
> of choice, or the reality of infinite sets, or the consistency of PA, or the
> existence of arbitrarily large integers.  Then the typical response is,
> "Fine, be a skeptic if you must, but at least we all agree that these
> theorems follow from these axioms according to these rules of inference."

If the skeptic just tries to be difficult, then I see no reason to
enter into "retreat mode" at all. If he is serious, then the challenge
is to answer his specific concern. In this context, it can happen
indeed that an argument involving "... these theorems follow from
these axioms according to these rules of inference." is appropriate,
and ZFC enters only in the "from these axioms" part. Let me repeat my
complete answer
(http://philosophy.stackexchange.com/questions/7643/what-is-the-proper-role-of-foundations-in-rigorous-mathematics-paused/7647#7647)
to such a specific concern here, to see how much I actually retreated
and how heavily I had to rely on Turing machines:

"""
goblin wrote:
> This raises an interesting question. If foundational theories like ZFC are not
> the right place to formalize definitions like group, field, topological space, etc.,
> then what is the proper role of foundations in rigorous mathematics?

If you invent an algorithm, the empirical approach to prove that you
have not left out any important detail is to implement it in an actual
programming language. Depending on the used programming language, this
can look quite ugly and contingent. However, the deeper problem is
that even if your program compiles and works correctly for all
problems on which you test it, what does this prove? Well, it forces
you to lay down all your cards, so if later something turns out to
miss, you can't just claim that it had been there all along and was
only not understood correctly.

My point here is that even if ZFC should turn out to correspond to an
ugly programming language, it still serves the purpose of a certain
kind of rigor good enough, even if this kind of rigor might not be the
last word regarding rigor.

Conclusion: Rigor in mathematics has something to do with playing with
open cards and not withholding boring details.
"""

I certainly did not give up ZFC, I only admitted that it might turn
out to be ugly, but nevertheless would still serve its purpose. Turing
machines implicitly entered the picture as a way of forcing you to lay
down all your cards, such that you can at least be proven wrong (if it
should turn out that you are wrong).


Even so Hilbert had hoped that some finitistic means (like Turing
machines?) could serve as a safe point of retreat, it wouldn't have
worked even without Gödel's proof that it fails completely. (Brouwer
tried to explain why, but I don't want to discuss that.) So
mathematicians know that they cannot really retreat to Turing
machines, otherwise they will be expelled from Cantor's paradise. But
if somebody questions the axiom of choice, we know that we can safely
retreat to ZF, and later return to ZFC. If Voevodsky questions the
consistency of PA
(http://m-phi.blogspot.de/2011/05/voevodsky-consistency-of-pa-is-open.html),
then he already rejects ZFC. He doesn't reject it because he is trying
to be difficult, but because he thinks univalent foundations and proof
assistants are an attractive alternative to ZFC as foundations of
mathematics. This gets us into deep water, but I believe an
appropriate answer to his concerns might be provided by the
Gödel-Gentzen translation
(https://en.wikipedia.org/wiki/Double-negation_translation) embedding
classical logic into intuitionistic logic. (Don't nail me on that, my
point here is that one should try to answer the specific concerns of
the skeptic, instead of throwing out the baby with the bathwater by an
inappropriate and ineffective generic retreat.) If N J Wildberger
questions the reality of infinite sets, or the existence of
arbitrarily large integers, then he does this because he objects to
the way we teach mathematics in school and at the undergraduate level.
But even so he is serious, this gets too much into politics to allow a
proper response on a mathematical level.

But speaking of politics, one should be aware of the fact that
Cantor's (philosophy behind) set theory and his insistence that the
only real question was consistency was politically motivated
(http://philosophy.stackexchange.com/questions/4175/cantor-and-infinities/4287#4287)
to prevent abuse of power by established mathematicians like Leopold
Kronecker. (He even founded the "Deutsche Mathematiker Vereinigung"
for that same purpose.) And it is not clear to me how much Alfred
Tarski and John von Neumann played a role in establishing first order
logic + ZFC as the undisputed foundations of mathematics. At least
Tarski had experienced the "power of the establishment" before
(https://en.wikipedia.org/wiki/Tarski's_theorem_about_choice), and
both had the experience of translating work from their own language
into German and later into English. So they knew the value of
established foundations for doing mathematics, as opposed to having
fruitless discussions (which would in the end be decided by the power
of the establishment).

I like to read Frank P. Ramsey, Willard Van Orman Quine or Randall
Holmes. So there is certainly some temptation for me to retreat to
simple type theory or Mac Lane set theory, since I would know better
arguments for defending them than the reference to "the von Neumann
cumulative hierarchy". But that would give up the consensus to use ZFC
as the undisputed foundations of mathematics. Since they are not
sufficiently different from ZFC, this would just not be worth it. The
univalent foundations on the other hand would be sufficiently
different, the question is just whether they will ever become
sufficiently easy to explain. But even if they do, there is no reason
to give up ZFC. Both foundations can coexist without any major
problems.