FOM: A question concerning HA*

[Robert M. Solovay]

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.]