This text is an outgrowth of notes prepared by J. Y. Girard for a course at the University of Paris VII. It deals with the mathematical background of the application to computer science of aspects of logic (namely the correspondence between proposition & types). Combined with the conceptual perspectives of Girard's ideas, this sheds light on both the traditional logic material & its prospective applications to computer science. The book covers a very active & exciting research area, & it will (...) be essential reading for all those working in logic & computer science. (shrink)

We informally discuss some recent results on the incompleteness of formal systems. These theorems, which are of great importance to contemporary mathematical epistemology, are proved using a variety of conceptual tools provably stronger than those of finitary axiomatisations. Those tools require no mathematical ontology, but rather constitute particularly concrete human constructions and acts of comprehending infinity and space rooted in different forms of knowledge. We shall also discuss, albeit very briefly, the mathematical intelligence both of God and of computers. We (...) hope in this manner to help the reader overcome formalist reductionism, while avoiding naive Platonist ontologies, typical symptoms of Godelitis which affected many in the last seventy years. (shrink)