Advertisement

Abstract

We address two questions:
  • what is the use of formal proofs?

  • how do we proceed from a formal proof to a computation?

Keywords

Formal Proof Proof Theory Combinatory Logic Truth Predicate Mathematical Explanation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    P. Aczel and M. Rathjen: Notes on Constructive Set Theory, Draft available from the Internet, http://www.cs.man.ac.uk/~petera/Google Scholar
  2. 2.
    M. Aschbacher: Highly complex proofs and implications of such proofs. Philosophical Transactions of the Royal Society A 363 (2005) pp 2401–2406CrossRefGoogle Scholar
  3. 3.
    J. Avigad: Number theory and elementary arithmetic. Philosophia Mathematica 11 (2003) pp 257–284Google Scholar
  4. 4.
    J. Avigad: Mathematical Method and Proof. Synthèse 153 (2006) pp 105–159CrossRefGoogle Scholar
  5. 5.
    J. Avigad, K. Donnelly, D. Gray and P. Raff: A formally verified proof of the prime number theorem. ACM Transactions on Computational Logic, 9, 1:2 (2007)CrossRefGoogle Scholar
  6. 6.
    H. Barendregt: The Lambda Calculus. Its Syntax and Semantics (Elsevier, Amsterdam, 1984)Google Scholar
  7. 7.
    P. Bernays: Mathematische Existenz und Widerspruchfreiheit. In: Ètudes de Philosophie des Sciences en hommage à Ferdinand Gonseth, (Neuchatel, 1950) pp 11–25 (English Translation by W. Sieg, R. Zach and S. Goodman, available as Text No.19, Bernays Project)Google Scholar
  8. 8.
    P. Bernays: Die Schematische Korrespondenz und die idealieserte Strukturen. Dialectica 24 (1970) pp 53–66 (English Translation by E. Reck and C.Parsons available as Text No.27, Bernays Project)CrossRefGoogle Scholar
  9. 9.
    A. Cantini: The axiom of choice and combinatory logic. Journal of Symbolic Logic 68 (2003) pp 1091–1108CrossRefGoogle Scholar
  10. 10.
    A. Cantini: Remarks on applicative theories. Annals of Pure and Applied Logic 136 (2005) pp 91–115CrossRefGoogle Scholar
  11. 11.
    L. Carroll: What the Tortoise said to Achilles. Mind 4 (1895) pp 278–280CrossRefGoogle Scholar
  12. 12.
    E. Casari: Matematica e Verità. Rivista di Filosofia 78 (1987) pp 329–350Google Scholar
  13. 13.
    C. Cellucci: The nature of mathematical explanation, this volume (2008)Google Scholar
  14. 14.
    C. Cornaros and C. Dimitracopoulos: The prime number theorem and fragments of PA. Arch. Math. Logic 33 (1994) pp 265–281CrossRefGoogle Scholar
  15. 15.
    L. Crosilla, H. Ishihara, P. Schuster: On constructing completions. Journal of Symbolic Logic 70 (2005) pp 969–978CrossRefGoogle Scholar
  16. 16.
    S. Feferman: In the Light of Logic (Oxford University Press, Oxford 1998)Google Scholar
  17. 17.
    E. Friedgut (with an appendix by J. Bourgain): Sharp thresholds of graph prop-erties and the k-Sat problem. Journal of the American Mathematical Society 12 (1999) pp 1017–1054CrossRefGoogle Scholar
  18. 18.
    E. Giusti: Ipotesi alla base dell’esistenza matematica (Boringhieri, Torino 1999)Google Scholar
  19. 19.
    A. Goerdt: A Threshold for Unsatisfiability. Journal of Computer and System Sciences 53 (1996) pp 469–486CrossRefGoogle Scholar
  20. 20.
    J. Hafner and P. Mancosu: The Varieties of Mathematical Explanation. In: Visualization, Explanation, and Reasoning Styles in Mathematics, ed by K. Jorgensen et al. (Kluwer, Dordrecht 2005).Google Scholar
  21. 21.
    G. Hardy: A mathematician’s apology (Cambridge University Press, Cambridge, 1941)Google Scholar
  22. 22. B. Intrigila and R. Statman: Some results on extensionality in lambda calculus. Annals of Pure and Applied Logic 132 (2005) pp 109–125CrossRefGoogle Scholar
  23. 23.
    R. Kahle: David Hilbert and functional self-application, preprint (2006)Google Scholar
  24. 24.
    U. Kohlenbach and P. Oliva: Proof mining: a systematic way of analysing proofs in mathematics. Proc. Steklov Inst. Math. 242 (2003) pp 136–164Google Scholar
  25. 25.
    U. Kohlenbach: Some Logical Metatheorems with Applications in Functional Analysis. Transactions of the American Mathematical Society 357 (2005) pp 89–128CrossRefGoogle Scholar
  26. 26.
    G. Kreisel: Principles of proofs and ordinals implicit in given concepts. In: Intuitionism and Proof Theory, ed by J. Myhill, A. Kino, J. Myhill and R. E. Vesley (North Holland, Amsterdam 1970) pp 489–516Google Scholar
  27. 27.
    G. Lee: Phase Transitions in Axiomatic Thought, Ph. Thesis, Westfalische Wilhelms-Universität Mönster (2005)Google Scholar
  28. 28.
    G. Lolli: Capire una dimostrazione (Il Mulino, Bologna 1988)Google Scholar
  29. 29.
    R. S. Lubarski and M. Rathjen: On the constructive Dedekind reals. To appear in Logic and Analysis, published online: 18 February (2008) pp 1–22Google Scholar
  30. 30.
    S. Mac Lane: Despite physicists, proof is essential in mathematics. Synthèse 111 (1997) pp 147–154CrossRefGoogle Scholar
  31. 31.
    P. Mancosu: Mathematical Explanation: Problems and Prospects. Topoi 20 (2001) pp 97–117CrossRefGoogle Scholar
  32. 32. G. Pólya: Eine Erinnerung an Hermann Weyl. Mathematische Zeitschrift 126 (1972) pp 296–298CrossRefGoogle Scholar
  33. 33.
    D. Prawitz: Natural Deduction: a Proof—theoretical Study (Almqvist and Wiksell, Stockholm 1965)Google Scholar
  34. 34.
    D. Prawitz: Philosophical Aspects of proof theory. In: Contemporary philosophy. A new survey, vol.I (Nijhoff, The Hague 1981) pp 235–277Google Scholar
  35. 35.
    Y. Rav: Why do we prove theorems. Philosophia Mathematica 7 (1999) pp 7–41Google Scholar
  36. 36.
    G. Rota: The phenomenology of mathematical beauty. Synthèse 111 (1997) pp 171–182CrossRefGoogle Scholar
  37. 37.
    B. Russell: The regressive method of discovering the premises of mathematics. In: B. Russell: Essays on Analysis (London 1973) pp 272–283Google Scholar
  38. 38.
    S.G. Simpson: Subsystems of Second Order Arithmetic (Springer, Berlin Heidelberg New York 1999)Google Scholar
  39. 39.
    A. Weiermann: An application of graphical enumeration to PA. J. Symbolic Logic 68 (2003) pp 5–16CrossRefGoogle Scholar
  40. 40.
    A. Weiermann: Analytic combinatorics, proof-theoretic ordinals, and phase transition for independence results. Ann. Pure Appl. Logic 136 (2005) pp 189-218CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Italia 2008

Authors and Affiliations

  • Andrea Cantini
    • 1
  1. 1.Dipartimento di FilosofiaUniversità di FirenzeFirenzeItaly

Personalised recommendations