OpenMath Content Dictionary: setname1

Canonical URL:
http://www.openmath.org/cd/setname1.ocd
CD File:
setname1.ocd
CD as XML Encoded OpenMath:
setname1.omcd
Defines:
C, N, P, Q, R, Z
Date:
2001-03-12
Version:
2
Review Date:
2003-04-01
Status:
official
Uses CD:
alg1, arith1, logic1, quant1, relation1, set1, nums1

This CD defines common sets of mathematics

Written by J.H. Davenport on 1999-04-18.
Revised to add Zm, GFp, GFpn on 1999-11-09.
Revised to add QuotientField and A on 1999-11-19.

P

This symbol represents the set of positive prime numbers.

Commented Mathematical property (CMP):
for all n | n is a positive prime number is equivalent to: n is a natural number and n > 1 and ((n=a*b and a and b are natural numbers) implies ((a=1 and b=n) or (b=1 and a=n)))
Formal Mathematical property (FMP):
<OMOBJ>
  <OMBIND>
    <OMS name="forall" cd="quant1"/>
    <OMBVAR>
       <OMV name="n"/>
    </OMBVAR>
    <OMA>
      <OMS name="equivalent" cd="logic1"/>
      <OMA>
        <OMS name="in" cd="set1"/>
        <OMV name="n"/>
        <OMS name="P" cd="setname1"/>
      </OMA>
      <OMA>
        <OMS name="and" cd="logic1"/>
        <OMA>
          <OMS name="in" cd="set1"/>
          <OMV name="n"/>
          <OMS name="N" cd="setname1"/>
        </OMA>
        <OMA>
          <OMS name="gt" cd="relation1"/>
          <OMV name="n"/>
          <OMS name="one" cd="alg1"/>
        </OMA>
        <OMA>
          <OMS name="implies" cd="logic1"/>
          <OMA>
            <OMS name="and" cd="logic1"/>
            <OMA>
              <OMS name="eq" cd="relation1"/>
              <OMV name="n"/>
              <OMA>
                <OMS name="times" cd="arith1"/>
                <OMV name="a"/>
                <OMV name="b"/>
              </OMA>
            </OMA>
            <OMA>
              <OMS name="in" cd="set1"/>
              <OMV name="a"/>
              <OMS name="N" cd="setname1"/>
            </OMA>
            <OMA>
              <OMS name="in" cd="set1"/>
              <OMV name="b"/>
              <OMS name="N" cd="setname1"/>
            </OMA>
          </OMA>
          <OMA>
            <OMS name="or" cd="logic1"/>
            <OMA>
              <OMS name="and" cd="logic1"/>
              <OMA>
                <OMS name="eq" cd="relation1"/>
                <OMV name="a"/>
                <OMS name="one" cd="alg1"/>
              </OMA>
              <OMA>
                <OMS name="eq" cd="relation1"/>
                <OMV name="b"/>
                <OMV name="n"/>
              </OMA>
            </OMA>
            <OMA>
              <OMS name="and" cd="logic1"/>
              <OMA>
                <OMS name="eq" cd="relation1"/>
                <OMV name="b"/>
                <OMS name="one" cd="alg1"/>
              </OMA>
              <OMA>
                <OMS name="eq" cd="relation1"/>
                <OMV name="a"/>
                <OMV name="n"/>
              </OMA>
            </OMA>
          </OMA>
        </OMA>
      </OMA>
    </OMA>
  </OMBIND>
</OMOBJ>

forall [ n ] . (equivalent (in ( n, P) , and (in ( n, N) , gt ( n, one) , implies (and (eq ( n, times ( a, b) ) , in ( a, N) , in ( b, N) ) , or (and (eq ( a, one) , eq ( b, n) ) , and (eq ( b, one) , eq ( a, n) ) ) ) ) ) )

Signatures:
sts


[Next: N] [Last: C] [Top]

N

This symbol represents the set of natural numbers (including zero).

