Theories for TC0 and Other Small Complexity Classes

TL;DR

This paper develops a minimal two-sorted logical theory VTC^0 for the complexity class TC^0, establishing its formal properties and showing its equivalence to a known single-sorted theory, thereby advancing formal understanding of small complexity classes.

Contribution

It introduces a finitely axiomatizable two-sorted theory VTC^0 for TC^0 and proves its isomorphism to an existing single-sorted theory, clarifying the formal foundations of TC^0.

Findings

VTC^0 captures all provably-total functions of TC^0

VTC^0 is isomorphic to Johannsen and Pollet's single-sorted theory

Formalization of binary multiplication via bit-counting functions

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 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.