To: QED <qed@mcs.anl.gov> Subject: Formalizing notations and context Date: Wed, 05 May 93 02:26:53 +0100 From: John Harrison <John.Harrison@cl.cam.ac.uk> Message-id: <"swan.cl.cam.:104680:930505012709"@cl.cam.ac.uk> Sender: qed-owner Precedence: bulk
I don't think it's so much formalizing mathematical *notations* that's the
problem. I agree with Bob Boyer -- my experience with HOL suggests that
embedding in lambda-calculus gives a very nice treatment of disparate uses of
bound variables (but some sloppy stuff like "the polynomial f(x)" has to go!)
Rather, I see the principal difficulty as being the large amount of informal or
semi-formal context which is traditionally associated with notations. For
example, flicking through the first few pages of Matsumura: "Commutative ring
theory" we find:
-1
"If f:A->B is a ring homomorphism and J is an ideal of B, then f (J) is an
ideal of A and we denote this by A /\ J; if A is a subring of B and f is the
inclusion map then this is the same as the usual set-theoretic notion of
intersection. In general this is not true, but confusion does not arise."
"When we say that R has characteristic p, or write char R = p, we always mean
that p > 0 is a prime number".
"In definitions and theorems about rings, it may sometimes happen that the
condition A =/= 0 is omitted even when it is actually necessary."
If one hopes to make mathematicians used to ignoring lowbrow details like this
use QED, then considerable powers of persuasion are called for. If it can't be
done, then some very difficult AI problems have to be faced!
John Harrison (jrh@cl.cam.ac.uk).