| |
VOLUME 2, ISSUE 1, PAPER 3
|
Theories for TC0 and Other Small Complexity Classes
|
©Phuong Nguyen, University of Toronto
©Stephen Cook, University of Toronto
|
Abstract
We present a general method for introducing finitely axiomatizable "minimal"
two-sorted theories for various subclasses of P (problems solvable in
polynomial time). The two sorts are natural numbers and finite sets of natural
numbers. The latter are essentially the finite binary strings, which provide a
natural domain for defining the functions and sets in small complexity classes.
We concentrate on the complexity class TC0, whose problems
are defined by uniform polynomial-size families of bounded-depth Boolean
circuits with majority gates. We present an elegant theory
VTC0 in which the provably-total functions are those
associated with TC0, and then prove that
VTC0 is "isomorphic" to a different-looking single-sorted
theory introduced by Johannsen and Pollet. The most technical part of the
isomorphism proof is defining binary number multiplication in terms a
bit-counting function, and showing how to formalize the proofs of its algebraic
properties.
|
Publication date: March 7, 2006
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-2(1:3)2006
Hit Counts: 6559 |
 Creative Commons | |
