Re: [Maxima-discuss] Early references on undefined variables?

[Richard F. <fa...@gm...>]

You ask ..
My question is: can you recommend good early references that discuss
this, i.e., that discuss how the notion of free/undefined variables in
CASs was invented?

.............

I don't see that as a CAS invention.

simplifying (x^2-y^2)   -  (x-y)*(x+y)  to 0 is logically asking for a
manipulation of the logical
expression

for all x in D:   (for all y in D :  (x^2-y^2)-(x-y)*(x+y) )    where the
domain D is something that supports addition, multiplication, powers...

perhaps an algorithmic reduction, that reduces to  for all x in D: for all
y in D:  0.     Or since the free variables x,y, no longer occur in
the expression,  just 0.

This logical notation  goes back to 1900 or so with logicians --   Frege
first introduced  existential and universal quantifiers, (∃*x*) and (∀*y*);

I suppose this can be related to lisp's notation  (lambda(x y) (plus (expt
x 2) (minus (expt y 2))  (minus ......)).
for which it may be useful to look at John McCarthy's paper on Recursive
Functions of Symbolic Expressions ..
  https://dl.acm.org/doi/pdf/10.1145/367177.367199

Coming up with proofs of mathematical statements by using beta reduction on
the symbolic expressions
seems unlikely to be sufficient for most computer algebra systems.

There is a (mostly distinct from this ..) community doing math proof stuff
by computer... see
https://cicm-conference.org/2022/cicm.php
which may be relevant to your inquiry.
(I think it is fairly widely recognized that the "mathematical knowledge"
community and the CAS community
share some objectives and should work together more.)

RJF