Jean Gallier
Computer Science Department
University of Pennsylvania
" What is a Proof?"
Abstract:
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!
Thursday, November 6, 2008
3:00 - 4:15
Wu & Chen
101 Levine Hall