Return-Path: Delivery-Date: Received: from antares.mcs.anl.gov (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 20 Apr 1993 18:19:20 +0100 Received: by antares.mcs.anl.gov id AA19185 (5.65c/IDA-1.4.4 for qed-outgoing); Tue, 20 Apr 1993 12:07:13 -0500 Received: from chelm.cs.umass.edu by antares.mcs.anl.gov with SMTP id AA19178 (5.65c/IDA-1.4.4 for ); Tue, 20 Apr 1993 12:07:09 -0500 Received: by chelm.cs.umass.edu (5.65/DEC-Ultrix/4.3) id AA29743; Tue, 20 Apr 1993 13:07:02 -0400 Date: Tue, 20 Apr 1993 13:07:02 -0400 From: yodaiken@chelm.cs.umass.edu (victor yodaiken) Message-Id: <9304201707.AA29743@chelm.cs.umass.edu> To: qed@mcs.anl.gov Subject: base language Sender: qed-owner@mcs.anl.gov Precedence: bulk How about the standard language of algebra? Take Serge Lang's text, set up a few syntactic rules, and be done with it. The meaning of a term and even whether or not the term is syntactically valid could depend on the specific subsystem. Let's not inflict the horrors of formal logic notation or worse on people who want to prove theorems about something other than logic itself. One of the most appealing aspects of Goodstien/Skolem's pra is that it integrates so easily into standard mathematical practice.