Commented Mathematical property (CMP):
for all n | n in the natural numbers is equivalent to saying n=0 or n-1 is a natural number
Formal Mathematical property (FMP):
<OMOBJ>
  <OMBIND>
    <OMS name="forall" cd="quant1"/>
    <OMBVAR>
       <OMV name="n"/>
    </OMBVAR>
    <OMA>
      <OMS name="implies" cd="logic1"/>
      <OMA>
        <OMS name="in" cd="set1"/>
        <OMV name="n"/>
        <OMS name="N" cd="setname1"/>
      </OMA>
      <OMA>
        <OMS name="or" cd="logic1"/>
        <OMA>
          <OMS name="eq" cd="relation1"/>
          <OMV name="n"/>
          <OMS name="zero" cd="alg1"/>
        </OMA>
        <OMA>
          <OMS name="in" cd="set1"/>
          <OMA>
            <OMS name="minus" cd="arith1"/>
            <OMV name="n"/>
            <OMS name="one" cd="alg1"/>
          </OMA>
          <OMS name="N" cd="setname1"/>
        </OMA>
      </OMA>
    </OMA>
  </OMBIND>
</OMOBJ>

forall [ n ] . (implies (in ( n, N) , or (eq ( n, zero) , in (minus ( n, one) , N) ) ) )

Signatures:
sts


[Next: Z] [Previous: P] [Top]

Z

This symbol represents the set of integers, positive, negative and zero.

Commented Mathematical property (CMP):
for all z | the statements z is an integer and z is a natural number or -z is a natural number are equivalent
Formal Mathematical property (FMP):
<OMOBJ>
  <OMBIND>
    <OMS name="forall" cd="quant1"/>
    <OMBVAR>
       <OMV name="z"/>
    </OMBVAR>
    <OMA>
      <OMS name="implies" cd="logic1"/>
      <OMA>
        <OMS name="in" cd="set1"/>
        <OMV name="z"/>
        <OMS name="Z" cd="setname1"/>
      </OMA>
      <OMA>
        <OMS name="or" cd="logic1"/>
        <OMA>
          <OMS name="in" cd="set1"/>
          <OMV name="z"/>
          <OMS name="N" cd="setname1"/>
        </OMA>
        <OMA>
          <OMS name="in" cd="set1"/>
          <OMA>
            <OMS name="unary_minus" cd="arith1"/>
            <OMV name="z"/>
          </OMA>
          <OMS name="N" cd="setname1"/>
        </OMA>
      </OMA>
    </OMA>
  </OMBIND>
</OMOBJ>

forall [ z ] . (implies (in ( z, Z) , or (in ( z, N) , in (unary_minus ( z) , N) ) ) )

Signatures:
sts


[Next: Q] [Previous: N] [Top]

Q

This symbol represents the set of rational numbers.

Commented Mathematical property (CMP):
for all z where z is a rational, there exists integers p and q with q > 1 and p/q = z
Formal Mathematical property (FMP):
<OMOBJ>
  <OMBIND>
    <OMS name="forall" cd="quant1"/>
    <OMBVAR>
       <OMV name="z"/>
    </OMBVAR>
    <OMA>
      <OMS name="implies" cd="logic1"/>
      <OMA>
        <OMS name="in" cd="set1"/>
        <OMV name="z"/>
        <OMS name="Q" cd="setname1"/>
      </OMA>
      <OMBIND>
        <OMS name="exists" cd="quant1"/>
        <OMBVAR>
          <OMV name="p"/>
          <OMV name="q"/>
        </OMBVAR>
        <OMA>
          <OMS name="and" cd="logic1"/>
          <OMA>
            <OMS name="in" cd="set1"/>
            <OMV name="p"/>
            <OMS name="Z" cd="setname1"/>
          </OMA>
          <OMA>
            <OMS name="in" cd="set1"/>
            <OMV name="q"/>
            <OMS name="Z" cd="setname1"/>
          </OMA>
          <OMA>
            <OMS name="geq" cd="relation1"/>
            <OMV name="q"/>
            <OMS name="one" cd="alg1"/>
          </OMA>
          <OMA>
            <OMS name="eq" cd="relation1"/>
            <OMV name="z"/>
            <OMA>
              <OMS name="divide" cd="arith1"/>
              <OMV name="p"/>
              <OMV name="q"/>
            </OMA>
          </OMA>
        </OMA>
      </OMBIND>
     </OMA>
  </OMBIND>
