A Third-Order Bounded Arithmetic Theory for PSPACE

We present a novel third-order theory W1 1 of bounded arithmetic suitable for reasoning about PSPACE functions. This theory has the advantages of avoiding the smash function symbol and is otherwise much simpler than previous PSPACE theories. As an example we outline a proof in W1 1 that from any configuration in the game of Hex, at least one player has a winning strategy. We then exhibit a translation of theorems of W1 1 into families of propositional tautologies with polynomial-size proofs in BPLK (a recent propositional proof system for PSPACE and an alternative to G). This translation is clearer and more natural in several respects than the analogous ones for previous PSPACE theories.

• Type: Conference
• Year: 2004
• Where: CSL
• Authors: Alan Skelley
• Keywords: CSL 2004, Propositional Tautologies, PSPACE Functions, Smash Function Symbol