When: Wednesday, May 07, 3:30 p.m.

Where: 8220 Wean Hall

William Lovas

Speaking Skills Talk

Abstract:
Intuitionistic logic shares an intimate connection with programming: a proof of a proposition A corresponds to a program of type A, and evaluation of that program corresponds to proof simplification. For example, a proof of "A implies B" corresponds to a function of type A -> B. But intuitionistic logic rejects classical proof-by-contradiction and principles like the excluded middle "A or not A". Although such principles might seem innocuous, they engender a collapse of our function space: classically, "A implies B" is equivalent to "not A or B"! The close connection with programming seems to be lost. We show how to recover the computational interpretation by systematically constructing a programming language based on classical logic. A program is a term currently being evaluated along with a continuation saying what to do next. Classical proof-by-contradiction corresponds to a call/cc-like mechanism that gives a name to the current continuation, and proofs of classical tautologies correspond to programs that make essential use of first-class continuations. We also show that program evaluation in our language always terminates. Because program evaluation corresponds to proof normalization, this directly entails the consistency of classical logic. Our proof proceeds by a simple structural induction on the types of the terms involved and uses only elementary methods, avoiding difficult techniques like logical relations and quantification over predicates.

Presented in Partial Fulfillment of the CSD Speaking Skills Requirement.

<< Back