From awodey@cmu.edu Tue Mar 20 10:36:48 2007
Date: Tue, 20 Mar 2007 10:36:48 -0400
From: Steve Awodey <awodey@cmu.edu>
To: Steve Awodey <awodey@andrew.cmu.edu>
Subject: scott at

{\rtf1\mac\ansicpg10000\cocoartf824\cocoasubrtf410
{\fonttbl\f0\fswiss\fcharset77 Helvetica;}
{\colortbl;\red255\green255\blue255;}
\margl1440\margr1440\vieww9000\viewh8400\viewkind0
\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\ql\qnatural\pardirnatural

\f0\fs24 \cf0 The Future of Proof\
Dana S. Scott\
University Professor Emeritus\
Carnegie Mellon University\
\
ABSTRACT. G\'9adel showed us many things.  Among\
others he showed us the *possibility* of proof\
(via the Completeness Theorem for First-Order\
Logic); and then quite soon thereafter he showed\
us the *impossibility* of proof (via the\
Incompleteness Theorem for (suitable) Higher-\
Order Logics).  These results are well known\
and famous, but their impact on the practice\
of mathematics has perhaps not been very noticeable.\
To be sure, related recursive unsolvability results\
have a clear explanatory value in keeping people from\
searching for algorithms where none can exist.\
And modern developments in complexity theory show\
that many easily stated problems have -- in general --\
no quick solutions.  But again, many commentators\
agree that there has not been a big shift in\
main-stream mathematics as a consequence of G\'9adel's\
fundamental work.  However, the insight into formalization\
sparked by G\'9adel's original work is now having major\
payoffs in mechanized mathematics and proof systems.\
The lecture will survey some developments, but it will\
also bring up the questions of what we should now regard\
as a proof and of how new proof methods develop.}