FOM: Re: A question concerning HA*

[Harvey Friedman]

Reply to Solovy 6/29/00 6:49PM

>In his posting of June 28th, 2000 entitled "Re: FOM: Effective Bounds in
>Core Mathematics", Harvey writes:
>
>As a constructivist, one can state the thesis: a sentence of HA is
>provable in HA* if and only if it is true. But it is well known that this
>is refutable, constructively.
>
>
>	How does the refutation go? [It's not even clear to me that the
>assertion has a clear constructive meaning.]

We argue constructively. By a recursive well ordering, we mean a Turing
algorithm which defines a linear ordering of an initial segment of omega
(proper or improper), where any progressive subset of its field is all of
its field. This makes sense in the standard constructive (intuitionistic)
theories of second order arithmetic, or even in standard constructive
(intuitionistic) theories of inductive definitions.

Assume the thesis is true. Let LEM(Pi-0-1) be the law of excluded middle
for Pi-0-1 sentences. By well known constructive arguments, LEM(Pi-0-1) is
not provable in HA* and notLEM(Pi-0-1) is not provable in HA*. Hence
notLEM(Pi-0-1) and notnotLEM(Pi-0-1). Contradiction.