Jean Gallier 

Department of Computer Information Science

"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 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!

 

 

 

Refreshments will be served on the

2nd Floor Mezzanine Level

outside Wu & Chen

immediately following the talk.

____________________________________________________________________________