Hostname: page-component-78c5997874-xbtfd Total loading time: 0 Render date: 2024-11-16T01:21:38.515Z Has data issue: false hasContentIssue false
  • English
  • Français

INCOMPLETENESS IN THE FINITE DOMAIN

Published online by Cambridge University Press:  15 February 2018

PAVEL PUDLÁK
PAVEL PUDLÁK*
Affiliation:
INSTITUTE OF MATHEMATICS CZECH ACEDEMY OF SCIENCES PRAGUE, CZECH REPUBLICE-mail:[email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

Motivated by the problem of finding finite versions of classical incompleteness theorems, we present some conjectures that go beyond NP ≠ coNP. These conjectures formally connect computational complexity with the difficulty of proving some sentences, which means that high computational complexity of a problem associated with a sentence implies that the sentence is not provable in a weak theory, or requires a long proof. Another reason for putting forward these conjectures is that some results in proof complexity seem to be special cases of such general statements and we want to formalize and fully understand these statements. Roughly speaking, we are trying to connect syntactic complexity, by which we mean the complexity of sentences and strengths of the theories in which they are provable, with the semantic concept of complexity of the computational problems represented by these sentences.

We have introduced the most fundamental conjectures in our earlier works [27, 33–35]. Our aim in this article is to present them in a more systematic way, along with several new conjectures, and prove new connections between them and some other statements studied before.

Keywords

03F2003D1568Q15finite consistencypropositional proof systemsdisjoint NP-setssearch problems
Type
Articles
Information
Bulletin of Symbolic Logic , Volume 23 , Issue 4 , December 2017 , pp. 405 - 441
Copyright
Copyright © The Association for Symbolic Logic 2017 

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

Beckmann, A. and Buss, S. R., Polynomial local search in the polynomial hierarchy and witnessing in fragments of bounded arithmetic. Journal of Mathematical Logic, vol. 9 (2009), no. 1, pp. 103–138.Google Scholar
Beckmann, A. and Buss, S. R., Characterizing definable search problems in bounded arithmetic via proof notations, Ways of Proof Theory (Schindler, R., editor), Ontos Series in Mathematical Logic, Walter de Gruyter GmbH, Berlin, 2010, pp. 65–134.Google Scholar
Beckmann, A. and Buss, S. R., Improved witnessing and local improvement principles for second-order bounded arithmetic. ACM Transactions on Computational Logic, vol. 15 (2014), no. 1, Article 2.Google Scholar
Beckmann, A., Pudlák, P., and Thapen, N., Parity games and propositional proofs. ACM Transactions on Computational Logic, vol 15 (2014), no. 2, Article 17.Google Scholar
Beyersdorff, O., Köbler, J., and Messner, J., Nondeterministic functions and the existence of optimal proof systems. Theoretical Computer Science, vol. 410 (2009), pp. 3839–3855.Google Scholar
Buss, S. R., Kołodziejczyk, L., and Thapen, N., Fragments of approximate counting. Journal of Symbolic Logic, vol. 79 (2014), no. 2, pp. 496–525.Google Scholar
Buss, S. R., Bounded Arithmetic, Bibliopolis, Naples, 1986.Google Scholar
Buss, S. R., An introduction to proof theory, Handbook of Proof Theory (Buss, S. R., editor), Elsevier, Amsterdam, 1998, pp. 1–78.Google Scholar
Buss, S. R. and Mints, G., The complexity of the disjunction and existence properties in intuitionistic logic. Annals of Pure and Applied Logic, vol. 99 (1999), pp. 93–104.CrossRefGoogle Scholar
Buss, S. and Pudlák, P., On the computational content of intuitionistic propositional proofs. Annals of Pure and Applied Logic, vol. 109 (2001), pp. 49–64.Google Scholar
Cook, S. A., Feasibly constructive proofs and the propositional calculus, Proceedings of the Seventh Annual ACM Symposium on Theory of Computing, ACM, New York, 1975, pp. 83–97.Google Scholar
Cook, S. A. and Reckhow, R. A., The relative efficiency of propositional proof systems. Journal of Symbolic Logic, vol. 44 (1979), no. 1, pp. 36–50.Google Scholar
Ehrenfeucht, A. and Mycielski, J., Abbreviating proofs by adding new axioms, this Bulletin, vol. 77 (1971), pp. 366–367.Google Scholar
Friedman, H., On the consistency, completeness and correctness. Unpublished typescript, 1979.Google Scholar
Glaßer, C., Selman, A. L., and Zhang, L., Canonical disjoint NP-pairs of propositional proof systems. Theoretical Computer Science, vol. 370 (2007), no. 1–3, pp. 60–73.Google Scholar
Glaßer, C., Selman, A. L., Sengupta, S., and Zhang, L., Disjoint NP-pairs. SIAM Journal on Computing, vol. 33 (2004), no. 6, pp. 1369–1416.Google Scholar
Hájek, P. and Pudlák, P., Metamathematics of First Order Arithmetic, ASL Perspectives in Logic, Springer-Verlag, Berlin, 1993.Google Scholar
Hanika, J., Herbrandizing search problems in bounded arithmetic. Mathematical Logic Quarterly, vol. 50 (2004), no. 6, pp. 577–586.Google Scholar
Impagliazzo, R. and Paturi, R., The complexity of k-SAT, Proceedings of the 14th Annual IEEE Conference on Computational Complexity, IEEE Computer Society, Los Alamitos, CA, 1999, pp. 237–240.Google Scholar
Johnson, D., Papadimitriou, C., and Yannakakis, M., How easy is local search? Journal of Computer and System Sciences, vol. 37 (1988), pp. 79–100.Google Scholar
Krajíček, J. and Impagliazzo, R., A note on conservativity relations among bounded arithmetic theories. Mathematical Logic Quarterly, vol. 48 (2002), no. 3, pp. 375–377.Google Scholar
Köbler, J., Messner, J., and Torán, J., Optimal proof systems imply complete sets for promise classes. Information and Computation, vol. 184 (2003), pp. 71–92.CrossRefGoogle Scholar
Kołodziejczyk, L., Nguyen, P., and Thapen, N., The provably total NP search problems of weak second order bounded arithmetic. Annals of Pure and Applied Logic, vol. 162 (2011), no. 6, pp. 419–446.Google Scholar
Krajíček, J., Bounded Arithmetic, Propositional Logic, and Complexity Theory, Encyclopedia of Mathematics and its Applications, vol. 60, Cambridge University Press, Cambridge, 1995.Google Scholar
Krajíček, J., Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. Journal of Symbolic Logic, vol. 62 (1997), no. 2, pp. 457–486.Google Scholar
Krajíček, J., On the proof complexity of the Nisan-Wigderson generator based on a hard NP∩coNP function. Journal of Mathematical Logic, vol. 11 (2011), no. 1, pp. 11–27.Google Scholar
Krajíček, J. and Pudlák, P., Propositional proof systems, the consistency of first order theories and the complexity of computations. Journal of Symbolic Logic, vol. 54 (1989), no. 3, pp. 1063–1079.Google Scholar
Krajíček, J., Pudlák, P., and Takeuti, G., Bounded arithmetic and polynomial hierarchy. Annals of Pure and Applied Logic, vol. 52 (1991), pp. 143–154.Google Scholar
Pudlák, P., On the length of proofs of finitistic consistency statements in first order theories, Logic Colloquium 84 (Paris, J. B., Wilkie, A. J., and Wilmers, G. M., editors), North Holland, Amsterdam, 1986, pp. 165–196.Google Scholar
Pudlák, P., Improved bounds to the length of proofs of finitistic consistency statements, Contemporary Mathematics, vol. 65, American Mathematical Society, 1987, pp. 309–331.Google Scholar
Pudlák, P., A note on bounded arithmetic. Fundamenta Mathematicae, vol. 136 (1990), no. 2, pp. 86–89.Google Scholar
Pudlák, P., Some relations between subsystems of arithmetic and the complexity theory, Logic from Computer Science, Proceedings of a Workshop held November 13-17, 1989 (Moschovakis, Y. N., editor), Springer-Verlag, New York, 1992, pp. 499–519.Google Scholar
Pudlák, P., Gödel and computations. ACM SIGACT News, vol. 37/4 (2006), pp. 13–21.Google Scholar
Pudlák, P., Logical Foundations of Mathematics and Computational Complexity, a Gentle Introduction, Springer Monographs in Mathematics, Springer-Verlag, Heidelberg, 2013.Google Scholar
Pudlák, P., On the complexity of finding falsifying assignments for Herbrand disjunctions. Archive for Mathematical Logic, vol. 54 (2015), no. 7, pp. 769–783.Google Scholar
Pudlák, P. and Thapen, N., Alternating minima and maxima, nash equilibria and bounded arithmetic. Annals of Pure and Applied Logic, vol. 163 (2012), no. 5, pp. 604–614.Google Scholar
Razborov, A. A., On provably disjoint NP-pairs. ECCC Technical report TR94–006, 1994.Google Scholar
Razborov, A. A., Pseudorandom generators hard for k-DNF resolution and polynomial calculus resolution. Annals of Mathematics, vol. 181 (2015), no. 2, pp. 415–472.Google Scholar
Skelley, A. and Thapen, N., The provably total search problems of bounded arithmetic. Proceedings of the London Mathematical Society, vol. 103 (2011), no. 1, pp. 106–138.Google Scholar
Smoryński, C., The incompleteness theorems, Handbook of Mathematical Logic (Barwise, J., editor), North-Holland, Amsterdam, 1977, pp. 821–865.Google Scholar