Απ: The Universe (matthias) (Timothy Y. Chow)

[Kapantais Doukas]

Dear list members,

Thank you for this stimulating exchange.
I will come back with specific points on the Linnebo & Shapiro paper.
An interesting related topic is the distinction between König's lemma and its intuitionistic proxy, the fan theorem. Also related is Van Dalen's
https://philpapers.org/rec/VANHCI
[https://philpapers.org/assets/raw/philpeople250.png]<https://philpapers.org/rec/VANHCI>
Dirk van Dalen, How connected is the intuitionistic continuum? - PhilPapers<https://philpapers.org/rec/VANHCI>
philpapers.org
Best,
Doukas Kapantais
________________________________
Από: FOM <fom-bounces at cs.nyu.edu> εκ μέρους του Timothy Y. Chow <tchow at math.princeton.edu>
Στάλθηκε: Σάββατο, 18 Ιουλίου 2020 9:13 μμ
Προς: fom at cs.nyu.edu <fom at cs.nyu.edu>
Θέμα: Re: The Universe (matthias) (Timothy Y. Chow)

Oystein Linnebo wrote:
> Yes, the strict potentialist regards all statements of first-order
> arithmetic as meaningful. And yes, on the analysis Shapiro and I
> provide, the strict potentialist can prove every theorem of Heyting
> arithmetic. For details, see Theorem 3 and footnote 31.
>
> As for second-order arithmetic, I claimed that the potentialist (whether
> liberal or strict) is not "entitled" to full second-order arithmetic --
> even if he accepts the combinatorial conception of classes (as
> completely arbitrary collections of antecedently available objects).
> This isn't because some second-order statements are deemed meaningless.
> Rather, it is because all the classes will be finite. After all, at any
> stage, there are only finitely many natural numbers available to serve
> as members of a class, understood combinatorially.

Thanks for these clarifications.  I looked at your paper again, still
skimming, but reading some parts more carefully.

In Section 9, you say that "a good first approximation" to which
arithmetic statements the strict potentialist accepts is given by "the
realizability interpretation."  If I understand correctly, then under this
"good first approximation," the strict potentialist accepts a statement A
of first-order arithmetic if and only if Heyting arithmetic plus ECT_0
plus Markov's principle proves (intuitionistically) ~~A.  Here Markov's
principle is that if a given formula B is decidable, then ~~ExB -> ExB,
and ECT_0 is some kind of "extended Church's thesis" (defined in
Troelstra's article on "Realizability" in the Handbook of Proof Theory).
This is a very sharp statement and has the advantage of being
understandable without having to follow the detour into modal logic that
you use to justify this conclusion.

For second-order arithmetic, the situation is less clear, at least to me.
It would be interesting if one could precisely describe, without any
reference to modal logic, a subsystem of second-order arithmetic (in the
sense of Simpson's book) that captures what the potentialist (either
strict or liberal) accepts.  If I understand correctly, this kind of
analysis of second-order arithmetic lies beyond the scope of your article.
But, failing a complete characterization, it would still be interesting to
give examples of specific statements that go beyond first-order arithmetic
and that the potentialist can or cannot prove.

Tim
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20200719/e90ebd73/attachment-0001.html>