</OMOBJ>

forall [ z ] . (implies (in ( z, Q) , exists [ p q ] . (and (in ( p, Z) , in ( q, Z) , geq ( q, one) , eq ( z, divide ( p, q) ) ) ) ) )

Commented Mathematical property (CMP):
for all a,b | a,b rational with a<b implies there exists rational a,c s.t. a<c and c<b
Formal Mathematical property (FMP):
<OMOBJ>
<OMBIND>
  <OMS cd="quant1" name="forall"/>
  <OMBVAR>
    <OMV name="a"/>
    <OMV name="b"/>
  </OMBVAR>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="logic1" name="and"/>
      <OMA>
        <OMS cd="set1" name="in"/>
	<OMV name="a"/>
	<OMS cd="setname1" name="Q"/>
      </OMA>
      <OMA>
        <OMS cd="set1" name="in"/>
	<OMV name="b"/>
	<OMS cd="setname1" name="Q"/>
      </OMA>
      <OMA>
        <OMS cd="relation1" name="lt"/>
	<OMV name="a"/>
	<OMV name="b"/>
      </OMA>
    </OMA>
    <OMBIND>
      <OMS cd="quant1" name="exists"/>
      <OMBVAR>
        <OMV name="c"/>
      </OMBVAR>
      <OMA>
        <OMS cd="logic1" name="and"/>
	<OMA>
	  <OMS cd="set1" name="in"/>
	  <OMV name="c"/>
	  <OMS cd="setname1" name="Q"/>
	</OMA>
	<OMA>
	  <OMS cd="relation1" name="lt"/>
	  <OMV name="a"/>
	  <OMV name="c"/>
	</OMA>
	<OMA>
	  <OMS cd="relation1" name="lt"/>
	  <OMV name="c"/>
	  <OMV name="b"/>
	</OMA>
      </OMA>
    </OMBIND>
  </OMA>
</OMBIND>
</OMOBJ>

forall [ a b ] . (implies (and (in ( a, Q) , in ( b, Q) , lt ( a, b) ) , exists [ c ] . (and (in ( c, Q) , lt ( a, c) , lt ( c, b) ) ) ) )

Signatures:
sts


[Next: R] [Previous: Z] [Top]

R

This symbol represents the set of real numbers.

