Penn Arts & Sciences Logo

Thursday, November 6, 2008 - 3:00pm

Jean Gallier

Penn

Location

University of Pennsylvania

Wu & Chen, 101 Levine Hall

What is truth? What is a proof? These deep and difficult questions have been studied by philosophers for at least two millennia. As suggested by Peter Andrews, ``truth is elusive'', and one approach to understand what truth is to study the notion of proof: `to truth 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 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!