[FOM] Classical/Constructive Arithmetic
Harvey Friedman
friedman at math.ohio-state.edu
Wed Mar 22 01:01:25 EST 2006
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
More information about the FOM
mailing list