Commented Mathematical property (CMP):
S \subset R and exists y in R : forall x in S x <= y) implies exists z in R such that (( forall x in S x <= z) and ((forall x in S x <= w) implies z <= w)
Formal Mathematical property (FMP):
<OMOBJ>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="logic1" name="and"/>
      <OMA>
        <OMS cd="set1" name="subset"/>
	<OMV name="S"/>
	<OMS cd="setname1" name="R"/>
      </OMA>
      <OMBIND>
        <OMS cd="quant1" name="exists"/>
	<OMBVAR>
	  <OMV name="y"/>
	</OMBVAR>
	<OMA>
	  <OMS cd="logic1" name="and"/>
	  <OMA>
	    <OMS cd="set1" name="in"/>
	    <OMV name="y"/>
	    <OMS cd="setname1" name="R"/>
	  </OMA>
	  <OMBIND>
	    <OMS cd="quant1" name="forall"/>
	    <OMBVAR>
	      <OMV name="x"/>
	    </OMBVAR>
	    <OMA>
	      <OMS cd="logic1" name="and"/>
	      <OMA>
	        <OMS cd="set1" name="in"/>
		<OMV name="x"/>
		<OMV name="S"/>
	      </OMA>
	      <OMA>
	        <OMS cd="relation1" name="leq"/>
		<OMV name="x"/>
		<OMV name="y"/>
	      </OMA>
	    </OMA>
	  </OMBIND>
	</OMA>
      </OMBIND>
    </OMA>
    <OMBIND>
      <OMS cd="quant1" name="exists"/>
      <OMBVAR>
        <OMV name="z"/>
      </OMBVAR>
      <OMA>
        <OMS cd="logic1" name="and"/>
	<OMA>
          <OMS cd="set1" name="in"/>
	  <OMV name="z"/>
	  <OMS cd="setname1" name="R"/>
	</OMA>
	<OMBIND>
	  <OMS cd="quant1" name="forall"/>
	  <OMBVAR>
	    <OMV name="x"/>
	  </OMBVAR>
	  <OMA>
	    <OMS cd="logic1" name="implies"/>
	    <OMA>
	      <OMS cd="set1" name="in"/>
	      <OMV name="x"/>
	      <OMV name="S"/>
	    </OMA>
	    <OMA>
	      <OMS cd="relation1" name="leq"/>
	      <OMV name="x"/>
	      <OMV name="z"/>
	    </OMA>
	  </OMA>
	</OMBIND>
	<OMA>
	  <OMS cd="logic1" name="implies"/>
	  <OMBIND>
	    <OMS cd="quant1" name="forall"/>
	    <OMBVAR>
	      <OMV name="x"/>
	    </OMBVAR>
	    <OMA>
	      <OMS cd="logic1" name="implies"/>
	      <OMA>
	        <OMS cd="set1" name="in"/>
		<OMV name="x"/>
		<OMV name="S"/>
	      </OMA>
	      <OMA>
	        <OMS cd="relation1" name="leq"/>
		<OMV name="x"/>
		<OMV name="w"/>
	      </OMA>
	    </OMA>
	  </OMBIND>
	  <OMA>
	    <OMS cd="relation1" name="leq"/>
	    <OMV name="z"/>
	    <OMV name="w"/>
	  </OMA>
	</OMA>
      </OMA>
    </OMBIND>
  </OMA>
</OMOBJ>

implies (and (subset ( S, R) , exists [ y ] . (and (in ( y, R) , forall [ x ] . (and (in ( x, S) , leq ( x, y) ) ) ) ) ) , exists [ z ] . (and (in ( z, R) , forall [ x ] . (implies (in ( x, S) , leq ( x, z) ) ) , implies (forall [ x ] . (implies (in ( x, S) , leq ( x, w) ) ) , leq ( z, w) ) ) ) )

Signatures:
sts


[Next: C] [Previous: Q] [Top]

C

This symbol represents the set of complex numbers.

Commented Mathematical property (CMP):
for all z | if z is complex then there exist reals x,y s.t. z = x + i * y
Formal Mathematical property (FMP):
<OMOBJ>
<OMBIND>
  <OMS cd="quant1" name="forall"/>
  <OMBVAR>
    <OMV name="z"/>
  </OMBVAR>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="set1" name="in"/>
      <OMV name="z"/>
      <OMS cd="setname1" name="C"/>
    </OMA>
    <OMBIND>
      <OMS cd="quant1" name="exists"/>
      <OMBVAR>
        <OMV name="x"/>
	<OMV name="y"/>
      </OMBVAR>
      <OMA>
        <OMS cd="logic1" name="and"/>
	<OMA>
	  <OMS cd="set1" name="in"/>
	  <OMV name="x"/>
	  <OMS cd="setname1" name="R"/>
	</OMA>
	<OMA>
	  <OMS cd="set1" name="in"/>
	  <OMV name="y"/>
	  <OMS cd="setname1" name="R"/>
	</OMA>
	<OMA>
	  <OMS cd="relation1" name="eq"/>
	  <OMV name="z"/>
	  <OMA>
	    <OMS cd="arith1" name="plus"/>
	    <OMV name="x"/>
	    <OMA>
	      <OMS cd="arith1" name="times"/>
	      <OMS cd="nums1" name="i"/>
	      <OMV name="y"/>
	    </OMA>
	  </OMA>
	</OMA>
      </OMA>
    </OMBIND>
  </OMA>
</OMBIND>
</OMOBJ>

forall [ z ] . (implies (in ( z, C) , exists [ x y ] . (and (in ( x, R) , in ( y, R) , eq ( z, plus ( x, times (i, y) ) ) ) ) ) )

Signatures:
sts


[First: P] [Previous: R] [Top]