[FOM] Classical/Constructive Arithmetic

[Harvey Friedman]

On 3/21/06 10:28 PM, "Bill Taylor" <W.Taylor at math.canterbury.ac.nz> wrote:

>> Examples where the known proof is nonconstructive, and where one can give
>> a constructive proof, but all known constructive proofs are grotesque
> 
> Examples abound in game theory.  e.g. That Hex has a first-player win.
>

I'm afraid I have trouble with this.

THEOREM. Any Pi02 theorem of PA that has a nice proof, also has a nice proof
in HA. 

Proof: By the so called Friedman A-translation. Godel was the first person
to prove this with "nice" deleted in both places. QED

So in order to give an example in game theory, the example has to

1. NOT be Pi02, OR
2. Pi02, but there is not proof in PA.

What examples do you have in mind?

Harvey Friedman