Path: utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!swrinde!zaphod.mps.ohio-state.edu!brutus.cs.uiuc.edu!jarthur!polyslo!vlsi3b15!vax1.cc.lehigh.edu!netnews.upenn.edu!grad2.cis.upenn.edu!aaron
From: aaron@grad2.cis.upenn.edu (Aaron Watters)
Newsgroups: comp.theory
Subject: Re: Proof theory (was Re: Academic legend)
Message-ID: <20332@netnews.upenn.edu>
Date: 13 Feb 90 14:37:47 GMT
References: <20433@watdragon.waterloo.edu> <2072@rex.cs.tulane.edu> <19983@netnews.upenn.edu> <1318@oravax.UUCP> <20010@netnews.upenn.edu> <9993@dime.cs.umass.edu>
Sender: news@netnews.upenn.edu
Reply-To: aaron@grad2.cis.upenn.edu.UUCP (Aaron Watters)
Organization: University of Pennsylvania
Lines: 22

In article <9993@dime.cs.umass.edu> yodaiken@freal.cs.umass.edu (victor yodaiken) writes:
>In article <20010@netnews.upenn.edu> aaron@grad2.cis.upenn.edu.UUCP (Aaron Watters) writes:

>Look at "Bounded Arithmetic" by Sam Buss (Bibliopolis 1986)
>for an iteresting"real mathematic" use of proof theory.

I apologise for using bad terminology.  I suppose the proof of the
semidecidability of first order predicate calculus could be called
a `use' of proof theory -- and it's certainly good mathematics.
This is not the sense I meant when I said that proof theory was
seldom `used' by mathematicians.  I meant `use' in the sense of
`no sensible programmer uses turing machines.'  I.e, turing machines
are a theoretical object of study and not a practical way to implement
programs.

I should have said
that the original posting was misleading because it suggested that
mathematicians operate within the realm of formal proofs, which they
don't.  Proof theories are a theoretical object of study and not
a practical way to arrive and mathematical truth.

-aaron.