{"docId":2257,"paperId":2257,"url":"https:\/\/lmcs.episciences.org\/2257","doi":"10.2168\/LMCS-2(1:3)2006","journalName":"Logical Methods in Computer Science","issn":"","eissn":"1860-5974","volume":[{"vid":115,"name":"Volume 2, Issue 1"}],"section":[],"repositoryName":"arXiv","repositoryIdentifier":"cs\/0505013","repositoryVersion":4,"repositoryLink":"https:\/\/arxiv.org\/abs\/cs\/0505013v4","dateSubmitted":"2004-11-30 00:00:00","dateAccepted":null,"datePublished":"2006-03-07 00:00:00","titles":["Theories for TC0 and Other Small Complexity Classes"],"authors":["Nguyen, Phuong","Cook, Stephen"],"abstracts":["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"],"keywords":["Computer Science - Logic in Computer Science","Computer Science - Computational Complexity","F.4.1"]}