Hostname: page-component-76fb5796d-x4r87 Total loading time: 0 Render date: 2024-04-25T07:55:10.730Z Has data issue: false hasContentIssue false
  • English
  • Français

The deduction rule and linear and near-linear proof simulations

Published online by Cambridge University Press:  12 March 2014

Maria Luisa Bonet  and
Samuel R. Buss
Maria Luisa Bonet
Affiliation:
Department of Mathematics, University of California, San Diego, Lajolla, California92093
Samuel R. Buss
Affiliation:
Department of Mathematics, University of California, San Diego, Lajolla, California92093
Get access Rights & Permissions [Opens in a new window]

Abstract

We introduce new proof systems for propositional logic, simple deduction Frege systems, general deduction Frege systems, and nested deduction Frege systems, which augment Frege systems with variants of the deduction rule. We give upper bounds on the lengths of proofs in Frege proof systems compared to lengths in these new systems. As applications we give near-linear simulations of the propositional Gentzen sequent calculus and the natural deduction calculus by Frege proofs. The length of a proof is the number of lines (or formulas) in the proof.

A general deduction Frege proof system provides at most quadratic speedup over Frege proof systems. A nested deduction Frege proof system provides at most a nearly linear speedup over Frege system where by “nearly linear” is meant the ratio of proof lengths is O(α(n)) where α is the inverse Ackermann function. A nested deduction Frege system can linearly simulate the propositional sequent calculus, the tree-like general deduction Frege calculus, and the natural deduction calculus. Hence a Frege proof system can simulate all those proof systems with proof lengths bounded by O(n . α(n)). Also we show that a Frege proof of n lines can be transformed into a tree-like Frege proof of O(n log n) lines and of height O(log n). As a corollary of this fact we can prove that natural deduction and sequent calculus tree-like systems simulate Frege systems with proof lengths bounded by O(n log n).

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 58 , Issue 2 , June 1993 , pp. 688 - 709
Copyright
Copyright © Association for Symbolic Logic 1993

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]Bonet, M. L., Number of symbols in Frege proofs with and without the deduction rule, Arithmetic, proof theory and computation complexity (Clote, P. and Krajíček, J., editors), Oxford University Press, London, 1993, pp. 61–95.CrossRefGoogle Scholar
[2]Bonet, M. L., The lengths of propositional proofs and the deduction rule, Ph.D. Thesis, U. C. Berkeley, Berkeley, California, 1991.Google Scholar
[3]Bonet, M. L. and Buss, S. R., On the serial transitive closure problem (submitted).Google Scholar
[4]Bonet, M. L. and Buss, S. R., On the deduction rule and the number of proof lines, Proceedings sixth annual IEEE symposium on logic in computer science, 1991, Institute of Electronics Engineers, New York, 1991, pp. 286–297.Google Scholar
[5]Buss, S. R., Bounded arithmetic, Bibliopolis, Naples, 1986 (revision of 1985 Ph.D. Thesis, Princeton University, Princeton).Google Scholar
[6]Cook, S. A., Feasibly constructive proofs and the propositional calculus, Proceedings of the 7th annual ACM symposium on theory of computing, 1975, Association for Computing Machinery, New York, pp. 83–97.Google Scholar
[7]Cook, S. A. and Reckhow, R. A., The relative efficiency of propositional proof systems, this Journal, vol. 44 (1979), pp. 36–50.Google Scholar
[8]Kleene, S. C., Introduction to metamathematics, Wolters-Noordhoff, Groningen, and North-Holland, Amsterdam, 1971.Google Scholar
[9]Krajíček, J., Lower bounds to the size of constant-depth Frege proofs, this Journal, (to appear).Google Scholar
[10]Orevkov, V. P., Upper bound on the lengthening of proofs by cut elimination, Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im. V. A. Steklova Akademii Nauk SSSR (LOMI), vol. 137 (1984), pp. 87–98; English translation, Journal of Soviet Mathematics, vol. 34 (1986).Google Scholar
[11]Orevkov, V. P., Reconstruction of a proof from its scheme, Doklady Akademii Nauk SSSR, vol. 293 (1987), pp. 313–316; English translation, Soviet Mathematics Doklady, vol. 35 (1987).Google Scholar
[12]Pitassi, T., Beame, P., and Impagliazzo, R., Exponential lower bounds for the pigeonhole principle, Computational Complexity, (to appear).Google Scholar
[13]Prawitz, D., Ideas and results in proof theory, Proceedings of the second Scandinavian logic symposium, 1971, North-Holland, 1971, pp. 235–307.CrossRefGoogle Scholar
[14]Reckhow, R. A., On the lengths of proofs in the propositional calculus, Ph.D. Thesis, Department of Computer Science, University of Toronto, Toronto, 1976 (technical report #87).Google Scholar
[15]Statman, R., Complexity of derivations from quantifier-free Horn formulae, mechanical introduction of explicit definitions, and refinement of completeness theorems, Logic Colloquium '76, North-Holland, Amsterdam, 1977, pp. 505–517.Google Scholar
[16]Szabo, M., The collected papers of Gerhard Gentzen, North-Holland, Amsterdam, 1969.Google Scholar
[17]Takeuti, G., Proof theory, 2nd ed., North-Holland, Amsterdam, 1987.Google Scholar