Hostname: page-component-78c5997874-94fs2 Total loading time: 0 Render date: 2024-11-16T16:10:59.421Z Has data issue: false hasContentIssue false
  • English
  • Français

Witnessing functions in bounded arithmetic and search problems

Published online by Cambridge University Press:  12 March 2014

Mario Chiari  and
Jan Krajíček
Mario Chiari
Affiliation:
Mathematical Institute, Academy of Sciences, Žitná 25, Prague, 115 67, Czech Republic E-mail: [email protected]
Jan Krajíček
Affiliation:
Mathematical Institute and Institute of Computer Science, Academy of Sciences, Žitná 25, Prague, 115 67, Czech Republic E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We investigate the possibility to characterize (multi)functions that are -definable with small i (i = 1, 2, 3) in fragments of bounded arithmetic T2 in terms of natural search problems defined over polynomial-time structures. We obtain the following results:

(1) A reformulation of known characterizations of (multi)functions that are and -definable in the theories and .

(2) New characterizations of (multi)functions that are and -definable in the theory .

(3) A new non-conservation result: the theory is not -conservative over the theory .

To prove that the theory is not -conservative over the theory , we present two examples of a -principle separating the two theories:

(a) the weak pigeonhole principle WPHP(a2, f, g) formalizing that no function f is a bijection between a2 and a with the inverse g,

