The Universe (matthias) (Timothy Y. Chow)

[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