# 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]