Hostname: page-component-745bb68f8f-hvd4g Total loading time: 0 Render date: 2025-01-09T10:06:53.703Z Has data issue: false hasContentIssue false
  • English
  • Français

Propositional proof systems, the consistency of first order theories and the complexity of computations

Published online by Cambridge University Press:  12 March 2014

Jan Krajíček  and
Pavel Pudlák
Jan Krajíček
Affiliation:
Mathematical Institute, Czechoslovak Academy of Sciences, 115 67 Prague 1, Czechoslovakia
Pavel Pudlák
Affiliation:
Mathematical Institute, Czechoslovak Academy of Sciences, 115 67 Prague 1, Czechoslovakia
Get access Rights & Permissions [Opens in a new window]

Abstract

We consider the problem about the length of proofs of the sentences saying that there is no proof of contradiction in S whose length is < n. We show the relation of this problem to some problems about propositional proof systems.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 54 , Issue 3 , September 1989 , pp. 1063 - 1079
Copyright
Copyright © Association for Symbolic Logic 1989

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

[BGS]Baker, T., Gill, J., and Solovav, R., Relativizations of the question, SIAM Journal on Computing, vol. 4 (1975), pp. 431–442.CrossRefGoogle Scholar
[Bu]Buss, S. R., Bounded arithmetic, Bibliopolis, Naples, 1986.Google Scholar
[Co]Cook, S. A., Feasibly constructive proofs and the propositional calculus, Proceedings of the seventh annual ACM symposium on the theory of computing, 1975, pp. 83–97.Google Scholar
[CR]Cook, S. A. and Reckhow, R. A., The relative efficiency of propositional proof systems, this Journal, vol. 44 (1979), pp. 36–50.Google Scholar
[Do]Dowd, M., Model-theoretic aspects of preprint, 1985.Google Scholar
[Fr]Friedman, H., On the consistency, completeness and correctness problems, preprint, Ohio State University, Columbus, Ohio, 1979.Google Scholar
[Ha]Haken, A., The intractability of resolution, Theoretical Computer Science, vol. 39 (1985), pp. 297–308.CrossRefGoogle Scholar
[KP]Krajíˇcek, J. and Pudlák, P., Quantified propositional calculi and fragments of bounded arithmetic, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik (to appear).Google Scholar
[Le]Levin, L. A., Universal sorting problems, Problemy Peredači Informacii, vol. 9 (1973), no. 3, pp. 115–116; English translation, Problems of Information Transmission, vol. 9 (1973), pp. 265–266.Google Scholar
[PW1]Paris, J. B. and Wilkie, A. J., Counting problems in bounded arithmetic, Methods in mathematical logic (proceedings, Caracas, 1983), Lecture Notes in Mathematics, vol. 1130, Springer-Verlag, Berlin, 1985, pp. 317–340.CrossRefGoogle Scholar
[PW2]Paris, J. B. 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
[Pu1]Pudlák, P., On the length of proofs of finitistic consistency statements in first order theories, Logic Colloquium '84 (Paris, J. B.et al., editors), North-Holland, Amsterdam, 1986, pp. 165–196.CrossRefGoogle Scholar
[Pu2]Pudlák, P., Improved bounds to the length of proofs of finitistic consistency statements, Logic and combinatorics (Simpson, S. G., editor), Contemporary Mathematics, vol. 65, American Mathematical Society, Providence, Rhode Island, 1987, pp. 309–332.CrossRefGoogle Scholar
[Sa]Savage, J., The complexity of computing, Wiley, New York, 1976.Google Scholar
[W]Wilkie, A. J., Subsystems of arithmetic and complexity theory, Lecture at the eighth international congress of logic, methodology and philosophy of science, Moscow, 1987.Google Scholar
[Wi]Wilson, G. B., Relativization, readabilities and the exponential hierarchy, Technical Report No. 140, University of Toronto, Toronto, 1980.Google Scholar