OpenMath Content Dictionary: quant1

Canonical URL:
http://www.openmath.org/cd/quant1.ocd
CD File:
quant1.ocd
CD as XML Encoded OpenMath:
quant1.omcd
Defines:
exists, forall
Date:
2001-03-12
Version:
2
Review Date:
2003-04-01
Status:
official
Uses CD:
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.

Example:
An example to represents the statement for all x | |sin(x)| <= 1
<OMOBJ>
  <OMBIND>
    <OMS cd="quant1" name="forall"/>
    <OMBVAR>
      <OMV name="x"/>
    </OMBVAR>
    <OMA>
      <OMS cd="relation1" name="leq"/>
      <OMA>
        <OMS cd="arith1" name="abs"/>
        <OMA>
          <OMS cd="transc1" name="sin"/>
          <OMV name="x"/>
        </OMA>
      </OMA>
      <OMF dec="1.0"/>
    </OMA>
  </OMBIND>
</OMOBJ>

forall [ x ] . (leq (abs (sin ( x) ) , 1.0 ) )

Signatures:
sts


[Next: exists] [Last: exists] [Top]

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.

Example:
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
<OMOBJ>
  <OMA>
    <OMS cd="logic1" name="not"/>
    <OMBIND>
      <OMS cd="quant1" name="exists"/>
      <OMBVAR>
        <OMV name="x"/>
        <OMV name="y"/>
        <OMV name="z"/>
        <OMV name="n"/>
      </OMBVAR>
      <OMA>
        <OMS cd="logic1" name="and"/>
        <OMA>
          <OMS cd="relation1" name="gt"/>
          <OMV name="n"/>
          <OMI> 2 </OMI>
        </OMA>
        <OMA>
          <OMS cd="relation1" name="eq"/>
          <OMA>
            <OMS cd="arith1" name="plus"/>
            <OMA>
               <OMS cd="arith1" name="power"/>
               <OMV name="x"/>
               <OMV name="n"/>
            </OMA>
            <OMA>
               <OMS cd="arith1" name="power"/>
               <OMV name="y"/>
               <OMV name="n"/>
            </OMA>
          </OMA>
          <OMA>
             <OMS cd="arith1" name="power"/>
             <OMV name="z"/>
             <OMV name="n"/>
          </OMA>
        </OMA>
      </OMA>
    </OMBIND>
  </OMA>
</OMOBJ>

not (exists [ x y z n ] . (and (gt ( n, 2 ) , eq (plus (power ( x, n) , power ( y, n) ) , power ( z, n) ) ) ) )

Signatures:
sts


[First: forall] [Previous: forall] [Top]