The computational content of arithmetical proofs. (English) Zbl 1269.03055
Natural deductions in intuitionistic arithmetic have a unique normal form. This is not true for Gentzen-style sequent derivations, especially in classical arithmetic. Using a special redundancy construction from a previous work with M. Baaz, the author proves that for a wide class of arithmetical theories \(T\) the number of possible cut-free forms of a single arithmetical derivation in \(T\) of a \(\Sigma^0_1\)-formula is not bounded by any function provably recursive in \(T\).
Reviewer: G. E. Mints (Stanford)
MSC:
| 03F05 | Cut-elimination and normal-form theorems |
| 03F07 | Structure of proofs |
| 03F30 | First-order arithmetic and fragments |
Keywords:
cut elimination; normal form; first-order arithmetic; arithmetical proofs; computational content; arithmetical theories; provably recursive functionReferences:
| [1] | Ackermann, W., “Zur Widerspruchsfreiheit der Zahlentheorie,” Mathematische Annalen , vol. 117 (1940), pp. 162-194. · Zbl 0022.29202 · doi:10.1007/BF01450016 |
| [2] | Avigad, J., “The computational content of classical arithmetic,” pp. 15-30 in Proofs, Categories, and Computations: Essays in Honor of Grigori Mints , edited by F. Solomon and S. Wilfried, vol. 13 of Tributes , College Publications, London, 2010. · Zbl 1244.03153 |
| [3] | Baaz, M., and S. Hetzl, “On the non-confluence of cut-elimination,” Journal of Symbolic Logic , vol. 76 (2011), pp. 313-340. · Zbl 1220.03048 · doi:10.2178/jsl/1294171002 |
| [4] | Baaz, M., S. Hetzl, A. Leitsch, C. Richter, and H. Spohr, “Cut-elimination: Experiments with CERES,” pp. 481-495 in Logic for Programming, Artificial Intelligence, and Reasoning , edited by F. Baader and A. Voronkov, vol. 3452 of Lecture Notes in Computer Science , Springer, Berlin, 2005. · Zbl 1108.03305 · doi:10.1007/b106931 |
| [5] | Friedman, H., “Classically and intuitionistically provable recursive functions,” pp. 21-27 in Higher Set Theory (Oberwolfach, 1977) , edited by G. H. Müller and D. S. Scott, vol. 669 of Lecture Notes in Mathematics , Springer, Berlin, 1978. · Zbl 0396.03045 |
| [6] | Gentzen, G., “Untersuchungen über das logische Schließen, I,” Mathematische Zeitschrift , vol. 39 (1935), pp. 176-210; “II,” pp. 405-431. · Zbl 0010.14601 · doi:10.1007/BF01201363 |
| [7] | Gentzen, G., “Die Widerspruchsfreiheit der reinen Zahlentheorie,” Mathematische Annalen , vol. 112 (1936), pp. 493-565. · Zbl 0014.38801 · doi:10.1007/BF01565428 |
| [8] | Girard, J.-Y., “Interprétation fonctionelle et élimination des coupures de l’arithmétique d’ordre supérieur,” Ph.D. thesis, Université Paris 7, 1972. |
| [9] | Gödel, K., “Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes,” Dialectica , vol. 12 (1958), pp. 280-287. · Zbl 0090.01003 · doi:10.1111/j.1746-8361.1958.tb01464.x |
| [10] | Hájek, P., and P. Pudlák, Metamathematics of First-Order Arithmetic , Perspectives in Mathematical Logic, Springer-Verlag, Berlin, 1998. · Zbl 0903.01017 |
| [11] | Kleene, S. C., “On the interpretation of intuitionistic number theory,” Journal of Symbolic Logic , vol. 10 (1945), pp. 109-124. · Zbl 0063.03260 · doi:10.2307/2269016 |
| [12] | Kohlenbach, U., Applied Proof Theory: Proof Interpretations and Their Use in Mathematics , Springer Monographs in Mathematics, Springer, Berlin, 2008. · Zbl 1158.03002 · doi:10.1007/978-3-540-77533-1 |
| [13] | Krajíček, J., “Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic,” Journal of Symbolic Logic , vol. 62 (1997), pp. 457-486. · Zbl 0891.03029 · doi:10.2307/2275541 |
| [14] | Kreisel, G., “On the interpretation of non-finitist proofs, II: Interpretation of number theory,” Journal of Symbolic Logic , vol. 17 (1952), pp. 43-58. · Zbl 0046.00701 · doi:10.2307/2267457 |
| [15] | Kreisel, G., “Finiteness theorems in arithmetic: An application of Herbrand’s theorem for \(\Sigma_{2}\)-formulas,” pp. 39-55, in Logic Colloquium ’81 ( Marseilles, 1981 ), edited by J. Stern, vol. 107 of Studies in Logic and the Foundations of Mathematics , North-Holland, Amsterdam, 1982. · Zbl 0499.03045 |
| [16] | Parigot, M., “\(\lambda\mu\)-Calculus: An algorithmic interpretation of classical natural deduction,” pp. 190-201, in Logic Programming and Automated Reasoning (St. Petersburg, 1992) , vol. 624 in Lecture Notes in Computer Science , Springer, Berlin, 1992. · Zbl 0925.03092 · doi:10.1007/BFb0013061 |
| [17] | Ratiu, D., and T. Trifonov, “Exploring the computational content of the infinite pigeonhole principle,” Journal of Logic and Computation , vol. 22 (2012), 329-350. · Zbl 1259.03072 · doi:10.1093/logcom/exq011 |
| [18] | Urban, C., and G. Bierman, “Strong normalisation of cut-elimination in classical logic,” Fundamenta Informaticae , vol. 45 (2000), pp. 123-155. · Zbl 0982.03032 |
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.
