Path: utzoo!attcan!uunet!lll-winken!brutus.cs.uiuc.edu!unix.cis.pitt.edu!zaphod.mps.ohio-state.edu!swrinde!ucsd!ucrmath!x!baez
From: baez@x.ucr.edu (john baez)
Newsgroups: comp.theory
Subject: Not again
Message-ID: <3977@ucrmath.UCR.EDU>
Date: 9 Feb 90 18:45:21 GMT
References: <20433@watdragon.waterloo.edu> <2072@rex.cs.tulane.edu> <19983@netnews.upenn.edu> <1318@oravax.UUCP>
Sender: news@ucrmath.UCR.EDU
Reply-To: baez@x.UUCP (john baez)
Organization: University of California, Riverside
Lines: 16

In article <1318@oravax.UUCP> harper@oravax.UUCP (Douglas Harper) writes:
>In article <19983@netnews.upenn.edu>, aaron@grad2.cis.upenn.edu (Aaron Watters) writes:
>|Proof theories are primarily an abstract object of mathematical discussion
>| and not a used mathematical technique.


>Mr. Watters is apparently unaware of the widespread use of proof theory
>in pure and applied logic.  Two applications that readers of this
>newsgroup will immediately recognize are automated theorem proving and
>program verification.

Oy, what a straight line.  Readers of other newsgroups will
immediately recognize that this will drive Watters into a
fury.  

Let the battle begin again!