For details see www.cis.upenn.edu/departmental/events/Jean.shtml

What is truth? What is a proof? These deep and difficult questions have been studied by philosophers for at least two millennia and no clear answers seem to have been provided. As suggested by Peter Andrews, ``truth is ellusive,´´ and one approach to understand what truth is to study the notion of proof: ``to thuth through proof´´!

In this talk, which will have an historical, philosophical, comical, and mildly technical flavor, we will attempt to explain what a proof is by describing the rules of logical reasoning in terms of natural deduction systems due to Gentzen and Prawitz. Some familiar proof principles such as ``proof by contradiction´´ and ´´double negation elimination´´ will reveal themselves as possibly unsafe and definitely non-constructive. This will lead us to a brief presentation of intuitionistic logic, to the notion of proof normalization, to various lambda-calculi encoding proofs, and to the ``Curry-Howard isomorphism´´ (or ``formulae as types principle ´´). We will conclude with a glimpse at more refined logics (such as linear logic) and semantic-driven logics, such as temporal logic. I will not prove anything during this talk; it is intended to be fun and provocative!