[om] forall
Andrew Solomon
andrew at illywhacker.net
Sun Jun 10 20:25:37 CEST 2001
This question refers to [quant1, forall].
The example in the cd is the statement:
for all x | |sin(x)| <= 1
but in order to be true, shouldn't that actually be:
for all x, (x \in R) implies (|sin(x)| <= 1 )
I wonder if it would also be nice to have a variant
of the form
forall(x, R) , |sin(x)| <= 1
This might be particurlarly nice in the case the statement is being
translated into a computer algebra system, where the system would either
want to type x or in other finite problems,
loop over R to test the statement. Then it couldn't simply
look at the thing before the "implies" because
for all x, (|sin(x)| > 1) implies not(x \in R)
would be impossible to deal with! In general, I don't think
forall in its current form could be automatically
translated into a computer algebra system.
Andrew
--
om at openmath.org - general discussion on OpenMath
Post public announcements to om-announce at openmath.org
Automatic list maintenance software at majordomo at openmath.org
Mail om-owner at openmath.org for assistance with any problems
More information about the Om
mailing list