[FOM] AI-completeness

[joeshipman@aol.com]

Very clever! At first, one might think this game was trivial to play 
because an optimal strategy for each player would be to add an axiom 
saying that the current set of axioms is consistent. But it is more 
interesting because of the possibility of bluffing -- you can add an 
axiom you have constructed to be inconsistent, but that you think your 
opponent will not be able to detect the inconsistency of, then pounce 
on him if he lazily asserts that your axiom is consistent.

The game is hard even if the new axioms are required to be delta^0_0 
statements. Suppose the starting set of axioms is PA. My first move is

Axiom G: "PA has no proofs of 0=1 of size smaller than 10^(10^100)."

If you are simply allowed to "show redundancy" by proving it in a 
higher system, you can easily win, but then there will be arguments 
about the validity of the higher system that you use, so it looks like 
you must show that my most recently added axiom is redundant by 
exhibiting a formal derivation of it from the earlier axioms, and you 
won't be able to.

Again, it seems that one can only win by bluffing; but actually my move 
was already worse than a bluff--being delta^0_0, it MUST be either 
redundant or inconsistent! However, you can prove feasibly in PA that 
either G was redundant or G was inconsistent, which maybe should be 
good enough  to count as victory.

-- JS


>Take some reasonably well-known formal system.  Players take turns
>adding additional axioms. Before his turn, a player may challenge his
>opponent's last move.  That player wins if he shows that the 
opponent's
>most recently added axiom is redundant, or that the current set of 
axioms
>is inconsistent.
>
>-- hendrik
________________________________________________________________________
AOL now offers free email to everyone.  Find out more about what's free 
from AOL at AOL.com.