Proofs, Reasoning and the Metamorphosis of Logic

  • Jean-Baptiste JoinetEmail author
Part of the Trends in Logic book series (TREN, volume 39)


With the “mathematical watershed”, Logic had been transformed into a foundational theory for mathematics, a theory of truth and proofs—far away from its philosophical status of theory of the intellectual process of reasoning. With the recent substitution of the traditional proofs-as-discourses paradigm by the proofs-as-programs one, Logic is now becomming a foundational theory for computing. One could interpret this new watershed as being “yet another technological drift”, bringing Logic always closer to practical ingeneering, always further from the human intellectual process of reasoning. This article promotes the dual point of view: enlightened by the contemporary analysis of the dynamic of proofs, which bring us to a new understanding of the semantic counterpart of processes operationality (including the links between semantic dereliction due to inconsistency and computational exuberance), Logic has never appeared so close to being, finally, the theory of reasoning.


Proof Computation Reasoning Philosophy of logic 



I would like to thank Gilles Dowek (french National Institute for Research in Computer Science and Automatics, I.N.R.I.A.) for the friendly and serious moments we spent, walking and talking in the tropical garden of the PUC university campus in Rio, John Tain for his help concerning English and François Rivenc for his remarks and advice about an earlier version of this article. My participation to the conference Natural Deduction, Rio 2002 was supported by the French National Center for Scientific Research (Proofs-Programs-Systems team) and the Brazilian Ministry for Research.


  1. 1.
    Hilbert, D. (1927). The foundations of mathematics. In J. van Heijenoort (Ed.), From Frege to Gödel: a sourcebook in mathematical logic (pp. 1971–1931). Cambridge: Harvard University Press.Google Scholar
  2. 2.
    Boole, G. (1930). Investigation of the laws of thought. Mineola: Dover Publications.Google Scholar
  3. 3.
    Hume, D. (1902). An enquiry concerning human understanding. Oxford: Oxford University Press. (First edition published in 1748).Google Scholar
  4. 4.
    Dummett, Michael. (1993). Origins of analytic philosophy. Cambridge, London: Duckworth, Harvard University Press.Google Scholar
  5. 5.
    Girard, J.-Y. (1996). Proof-nets: the parallel syntax for proof-theory. In Ursini & Agliano (Eds.), Logic and algebra. New York: Marcel Dekker.Google Scholar
  6. 6.
    Girard, J. Y. (1995). Linear logic: its syntax and semantics. In J.-Y. Girard, Y. Lafont, & L. Regnier (Eds.), Advances in linear logic: mathematical society lecture notes series (Vol. 222, pp. 1–42). London: Cambridge University Press.CrossRefGoogle Scholar
  7. 7.
    Dummett, M. (1978). The philosophical basis of intuitionistic logic. Truth and other enigmas. London: Duckworth.Google Scholar
  8. 8.
    Girard, J.-Y. (2001). Locus solum. Mathematical Structures in Computer Science, 11(03), 301–506.CrossRefGoogle Scholar
  9. 9.
    Wainer, S. S., & Wallen, L. A. (1992). Basic proof theory. In S. S. Wainer, P. Aczel, & H. Simmons (Eds.), Proof theory: a selection of papers from the Leeds proof theory programme 1990 (pp. 1–26). New York: Cambridge University Press.Google Scholar
  10. 10.
    Danos, Vincent, & Krivine, Jean-Louis. (2000). Disjunctive tautologies as synchronisation schemes. Proceedings of CSL’2000. LCS, 1862, (pp. 202–301).Google Scholar
  11. 11.
    Pinkas, D. (1995). La matérialité de l’esprit. Paris: La découverte.Google Scholar
  12. 12.
    Panaccio, C. (1999). Le discours intérieur: de Platon à Guillaume d’Ockham. Paris: Editions du Seuil.Google Scholar
  13. 13.
    Danos, V. (1990). La logique linéaire appliquée à l’étude de divers processus de normalisation (principalement du lambda-calcul), (Université Paris 7, Paris). Ph.D. Thesis.Google Scholar
  14. 14.
    Joinet, J.B. (2007). Sur le temps logique. Logique, dynamique et cognition, (pp. 31–49). Paris: Publications de la Sorbonne. ISBN 978-2-85944-584-3.Google Scholar
  15. 15.
    Joinet, T.-A. (2009). Ouvrir la logique au monde. Hermann: Philosophie et mathématique de l’interaction. Paris. ISBN 978-2-85944-584-3.Google Scholar
  16. 16.
    Danos, Vincent, & Joinet, Jean-Baptiste. (2003). Linear logic and elementary time. Information and Computation, 183(1), 123–137.CrossRefGoogle Scholar
  17. 17.
    Girard, J. Y. (1998). Light linear logic. Information and Computation, 143(2), 175–204.CrossRefGoogle Scholar
  18. 18.
    Prawitz, D. (1977). Meaning and proofs: on the conflict between classical and intuitionistic logic. Theoria, 43(1), 1–40.Google Scholar
  19. 19.
    Danos, V., Joinet, J. B., & Schellinx, H. (1997). A new deconstructive logic: linear logic. The Journal of Symbolic Logic, 62(3), 755–807.CrossRefGoogle Scholar
  20. 20.
    Girard, J.-Y. (1991). A new constructive logic: classical logic. Mathematical Structures in Computer Science, 1(3), 255–296.CrossRefGoogle Scholar
  21. 21.
    Krivine, J.-L. (1994). Classical logic, storage operators and second order lambda-calculus. In Annals of Pure and Applied Logic, 68, 63–78.CrossRefGoogle Scholar
  22. 22.
    Krivine, J.-L. (2001). Typed lambda-calculus in classical Zermelo-Fraenkel set theory. Archive for Mathematical Logic, 40(3), 189–205.CrossRefGoogle Scholar
  23. 23.
    Parigot, M. (1992). Lambda-mu calculus: An algorithmic interpretation of classical natural deduction. Proceedings of the International Conference on Logic Programming and Automated Reasoning (pp. 190–201).Google Scholar

Copyright information

© Springer Science+Business Media Dordrecht 2014

Authors and Affiliations

  1. 1.Faculté de philosophieUniversité Jean Moulin - Lyon 3LyonFrance

Personalised recommendations