×

Open induction in a bounded arithmetic for \(\mathrm{TC}^{0}\). (English) Zbl 1371.03090

Summary: The elementary arithmetic operations \(+\), \(\cdot\), \(\leq\) on integers are well-known to be computable in the weak complexity class \(\mathrm{TC}^{0}\), and it is a basic question what properties of these operations can be proved using only \(\mathrm{TC}^{0}\)-computable objects, i.e., in a theory of bounded arithmetic corresponding to \(\mathrm{TC}^{0}\). We will show that the theory \(\mathrm{VTC}^{0}\) extended with an axiom postulating the totality of iterated multiplication (which is computable in \(\mathrm{TC}^{0}\)) proves induction for quantifier-free formulas in the language \({\langle{+,\cdot,\leq}\rangle}\) (IOpen), and more generally, minimization for \({\Sigma_{0}^{b}}\) formulas in the language of Buss’s \(S_2\).

MSC:

03F20 Complexity of proofs
03F30 First-order arithmetic and fragments
12Y05 Computational aspects of field theory and polynomials (MSC2010)
12J10 Valued fields
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Barrington D.A.M., Immerman N., Straubing H.: On uniformity within NC1. J. Comput. Syst. Sci. 41(3), 274-306 (1990) · Zbl 0719.68023
[2] Basu S., Pollack R., Roy M.-F.: Algorithms in Real Algebraic Geometry. Springer, Berlin (2006) · Zbl 1102.14041
[3] Beame P.W., Cook S.A., Hoover H.J.: Log depth circuits for division and related problems. SIAM J. Comput. 15(4), 994-1003 (1986) · Zbl 0619.68047
[4] Boughattas S., Kołodziejczyk L.A.: The strength of sharply bounded induction requires MSP. Ann. Pure Appl. Logic 161(4), 504-510 (2010) · Zbl 1223.03045
[5] Buss, S.R.: Bounded Arithmetic. Bibliopolis, Naples (1986). Revision of 1985 Princeton University Ph.D. thesis · Zbl 0801.68052
[6] Chandra A.K., Stockmeyer L., Vishkin U.: Constant depth reducibility. SIAM J. Comput. 13(2), 423-439 (1984) · Zbl 0538.68038
[7] Chiu A.Y., Davida G.I., Litow B.E.: Division in logspace-uniform NC1. RAIRO Theor. Inform. Appl. 35(3), 259-275 (2001) · Zbl 1014.68062
[8] Cook S.A., Nguyen P.: Logical Foundations of Proof Complexity. Perspectives in Logic. Cambridge University Press, New York (2010) · Zbl 1206.03051
[9] Engler A.J., Prestel A.: Valued fields. Springer Monographs in Mathematics. Springer, Berlin (2005) · Zbl 1128.12009
[10] Hajnal A., Maass W., Pudlák P., Szegedy M., Turán G.: Threshold circuits of bounded depth. J. Comput. Syst. Sci. 46(2), 129-154 (1993) · Zbl 0801.68052
[11] Hesse W., Allender E., Barrington D.A.M.: Uniform constant-depth threshold circuits for division and iterated multiplication. J. Comput. Syst. Sci. 65(4), 695-716 (2002) · Zbl 1059.68044
[12] Immerman N.: Expressibility and parallel complexity. SIAM J. Comput. 18(3), 625-638 (1989) · Zbl 0688.68038
[13] Jeřábek E.: The strength of sharply bounded induction. Math. Logic Q. 52(6), 613-624 (2006) · Zbl 1109.03067
[14] Jeřábek E.: On theories of bounded arithmetic for NC1. Ann. Pure Appl. Logic 162(4), 322-340 (2011) · Zbl 1239.03035
[15] Jeřábek E.: Root finding with threshold circuits. Theor. Comput. Sci. 462, 59-69 (2012) · Zbl 1282.68116
[16] Johannsen, J.: On the weakness of sharply bounded polynomial induction. In: Gottlob, G. Leitsch, A., Mundici, D. (eds.) Computational logic and proof theory. Proceedings of Kurt Gödel Colloquium ’93, Lecture Notes in Computer Science, vol. 713, pp. 223-230. Springer (1993) · Zbl 0793.68064
[17] Johannsen, J.: Weak bounded arithmetic, the Diffie-Hellman problem, and Constable’s class K. In: Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, pp. 268-274 (1999)
[18] Johannsen, J., Pollett, C.: On proofs about threshold circuits and counting hierarchies (extended abstract). In: Proceedings of the 13th Annual IEEE Symposium on Hogic in Computer Science, pp. 444-452 (1998)
[19] Johannsen, J., Pollett, C.: On the \[{\Delta^b_1}\] Δ1b-bit-comprehension rule. In: Buss, S.R., Hájek, P., Pudlák, P. (eds.) Logic Colloquium ’98: Proceedings of the 1998 ASL European Summer Meeting held in Prague, Czech Republic, pp. 262-280. ASL (2000) · Zbl 0988.03088
[20] Kołodziejczyk L.A.: Independence results for variants of sharply bounded induction. Ann. Pure Appl. Logic 162(12), 981-990 (2011) · Zbl 1230.03091
[21] Krajíček, J.: Bounded Arithmetic, Propositional Logic, and Complexity Theory, Encyclopedia of Mathematics and Its Applications, vol. 60. Cambridge University Press, Cambridge (1995) · Zbl 0835.03025
[22] Maciel A., Thérien D.: Efficient threshold circuits for power series. Inf. Comput. 152(1), 62-73 (1999) · Zbl 1009.68061
[23] Mantzivis S.G.: Circuits in bounded arithmetic part I. Ann. Math. Artif. Intell. 6(1-3), 127-156 (1991) · Zbl 0865.03046
[24] Nguyen, P., Cook, S.A.: Theories for TC0 and other small complexity classes. Log. Methods Comput. Sci. 2(1) (2006). Paper no. 3 · Zbl 1126.68048
[25] Parberry I., Schnitger G.: Parallel computation with threshold functions. J. Comput. Syst. Sci. 36(3), 278-302 (1988) · Zbl 0652.68064
[26] Reif J.H.: Logarithmic depth circuits for algebraic functions. SIAM J. Comput. 15(1), 231-242 (1986) · Zbl 0611.68014
[27] Reif J.H., Tate S.R.: On threshold circuits and polynomial computation. SIAM J. Comput. 21(5), 896-908 (1992) · Zbl 0765.68057
[28] Scott, D.: On completing ordered fields. In: Luxemburg, W.A.J. (ed.) Applications of Model Theory to Algebra, Analysis, and Probability, pp. 274-278. Holt, Rinehart and Winston, New York (1969) · Zbl 0188.32202
[29] Shepherdson J.C.: A nonstandard model for a free variable fragment of number theory. Bull. Acad. Pol. Sci. Sér. Sci. Math. Astron. Phys. 12(2), 79-86 (1964) · Zbl 0132.24701
[30] Takeuti, G.: Sharply bounded arithmetic and the function a ∸ 1. In: Sieg, W. (ed.) Hogic and Computation, Proceedings of a Workshop held at Carnegie Mellon University, 30 June-2 July 1987, Contemporary Mathematics, vol. 106, pp. 281-288. American Mathematical Society (1990) · Zbl 0611.68014
[31] Vámos P.: Decomposition problems for modules over valuation domains. J. Lond. Math. Soc. 2(1), 10-26 (1990) · Zbl 0736.13013
[32] Wilkie, A.J.: Some results and problems on weak systems of arithmetic. In: Macintyre, A. (ed.) Logic Colloquium ’77, pp. 285-296. North-Holland (1978) · Zbl 0449.03076
[33] Zambella D.: Notes on polynomially bounded arithmetic. J. Symb. Logic 61(3), 942-966 (1996) · Zbl 0864.03039
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.