[om] forall

[Andrew Solomon]

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