10.2168/LMCS-2(1:3)2006
https://lmcs.episciences.org/2257
Nguyen, Phuong
Phuong
Nguyen
Cook, Stephen
Stephen
Cook
Theories for TC0 and Other Small Complexity Classes
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 TC^0, whose problems are defined by
uniform polynomial-size families of bounded-depth Boolean circuits with
majority gates. We present an elegant theory VTC^0 in which the provably-total
functions are those associated with TC^0, and then prove that VTC^0 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.
Comment: 40 pages, Logical Methods in Computer Science
episciences.org
Computer Science - Logic in Computer Science
Computer Science - Computational Complexity
F.4.1
arXiv.org - Assumed non-exclusive license to distribute
2023-03-27
2006-03-07
2006-03-07
eng
journal article
arXiv:cs/0505013
10.48550/arXiv.cs/0505013
1860-5974
https://lmcs.episciences.org/2257/pdf
VoR
application/pdf
Logical Methods in Computer Science
Volume 2, Issue 1
Researchers
Students