From owner-qed Thu Oct 27 12:47:14 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id MAA27464 for qed-out; Thu, 27 Oct 1994 12:46:19 -0500
Received: from chelm.nmt.edu (chelm.nmt.edu [129.138.6.50]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id MAA27458 for <qed@mcs.anl.gov>; Thu, 27 Oct 1994 12:46:13 -0500
Received: (from yodaiken@localhost) by chelm.nmt.edu (8.6.8.1/8.6.6) id LAA12359; Thu, 27 Oct 1994 11:49:38 -0600
Message-Id: <199410271749.LAA12359@chelm.nmt.edu>
From: yodaiken@sphinx.nmt.edu (Victor Yodaiken)
Date: Thu, 27 Oct 1994 11:49:38 -0600
In-Reply-To: Randall Holmes <holmes@catseye.idbsu.edu>
       "Shuffling syntax" (Oct 27,  9:31am)
reply_to: yodaiken@chelm.nmt.edu
X-Mailer: Mail User's Shell (7.2.5 10/14/92)
To: Randall Holmes <holmes@catseye.idbsu.edu>, qed@mcs.anl.gov
Subject: Re: Shuffling syntax
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

On Oct 27,  9:31am, Randall Holmes wrote:
 Subject: Shuffling syntax
>
>It is important for those who design, maintain, and theorize about
>theorem provers to be aware that they are ultimately shuffling syntax
>(or even bit strings at the lowest level).
>
>It should be the aim for the consumer to be entirely unaware of this
>fact most of the time.  The consumer should perceive that he is proving
>theorems about mathematical objects, not that he is shuffling bit
>strings.  

Sure.