The Universe (matthias) (Timothy Y. Chow) (Timothy Y. Chow)
Øystein Linnebo
linnebo at gmail.com
Mon Jul 20 04:08:51 EDT 2020
First, concerning the strict potentialist's view of first-order arithmetic:
On the "good first approximation" that Tim mentions, this potentialist
accepts a sentence A of first-order arithmetic iff A has a realizer.
Footnote 31 of the article provides references to precise results
concerning which such sentences have realizers. Unsurprisingly, we get
somewhat different answers from classical and intuitionistic arithmetic.
Tim states the answer from classical arithmetic. By contrast, according to
intuitionistic arithmetic fewer first-order sentences have realizers;
indeed, Troelstra shows that according to a slight extension of Heyting
Arithmetic plus ECT_0, any formula A is equivalent to the statement that A
has a realizer. Again, see fn. 31 for details and references.
This situation raises the question of who the strict potentialist should
listen to in order to answer the question of which first-order sentences
have realizers. Since the logic of the theory in the object language is
anyway going to be intuitionistic, Shapiro and I think it would be most
coherent to let *Heyting *Arithmetic answer this question (with the answer
stated above).
Second, concerning the (strict or liberal) potentialist's view of
second-order arithmetic:
Yes, here there is a need for more work. Much will depend on whether the
classes of numbers are understood combinatorially (i.e. as completely
arbitrary collections of antecedently available objects) or in some other
way (e.g. as logical classes, perhaps developed in some predicative way).
In the former case, there will (as explained in my earlier FOM postings)
only be finite classes. This means that the classes will be governed by
so-called "weak second-order logic", where the second-order variables are
stipulated to range over all and only finite collections from the
first-order domain (see Shapiro 1991, *Foundations without
Foundationalism*, Chapter
9). In the latter case, the answer will be some sort of predicative theory
of classes of natural numbers (which, as Tim requests, can very likely be
stated without any use of modal resources). But the details remain to be
worked out and will depend on one's choice of a potentialist explication of
predicativism relative to the naturals. Shapiro and I are working on this
-- and encourage others to do so as well.
Oystein
> Date: Sat, 18 Jul 2020 14:13:20 -0400 (EDT)
> From: "Timothy Y. Chow" <tchow at math.princeton.edu>
> To: fom at cs.nyu.edu
> Subject: Re: The Universe (matthias) (Timothy Y. Chow)
> Message-ID: <alpine.LRH.2.21.2007181336550.12844 at math.princeton.edu>
> Content-Type: text/plain; charset=US-ASCII; format=flowed
>
> 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/20200720/c422c4cf/attachment.html>
More information about the FOM
mailing list