Geodesic
The Lengths of Proofs: Kreisel's conjecture and Gödel's speed-up theorem
Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part XI, Tome 358 (2008), pp. 153-188 Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice du chapitre de livre

We collect and compare several results which have been obtained so far in the attempts to prove a statement conjectured by Kreisel, about the lengths of proofs. We also survey several results regarding a speed-up theorem announced by Gödel in an abstract published in 1936. Finally we connect this to Kreisel's conjecture. Bibl. – 63 titles. 
@article{ZNSL_2008_358_a8,
     author = {S. Cavagnetto},
     title = {The {Lengths} of {Proofs:} {Kreisel's} conjecture and {G\"odel's} speed-up theorem},
     journal = {Zapiski Nauchnykh Seminarov POMI},
     pages = {153--188},
     year = {2008},
     volume = {358},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/ZNSL_2008_358_a8/}
}
TY  - JOUR
AU  - S. Cavagnetto
TI  - The Lengths of Proofs: Kreisel's conjecture and Gödel's speed-up theorem
JO  - Zapiski Nauchnykh Seminarov POMI
PY  - 2008
SP  - 153
EP  - 188
VL  - 358
UR  - http://geodesic.mathdoc.fr/item/ZNSL_2008_358_a8/
LA  - en
ID  - ZNSL_2008_358_a8
ER  - 
%0 Journal Article
%A S. Cavagnetto
%T The Lengths of Proofs: Kreisel's conjecture and Gödel's speed-up theorem
%J Zapiski Nauchnykh Seminarov POMI
%D 2008
%P 153-188
%V 358
%U http://geodesic.mathdoc.fr/item/ZNSL_2008_358_a8/
%G en
%F ZNSL_2008_358_a8
S. Cavagnetto. The Lengths of Proofs: Kreisel's conjecture and Gödel's speed-up theorem. Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part XI, Tome 358 (2008), pp. 153-188. http://geodesic.mathdoc.fr/item/ZNSL_2008_358_a8/

