base language
yodaiken@chelm.cs.umass.edu (victor yodaiken)
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
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.