# [FOM] AI-completeness

joeshipman@aol.com joeshipman at aol.com
Tue May 1 18:49:04 EDT 2007

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