Check nearby libraries
Buy this book

We introduce a finitely axiomatizable second-order theory VTC 0 and show that it characterizes precisely the class uniform TC0. It is simply the theory V0 [12] together with the axiom NUMONES, which states the existence of a "counting array" Y for any string X : the ith row of Y contains only the number of 1 bits upto (excluding) bit i of X. First, we introduce the notion of "strong DB1 -definability" for relations in a theory, and use the recursive properties of TC0 relations (rather than functions) to show that TC0 relations are strongly DB1 -definable, and TC0 functions are SB1 -definable in VTC0. Then, we generalize the Witnessing Theorem for V0 [12], and obtain the witnessing theorem for VTC0 from this general result: ∃SB0+ SB1 theorems of VTC0 can be witnessed by TC0 functions (here, SB0+S B1 formulas are those obtained from SB1 formulas using ∧,∨ and bounded number quantifications). Finally, we show that VTC0 is RSUV isomorphic to the first-order theory Db1 -CR, which has been claimed the "minimal" theory for TC0 [20]. This isomorphism shows that VTC0 admits the SB0+D B1 comprehension rule. Hence, in VTC0, strong DB1 -definability and the usual DB1 -definability coincide. It also follows that Db1 - CR = Db1 - CRi, for some i. This answers affirmatively an open question from [20].
Check nearby libraries
Buy this book

Edition | Availability |
---|---|
1 |
aaaa
|
Book Details
Edition Notes
Adviser: Stephen Cook.
Thesis (M.Sc.)--University of Toronto, 2004.
Electronic version licensed for access by U. of T. users.
Source: Masters Abstracts International, Volume: 42-06, page: 2240.
MICR copy on microfiche (1 microfiche).
The Physical Object
Edition Identifiers
Work Identifiers
Community Reviews (0)
January 25, 2010 | Edited by WorkBot | add more information to works |
December 11, 2009 | Created by WorkBot | add works page |