[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 | MR | Zbl

[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 | MR | Zbl

[6] M. Baaz, R. Zach, “Generalizing theorems in real closed fields”, Annals of Pure and Applied Logic, 75 (1995), 3–23 | DOI | MR | Zbl

[7] M. Baaz, R. Zach, “Note on generalizing theorems in algebrically closed fields”, Archive for Mathematical Logic, 37 (1998), 297–307 | DOI | MR | Zbl

[8] H. P. Barendregt, The Lambda Calculus, revised edition, North-Holland, Amsterdam, 1984 | MR | Zbl

[9] J. Barwise (ed.), Handbook of Mathematical Logic, North-Holland, Amsterdam, 1977 | MR

[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 | MR | Zbl

[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 | DOI | MR | Zbl

[13] S. Buss, “Bounded Arithmetic, Proof Complexity and two papers of Parikh”, Annals of Pure and Applied Logic, 96 (1999), 45–55 | DOI | MR

[14] S. Buss (ed.), Handbook of Proof Theory, North-Holland, Amsterdam, 1998 | MR

[15] S. Buss, “The undecidability of $k$-provability”, Annals of Pure and Applied Logic, 52 (1991), 3–29 | DOI | MR | Zbl

[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 | MR | Zbl

[18] P. Clote, J. Krajíček (eds.), Arithmetic Proof Theory and Computational Complexity, Oxford University Press, 1993 | MR

[19] A. Ehrenfeucht, J. Mycielski, “Abbreviating proofs by adding new axioms”, Bulletin of the American Mathematical Society, 77 (1971), 366–367 | DOI | MR | Zbl

[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 | DOI | MR | Zbl

[22] W. Farmer, “A unification theoretic method for investigating the $k$-provability problem”, Annals of Pure and Applied Logic, 51 (1991), 173–214 | DOI | MR | Zbl

[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 | DOI | MR | Zbl

[25] Kurt Gödel, Collected Works, Vol. 1, Oxford University Press, London–New York, 1986, 396–399 | DOI | MR | MR | Zbl

[26] Kurt Gödel, Collected Works, Vol. 1, Oxford University Press, London–New York, 1986, 234–237 | MR

[27] Kurt Gödel, Collected Works, Vol. 1, Oxford University Press, London–New York, 1986, 396–399 | MR | Zbl

[28] W. Goldfarb, “The undecidability of the second-order unification problem”, Theoretical Computer Science, 13 (1981), 225–230 | DOI | MR | Zbl

[29] C. Hankin, Lambda Calculi. A guide for computer scientist, Graduate Texts in Computer Science, 3, Oxford Univ. Press, 1994 | MR | Zbl

[30] P. Hrubeš, “Theories very close to $PA$ where Kreisel's conjecture is false”, J. of Symbolic Logic, 72:1 (2007), 123–137 | DOI | MR | Zbl

[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 | DOI | MR | Zbl

[33] S. Kleene, Introduction to Metamathematics, D. Van Nostrand Comp., Inc., New York–Toronto, 1952 | MR

[34] J. Krajíček, “On the number of steps in proofs”, Annals of Pure and Applied Logic, 41 (1989), 153–178 | DOI | MR | Zbl

[35] J. Krajíček, “Generalizations of proofs”, Proc. 5th Eastern Conf. on Model Theory, Humboldt University, Berlin, 1987, 82–99 | Zbl

[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 | DOI | MR | Zbl

[37] G. Kreisel, “A survey of Proof theory. II”, Proc. Sec. Scand. Log. Symp., ed. J. E. Fenstad, North-Holland, Amsterdam, 1971, 109–170 | MR

[38] G. S. Makanin, “The problem of solvability of equations in a free semigroup”, Math. Sbornik, 103(145):2 (1977), 147–236 (Russian) | MR | Zbl

[39] J. V. Matiyasevich, “Enumerable sets are diophantine”, Soviet Math. Dokl., 11 (1970), 354–358 | Zbl

[40] E. Mendelson, Introduction to Mathematical Logic, D. Van Nostrand Comp., Inc., Princeton–Toronto–New York–London, 1964 | MR

[41] T. Miyatake, “On the Lenght of Proofs in Formal Systems”, Tsukuba J. of Mathematics, 4 (1980), 115–125 | MR | Zbl

[42] A. Mostowski, Sentences undecidable in formalized arithmetic, North-Holland, Amsterdam, 1952 | MR | Zbl

[43] V. P. Orevkov, “Theorems with very short proof can be strengthened”, Semiotika i Informatika, 1979, no. 12, 37–38 (Russian) | MR

[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 | MR | Zbl

[46] R. Parikh, “Some results on the lengths of proofs”, Transactions of the American Mathematical Society, 177 (1973), 29–36 | DOI | MR | Zbl

[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 | DOI | MR | Zbl

[49] R. Parikh, “Existence and feasibility in arithmetic”, J. of Symbolic Logic, 36 (1971), 494–508 | DOI | MR | Zbl

[50] J. Paris, “A hierarchy of cuts in models of arithmetic”, Lecture Notes in Mathematics, 834, Springer, Berlin, 1980, 312–337 | MR

[51] J. Paris, L. Harrington, “A mathematical incompleteness in Peano Arithmetic”, Handbook of Mathematical Logic, ed. J. Barwise, North-Holland, Amsterdam, 1977, 1133–1142 | MR

[52] P. Pudlák, “Lengths of proofs”, Handbook of Proof Theory, ed. S. Buss, North-Holland, Amsterdam, 1998, 547–637 | MR

[53] P. Pudlák, “On a unification problem related to Kreisel's conjecture”, Comm. Math. Univ. Carol., 29:3 (1988), 551–556 | MR | Zbl

[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 | MR

[55] D. Richardson, “Sets theorems with short proofs”, J. of Symbolic Logic, 39 (1974), 235–242 | DOI | MR | Zbl

[56] A. Robinson, “A machine-oriented logic based on the resolution principle”, J. ACM, 12 (1965), 23–41 | DOI | MR | Zbl

[57] A. Robinson, A. Voronkov (eds.), Handbook of Automated Reasoning, Elsevier Science Publishers, 2001

[58] J. Shoenfield, Mathematical Logic, Addison-Wesley, Reading, MA, 1967 | MR | Zbl

[59] C. Smorynski, “The incompleteness theorems”, Handbook of Mathematical Logic, ed. J. Barwise, North Holland, Amsterdam, 1977, Part D, sec. 1, 821–865 | MR

[60] G. Takeuti, Proof theory, 2nd edition, North-Holland, Amsterdam, 1987 | MR | Zbl

[61] T. Yukami, “A theorem on the formalized arithmetic with function sysmbols $'$ and $+$”, Tsukuba J. of Mathematics, 1 (1977), 195–211 | MR | Zbl

[62] T. Yukami, “A note on a formalized arithmetic with function symbols $'$ and $+$”, Tsukuba J. of Mathematics, 2 (1978), 69–73 | MR | Zbl

[63] T. Yukami, “Some results on speed-up”, Annals Japan Assoc. Phil. of Science, 6:4 (1984), 195–205 | MR | Zbl