(b) the iteration principle Iter(a, R, f) formalizing that no function f defined on a strict partial order ({0,…, a}, R) can have increasing iterates.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 63 , Issue 3 , September 1998 , pp. 1095 - 1115
Copyright
Copyright © Association for Symbolic Logic 1998

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Ajtai, M., formulae on finite structures, Annals of Pure and Applied Logic, vol. 24 (1983), pp. 1–48.CrossRefGoogle Scholar
[2]Buss, S. R., Bounded arithmetic, Bibliopolis, Naples, 1986.Google Scholar
[3]Buss, S. R., The propositional pigeonhole principle has polynomial size Frege proofs, this Journal, vol. 52 (1987), pp. 916–927.Google Scholar
[4]Buss, S. R., Axiomatizations and conservation results for fragments of bounded arithmetic, Logic and computation, Contemporary Mathematics, no. 106, American Mathematical Society, Providence, 1990, pp. 57–84.CrossRefGoogle Scholar
[5]Buss, S. R. and Krajíček, J., An application of boolean complexity to separation problems in bounded arithmetic, Proceedings of the London Mathematical Society, vol. 69 (1994), no. 3, pp. 1–27.CrossRefGoogle Scholar
[6]Buss, S. R., Krajíček, J., and Takeuti, G., On provably total functions in bounded arithmetic theories , and , Arithmetic, proof theory and computational complexity (Cloteand, P.Krajíček, J., editors), Oxford University Press, Oxford, 1993, pp, 116–161.Google Scholar
[7]Chiari, M. and Krajíček, J., Lifting independence results in bounded arithmetic, to appear, 1995.Google Scholar
[8]Cook, S. A., The complexity of theorem proving procedures, Proceedings of the 3rd annual ACM symposium on theory of computing, ACM Press, 1971, pp. 151–158.Google Scholar
[9]Cook, S. A., Feasibly constructive proofs and the propositional calculus, Proceedings of the 7th annual ACM symposium on theory of computing, ACM Press, 1975, pp. 83–97.Google Scholar
[10]Cook, S. A. and Reckhow, A. R., The relative efficiency of propositional proof systems, this Journal, vol. 44 (1979), no. 1, pp. 36–50.Google Scholar
[11]Furst, M., Saxe, J. B., and Sipser, M., Parity, circuits and the polynomial-time hierarchy, Mathematical Systems Theory, vol. 17 (1984), pp. 13–27.CrossRefGoogle Scholar
[12]Hastad, J., Almost optimal lower bounds for small depth circuits, Randomness and computation (Micali, S., editor), Series in Advanced Comp. Res., no. 5, JAI Press, 1989, pp. 143–170.Google Scholar
[13]Krajíček, J., No counter-example interpretation and interactive computation, Logic from computer science (Moschovakis, Y. N., editor), Mathematical Sciences Research Institute Publication, no. 21, Springer-Verlag, New York, 1992, Proceedings of a Workshop held November 13–17, 1989, in Berkeley, pp. 287–293.CrossRefGoogle Scholar
[14]Krajíček, J., Fragments of bounded arithmetic and bounded query classes, Transactions of the American Mathematical Society, vol. 338 (1993), no. 2, pp. 587–598.CrossRefGoogle Scholar
[15]Krajíček, J., Bounded arithmetic, propositional logic, and complexity theory, Encyclopedia of Mathematics and Its Applications, vol. 60, Cambridge University Press, Cambridge-New York-Melbourne, 1995.CrossRefGoogle Scholar
[16]Krajíček, J. and Pudlák, P., Quantified propositional calculi and fragments of bounded arithmetic, Zeitschrift für Mathematikal Logik und Grundlagen der Mathematik, vol. 36 (1990), pp. 29–46.CrossRefGoogle Scholar
[17]Krajíček, J., Pudlák, P., and Takeuti, G., Bounded arithmetic and the polynomial hierarchy, Annals of Pure and Applied Logic, vol. 52 (1991), pp. 143–153.CrossRefGoogle Scholar
[18]Krajíček, J., Pudlák, P., and Woods, A., Exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle, Random Structures and Algorithms, vol. 7 (1995), no. 1, pp. 15–39.CrossRefGoogle Scholar
[19]Papadimitriou, C. H., On graph-theoretic lemmata and complexity classes (extended abstract), Proceedings of the 31st IEEE symposium on foundations of computer science, vol. II, IEEE Computer Society, 1990, pp. 794–801.Google Scholar
[20]Papadimitriou, C. H. and Yannakakis, M., Optimization, approximation and complexity classes, 20th annual ACM symposium on theory of computing, ACM Press, 1988, pp. 229–234.Google Scholar
[21]Parikh, R., Existence and feasibility in arithmetic, this Journal, vol. 36 (1971), pp. 494–508.Google Scholar
[22]Paris, J. and Wilkie, A. J., Counting problems in bounded arithmetic, Methods in mathematical logic, Lecture Notes in Mathematics, no. 1130, Springer-Verlag, 1985, pp. 317–340.CrossRefGoogle Scholar
[23]Paris, J. and Wilkie, A. J., On the scheme of induction for bounded arithmetic formulas, Annals of Pure and Applied Logic, vol. 35 (1987), pp. 261–302.Google Scholar
[24]Paris, J. B., Wilkie, A. J., and Woods, A. R., Provability of the pigeonhole principle and the existence of infinitely many primes, this Journal, vol. 53 (1988), pp. 1235–1244.Google Scholar
[25]Pitassi, T., Beame, P., and Impagliazzo, R., Exponential lower bounds for the pigeonhole principle, Computational Complexity, vol. 3 (1993), pp. 97–140.CrossRefGoogle Scholar
[26]Pudlák, P., Some relations between subsystems of arithmetic and the complexity of computations, Logic from computer science (Moschovakis, Y. N., editor), Mathematical Sciences Research Institute Publication, no. 21, Springer-Verlag, 1992, Proceedings of a Workshop held November 13–17, 1989, in Berkeley, pp. 499–519.CrossRefGoogle Scholar
[27]Riis, S., Making infinite structures finite in models of second order bounded arithmetic, Arithmetic, proof theory and computational complexity (Clote, P. and Krajíček, J., editors), Oxford University Press, Oxford, 1993, pp. 289–319.Google Scholar
[28]Smullyan, R., Theory of formal systems, Annals of Mathematical Studies, no. 47, Princeton University Press, Princeton, 1961.CrossRefGoogle Scholar
[29]Takeuti, G., RSUV isomorphism, Arithmetic, proof theory and computational complexity (Clote, P. and Krajiček, J., editors), Oxford University Press, Oxford, 1993, pp. 364–386.CrossRefGoogle Scholar
[30]Yao, Y., Separating the polynomial-time hierarchy by oracles, Proceedings of the 26th annual IEEE symposium on foundations of computer science, 1985, pp. 1–10.Google Scholar