[FOM] AI-completeness

[hendrik@topoi.pooq.com]

On Sun, Apr 29, 2007 at 11:40:32PM -0400, Timothy Y. Chow wrote:
> 
> This might seem surprising because ostensibly chess and go belong to 
> higher computational complexity classes than theorem-proving (PSPACE and 
> NP respectively, once you impose some kind of size bound).  Can someone 
> disprove *** by concocting a game that is not so hard to play but that is 
> hard to master---as hard as producing first-rate, original mathematics?  

Let's have a try at that.

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