RUS  ENG
Full version
JOURNALS // Zapiski Nauchnykh Seminarov POMI
Zap. Nauchn. Sem. POMI, 2008, Volume 358, Pages 153–188 (Mi znsl2150)
The Lengths of Proofs: Kreisel's conjecture and Gödel's speed-up theorem
S. Cavagnetto

References
1. J. Avigad, R. Zach, The Epsilon Calculus, http:// plato.stanford.edu/archives/win2008/entries/epsilon-calculus/
2. F. Baader, W. Snyder, “Unification theory”, Handbook of Automated Reasoning, eds. A. Robinson, A. Voronkov, Elsevier Science Publishers, 2001, 447–533
3. F. Baader, T. Nipkow, Term Rewriting and All That, Cambridge University Press, Cambridge, 1999  mathscinet  zmath
4. M. Baaz, General solutions of equations with variables for substitution, preprint
5. M. Baaz, P. Pudlák, “Kreisel's conjecture for $L\exists_1$”, Arithmetic Proof Theory and Computational Complexity, eds. P. Clote, J. Krajíček, Oxford University Press, 1993, 30–60  mathscinet  zmath
6. M. Baaz, R. Zach, “Generalizing theorems in real closed fields”, Annals of Pure and Applied Logic, 75 (1995), 3–23  crossref  mathscinet  zmath
7. M. Baaz, R. Zach, “Note on generalizing theorems in algebrically closed fields”, Archive for Mathematical Logic, 37 (1998), 297–307  crossref  mathscinet  zmath
8. H. P. Barendregt, The Lambda Calculus, revised edition, North-Holland, Amsterdam, 1984  mathscinet  zmath
9. J. Barwise (ed.), Handbook of Mathematical Logic, North-Holland, Amsterdam, 1977  mathscinet
10. E. W. Beth, The foundation of mathematics, North-Holland, Amsterdam, 1965
11. M. Blum, “A machine-independent theory of the complexity of recursive functions”, J. of the Association for Computing Machinery, 14 (1967), 322–336  mathscinet  zmath
12. S. Buss, “On Gödel's theorems on lengths of proofs. I: Number of lines and speed-up for arithmetic”, J. of Symbolic Logic, 59:3 (1994), 737–756  crossref  mathscinet  zmath
13. S. Buss, “Bounded Arithmetic, Proof Complexity and two papers of Parikh”, Annals of Pure and Applied Logic, 96 (1999), 45–55  crossref  mathscinet
14. S. Buss (ed.), Handbook of Proof Theory, North-Holland, Amsterdam, 1998  mathscinet
15. S. Buss, “The undecidability of $k$-provability”, Annals of Pure and Applied Logic, 52 (1991), 3–29  crossref  mathscinet  zmath
16. S. Cavagnetto, “Speed-up theorem and Kreisel's Conjecture (abstract)”, Bulletin of Symbolic Logic, 12:2 (2005), 327–328
17. C. L. Chang, R. C. Lee, Symbolic logic and mechanical theorem proving, Academic Press, New York–London, 1973  mathscinet  zmath
18. P. Clote, J. Krajíček (eds.), Arithmetic Proof Theory and Computational Complexity, Oxford University Press, 1993  mathscinet
19. A. Ehrenfeucht, J. Mycielski, “Abbreviating proofs by adding new axioms”, Bulletin of the American Mathematical Society, 77 (1971), 366–367  crossref  mathscinet  zmath
20. W. Farmer, Lenght of proofs and unification theory, PhD thesis, University of Wisconsin–Madison, 1984
21. W. Farmer, “A unification algorithm for second order monadic terms”, Annals of Pure and Applied Logic, 39 (1988), 131–174  crossref  mathscinet  zmath
22. W. Farmer, “A unification theoretic method for investigating the $k$-provability problem”, Annals of Pure and Applied Logic, 51 (1991), 173–214  crossref  mathscinet  zmath
23. W. Farmer, The $k$-provability problem for Gentzen-style sequent systems, Technical report M89-20, The MITRE Corporation, 1989
24. H. Friedman, “One hundred and two problems in mathematical logic”, J. of Symbolic Logic, 40 (1975), 113–129  crossref  mathscinet  zmath
25. Kurt Gödel, Collected Works, Vol. 1, Oxford University Press, London–New York, 1986, 396–399  crossref  mathscinet  mathscinet  zmath
26. Kurt Gödel, Collected Works, Vol. 1, Oxford University Press, London–New York, 1986, 234–237  mathscinet
27. Kurt Gödel, Collected Works, Vol. 1, Oxford University Press, London–New York, 1986, 396–399  mathscinet  zmath
28. W. Goldfarb, “The undecidability of the second-order unification problem”, Theoretical Computer Science, 13 (1981), 225–230  crossref  mathscinet  zmath
29. C. Hankin, Lambda Calculi. A guide for computer scientist, Graduate Texts in Computer Science, 3, Oxford Univ. Press, 1994  mathscinet  zmath
30. P. Hrubeš, “Theories very close to $PA$ where Kreisel's conjecture is false”, J. of Symbolic Logic, 72:1 (2007), 123–137  crossref  mathscinet  zmath
31. P. Hrubeš, A theory where Kreisel's Conjecture is true, draft
32. R. Kaye, “Diophantine induction”, Annals of Pure and Applied Logic, 46:1 (1990), 1–40  crossref  mathscinet  zmath
33. S. Kleene, Introduction to Metamathematics, D. Van Nostrand Comp., Inc., New York–Toronto, 1952  mathscinet
34. J. Krajíček, “On the number of steps in proofs”, Annals of Pure and Applied Logic, 41 (1989), 153–178  crossref  mathscinet  zmath
35. J. Krajíček, “Generalizations of proofs”, Proc. 5th Eastern Conf. on Model Theory, Humboldt University, Berlin, 1987, 82–99  zmath
36. J. Krajíček, P. Pudlák, “The number of proof lines and the size of proofs in first order logic”, Archive for Mathematical Logic, 27 (1988), 69–84  crossref  mathscinet  zmath
37. G. Kreisel, “A survey of Proof theory. II”, Proc. Sec. Scand. Log. Symp., ed. J. E. Fenstad, North-Holland, Amsterdam, 1971, 109–170  mathscinet
38. G. S. Makanin, “The problem of solvability of equations in a free semigroup”, Math. Sbornik, 103(145):2 (1977), 147–236 (Russian)  mathnet  mathscinet  zmath
39. J. V. Matiyasevich, “Enumerable sets are diophantine”, Soviet Math. Dokl., 11 (1970), 354–358  zmath
40. E. Mendelson, Introduction to Mathematical Logic, D. Van Nostrand Comp., Inc., Princeton–Toronto–New York–London, 1964  mathscinet
41. T. Miyatake, “On the Lenght of Proofs in Formal Systems”, Tsukuba J. of Mathematics, 4 (1980), 115–125  mathscinet  zmath
42. A. Mostowski, Sentences undecidable in formalized arithmetic, North-Holland, Amsterdam, 1952  mathscinet  zmath
43. V. P. Orevkov, “Theorems with very short proof can be strengthened”, Semiotika i Informatika, 1979, no. 12, 37–38 (Russian)  mathscinet
44. V. P. Orevkov, “Reconstruction of the proof from its scheme”, Russian abstract, 7-th Conf. Math. Log., 1984, 133
45. V. P. Orevkov, “Reconstruction of the proof by its analysis”, Dokl. Akad. Nauk, 293:2 (1987), 313–316  mathnet  mathscinet  zmath
46. R. Parikh, “Some results on the lengths of proofs”, Transactions of the American Mathematical Society, 177 (1973), 29–36  crossref  mathscinet  zmath
47. R. Parikh, “Introductory note to 1936 a”, Collected Works, Vol. 1, Oxford University Press, London–New York, 1986, 394–396
48. R. Parikh, “Length and structure of proofs”, Synthese, 114 (1998), 41–48  crossref  mathscinet  zmath
49. R. Parikh, “Existence and feasibility in arithmetic”, J. of Symbolic Logic, 36 (1971), 494–508  crossref  mathscinet  zmath
50. J. Paris, “A hierarchy of cuts in models of arithmetic”, Lecture Notes in Mathematics, 834, Springer, Berlin, 1980, 312–337  mathscinet
51. J. Paris, L. Harrington, “A mathematical incompleteness in Peano Arithmetic”, Handbook of Mathematical Logic, ed. J. Barwise, North-Holland, Amsterdam, 1977, 1133–1142  mathscinet  adsnasa
52. P. Pudlák, “Lengths of proofs”, Handbook of Proof Theory, ed. S. Buss, North-Holland, Amsterdam, 1998, 547–637  mathscinet
53. P. Pudlák, “On a unification problem related to Kreisel's conjecture”, Comm. Math. Univ. Carol., 29:3 (1988), 551–556  mathscinet  zmath
54. P. Pudlák, “On the lenghts of proofs of finitistic consistency statements in first-order theories”, Logic Colloquium' 84, North-Holland, Amsterdam, 1986, 165–196  mathscinet
55. D. Richardson, “Sets theorems with short proofs”, J. of Symbolic Logic, 39 (1974), 235–242  crossref  mathscinet  zmath
56. A. Robinson, “A machine-oriented logic based on the resolution principle”, J. ACM, 12 (1965), 23–41  crossref  mathscinet  zmath
57. A. Robinson, A. Voronkov (eds.), Handbook of Automated Reasoning, Elsevier Science Publishers, 2001
58. J. Shoenfield, Mathematical Logic, Addison-Wesley, Reading, MA, 1967  mathscinet  zmath
59. C. Smorynski, “The incompleteness theorems”, Handbook of Mathematical Logic, ed. J. Barwise, North Holland, Amsterdam, 1977, Part D, sec. 1, 821–865  mathscinet
60. G. Takeuti, Proof theory, 2nd edition, North-Holland, Amsterdam, 1987  mathscinet  zmath
61. T. Yukami, “A theorem on the formalized arithmetic with function sysmbols $'$ and $+$”, Tsukuba J. of Mathematics, 1 (1977), 195–211  mathscinet  zmath
62. T. Yukami, “A note on a formalized arithmetic with function symbols $'$ and $+$”, Tsukuba J. of Mathematics, 2 (1978), 69–73  mathscinet  zmath
63. T. Yukami, “Some results on speed-up”, Annals Japan Assoc. Phil. of Science, 6:4 (1984), 195–205  mathscinet  zmath

© Steklov Math. Inst. of RAS, 2025