quant1
http://www.openmath.org/cd/quant1.ocd
2003-04-01
2001-03-12
2
0
official
arith1
logic1
relation1
transc1
This CD holds the definitions of the basic universal ("for all")
quantifier and existential ("there exists") quantifier. It is
intended to be `compatible' with the MathML elements representing
these quantifiers.
forall
This symbol represents the universal ("for all") quantifier which takes two
arguments. It must be placed within an OMBIND element. The first argument is the
bound variables (placed within an OMBVAR element), and the second is an expression.
An example to represents the statement for all x | |sin(x)| <= 1
exists
This symbol represents the existential ("there exists") quantifier
which takes two arguments. It must be placed within an OMBIND element. The first
argument is the bound variables (placed within an OMBVAR element), and the second
is an expression.
An example which represents the statement that there is no solution
to x^n+y^n=z^n for n>2, that is:
it is not true that there exists x,y,z,n | n>2 and x^n+y^n=z^n
2