OpenMath Content Dictionary: setname2

Canonical URL:

http://www.openmath.org/cd/setname2.ocd

CD File:

setname2.ocd

CD as XML Encoded OpenMath:

setname2.omcd

Defines:

A, AlgebraicExtension, Boolean, GFp, GFpn, H, QuotientField, Zm

Date:

2000-02-02

Version:

3

Review Date:

2003-04-01

Status:

experimental

Uses CD:

alg1, arith1, logic1, polyu, quant1, relation1, setname1, set1, sts

This CD defines some 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.
AlgebraicExtension added 2003-09-16

Boolean

Description:

This symbol represents the set of Booleans. That is the truth values, true and false.

Commented Mathematical property (CMP):

for all b in the booleans | (there exists an nb in the booleans | nb not= b implies nb = not b)

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMBIND>
    <OMS cd="quant1" name="forall"/>
    <OMBVAR>
      <OMV name="b"/>
    </OMBVAR>
    <OMA>
      <OMS cd="logic1" name="implies"/>
      <OMA>
	<OMS cd="set1" name="in"/>
	<OMV name="b"/>
	<OMS cd="setname2" name="Boolean"/>
      </OMA>
      <OMBIND>
        <OMS cd="quant1" name="exists"/>
	<OMBVAR>
	  <OMV name="nb"/>
	</OMBVAR>
	<OMA>
	  <OMS cd="logic1" name="and"/>
	  <OMA>
	    <OMS cd="set1" name="in"/>
	    <OMV name="nb"/>
	    <OMS cd="setname2" name="Boolean"/>
	  </OMA>
	  <OMA>
	    <OMS cd="relation1" name="neq"/>
	    <OMV name="nb"/>
	    <OMV name="b"/>
	  </OMA>
	  <OMA>
	    <OMS cd="relation1" name="eq"/>
	    <OMV name="nb"/>
	    <OMA>
	      <OMS cd="logic1" name="not"/>
  	      <OMV name="b"/>
	    </OMA>
	 </OMA>
	</OMA>
      </OMBIND>
    </OMA>
  </OMBIND>
</OMOBJ>

forall [ b ] . (implies (in ( b, Boolean) , exists [ nb ] . (and (in ( nb, Boolean) , neq ( nb, b) , eq ( nb, not ( b) ) ) ) ) )

$$\forall \hspace{0.17em}b.b\in \mathrm{Boolean}\Rightarrow \exists \hspace{0.17em}\mathrm{nb}.\mathrm{nb}\in \mathrm{Boolean}\wedge \mathrm{nb}\ne b\wedge \mathrm{nb}=\neg b$$

Signatures:

sts

A

Description:

This symbol represents the set of algebraic numbers.

Commented Mathematical property (CMP):

The algebraic numbers are a proper subset of the reals

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS cd="set1" name="prsubset"/>
    <OMS cd="setname2" name="A"/>
    <OMS cd="setname1" name="R"/>
  </OMA>
</OMOBJ>

prsubset (A, R)

$$A\subset \mathbb{R}$$

Commented Mathematical property (CMP):

The rationals are a proper subset of the algebraic numbers

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS cd="set1" name="prsubset"/>
    <OMS cd="setname1" name="Q"/>
    <OMS cd="setname2" name="A"/>
  </OMA>
</OMOBJ>

prsubset (Q, A)

$$\mathbb{Q}\subset A$$

Signatures:

sts

Zm

Description:

This symbol represents the set of integers modulo m, where m is not necessarily a prime. It takes one argument, the integer m.

Commented Mathematical property (CMP):

for all x in the integers modulo m | there exists an n such that n is an integer and n <= m and x^n = x

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <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"/>
	<OMA>
	  <OMS cd="setname2" name="Zm"/>
	  <OMV name="m"/>
	</OMA>
      </OMA>
      <OMBIND>
        <OMS cd="quant1" name="exists"/>
	<OMBVAR>
	  <OMV name="n"/>
	</OMBVAR>
	<OMA>
	  <OMS cd="logic1" name="and"/>
	  <OMA>
	    <OMS cd="set1" name="in"/>
	    <OMV name="n"/>
	    <OMS cd="setname1" name="Z"/>
	  </OMA>
	  <OMA>
	    <OMS cd="relation1" name="leq"/>
	    <OMV name="n"/>
	    <OMV name="m"/>
	  </OMA>
	  <OMA>
	    <OMS cd="relation1" name="eq"/>
	    <OMA>
	      <OMS cd="arith1" name="power"/>
	      <OMV name="x"/>
	      <OMV name="n"/>
	    </OMA>
	    <OMV name="x"/>
	  </OMA>
	</OMA>
      </OMBIND>
    </OMA>
  </OMBIND>
</OMOBJ>

forall [ x ] . (implies (in ( x, Zm ( m) ) , exists [ n ] . (and (in ( n, Z) , leq ( n, m) , eq (power ( x, n) , x) ) ) ) )

$$\forall \hspace{0.17em}x.x\in {\mathbb{Z}}_m\Rightarrow \exists \hspace{0.17em}n.n\in \mathbb{Z}\wedge n\le m\wedge x^n=x$$

Example:

The integers mod 12:

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS name="Zm" cd="setname2"/>
    <OMI> 12 </OMI>
  </OMA>
</OMOBJ>

Zm ( 12 )

$${\mathbb{Z}}_{12}$$

Example:

The integers mod m:

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS name="Zm" cd="setname2"/>
    <OMV name="m"/>
  </OMA>
</OMOBJ>

Zm ( m)

$${\mathbb{Z}}_m$$

Example:

4*5=8 in Z mod 12

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS name="eq" cd="relation1"/>
    <OMA>
      <OMS name="times" cd="arith1"/>
      <OMATTR>
        <OMATP>
          <OMS name="type" cd="sts"/>
          <OMA>
            <OMS name="Zm" cd="setname2"/>
            <OMI> 12 </OMI>
          </OMA>
        </OMATP>
        <OMI> 4 </OMI> 
      </OMATTR>
      <OMATTR>
        <OMATP>
          <OMS name="type" cd="sts"/>
          <OMA>
            <OMS name="Zm" cd="setname2"/>
            <OMI> 12 </OMI>
          </OMA>
        </OMATP>
        <OMI> 5 </OMI> 
      </OMATTR>
    </OMA>
    <OMATTR>
      <OMATP>
        <OMS name="type" cd="sts"/>
        <OMA>
          <OMS name="Zm" cd="setname2"/>
          <OMI> 12 </OMI>
        </OMA>
      </OMATP>
      <OMI> 8 </OMI> 
    </OMATTR>
  </OMA>
</OMOBJ>

eq (times (Attrib([ type Zm ( 12 ) ], 4 ) , Attrib([ type Zm ( 12 ) ], 5 ) ) , Attrib([ type Zm ( 12 ) ], 8 ) )

$$45=8$$

Signatures:

sts

GFp

Description:

This symbol represents the finite field of integers modulo p, where p is a prime.

Commented Mathematical property (CMP):

x^p = x mod p

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS name="eq" cd="relation1"/>
    <OMA>
      <OMS name="power" cd="arith1"/>
      <OMATTR>
        <OMATP>
          <OMS name="type" cd="sts"/>
          <OMA>
            <OMS name="GFp" cd="setname2"/>
            <OMV name="p"/>
          </OMA>
        </OMATP>
       <OMV name="x"/>
      </OMATTR>
      <OMV name="p"/>
    </OMA>
    <OMATTR>
      <OMATP>
        <OMS name="type" cd="sts"/>
        <OMA>
          <OMS name="GFp" cd="setname2"/>
          <OMV name="p"/>
        </OMA>
      </OMATP>
      <OMV name="x"/>
    </OMATTR>
  </OMA>
</OMOBJ>

eq (power (Attrib([ type GFp ( p) ], x) , p) , Attrib([ type GFp ( p) ], x) )

$$x^p=x$$

Signatures:

sts

GFpn

Description:

This symbol represents the finite field with p^n elements, where p is a prime.

Example:

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS name="eq" cd="relation1"/>
    <OMA>
      <OMS name="GFp" cd="setname2"/>
      <OMV name="p"/>
    </OMA>
    <OMA>
      <OMS name="GFpn" cd="setname2"/>
      <OMV name="p"/>
      <OMS name="one" cd="alg1"/>
    </OMA>
  </OMA>
</OMOBJ>

eq (GFp ( p) , GFpn ( p, one) )

$${\mathbb{GF}}_p={\mathbb{GF}}_{p^1}$$

Signatures:

sts

QuotientField

Description:

This symbol represents the quotient field of any integral domain.

Example:

The rationals equals QuotientField(Integers)

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
<OMA>
  <OMS cd="relation1" name="eq"/>
  <OMS cd="setname1" name="Q"/>
  <OMA>
    <OMS cd="setname2" name="QuotientField"/>
    <OMS cd="setname1" name="Z"/>
  </OMA>
</OMA>
</OMOBJ>

eq (Q, QuotientField (Z) )

$$\mathbb{Q}=\mathrm{QuotientField}\left(\mathbb{Z}\right)$$

Commented Mathematical property (CMP):

R is a field iff QuotientField(R)=R

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS name="equivalent" cd="logic1"/>
    <OMA>
      <OMS name="in" cd="set1"/>
      <OMV name="R"/>
      <OMA>
        <OMS name="structure" cd="sts"/>
        <OMV name="Field"/>
      </OMA>
    </OMA>
    <OMA>
      <OMS name="eq" cd="relation1"/>
      <OMA>
        <OMS name="QuotientField" cd="setname2"/>
        <OMV name="R"/>
      </OMA>
      <OMV name="R"/>
    </OMA>
  </OMA>
</OMOBJ>

equivalent (in ( R, structure ( Field) ) , eq (QuotientField ( R) , R) )

$$R\in \mathrm{structure}\left(\mathrm{Field}\right)\equiv (\mathrm{QuotientField}\left(R\right)=R)$$

Signatures:

sts

AlgebraicExtension

Description:

This symbol represents an algebraic extension of any integral domain.

Example:

The complex numbers are the extension of the reals by a root of x^2+1

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
<OMA>
  <OMS cd="relation1" name="eq"/>
  <OMS cd="setname1" name="C"/>
  <OMA>
    <OMS cd="setname2" name="AlgebraicExtension"/>
    <OMS cd="setname1" name="R"/>
    <OMA>
      <OMS cd="polyu" name="poly_u_rep"/>
      <OMV name="x"/>
      <OMA>
        <OMS cd="polyu" name="term"/> 
	<OMI> 2 </OMI>
	<OMI> 1 </OMI>
      </OMA>
      <OMA>
        <OMS cd="polyu" name="term"/> 
	<OMI> 0 </OMI>
	<OMI> 1 </OMI>
      </OMA>
    </OMA>
  </OMA>
</OMA>
</OMOBJ>

eq (C, AlgebraicExtension (R, poly_u_rep ( x, term ( 2 , 1 ) , term ( 0 , 1 ) ) ) )

$$\mathbb{C}=\mathrm{AlgebraicExtension}(\mathbb{R},\mathrm{poly\_u\_rep}(x,\mathrm{term}(2,1),\mathrm{term}(0,1)))$$

Signatures:

sts

H

Description:

This symbol represents the set of quaternions.

Commented Mathematical property (CMP):

1 is a quaternion and there exists i,j,k s.t. i,j,k are quaternions and i^2 = j^2 = k^2 = ijk = -1 with abs(i) not = abs(j) not = abs(k) not = 1 implies for all q, q a quaternion implies there exists r_0, r_1, r_2, r_3 reals s.t. q = r_0 + r_1*i + r_2*j + r_3*k

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS cd="logic1" name="and"/>
    <OMA>
      <OMS cd="set1" name="in"/>
      <OMS cd="alg1" name="one"/>
      <OMS cd="setname2" name="H"/>
    </OMA>
    <OMBIND>
      <OMS cd="quant1" name="exists"/>
      <OMBVAR>
        <OMV name="i"/>
        <OMV name="j"/>
        <OMV name="k"/>
      </OMBVAR>
      <OMA>
	<OMS cd="logic1" name="and"/>
	<OMA>
	  <OMS cd="set1" name="in"/>
	  <OMV name="i"/>
	  <OMS cd="setname2" name="H"/>
	</OMA>
	<OMA>
	  <OMS cd="set1" name="in"/>
	  <OMV name="j"/>
	  <OMS cd="setname2" name="H"/>
	</OMA>
	<OMA>
	  <OMS cd="set1" name="in"/>
	  <OMV name="k"/>
	  <OMS cd="setname2" name="H"/>
	</OMA>
	<OMA>
	  <OMS cd="relation1" name="eq"/>
	  <OMA>
	    <OMS cd="arith1" name="power"/>
	    <OMV name="i"/>
	    <OMI> 2 </OMI>
	  </OMA>
	  <OMA>
	    <OMS cd="arith1" name="unary_minus"/>
	    <OMS cd="alg1" name="one"/>
	  </OMA>
	</OMA>
	<OMA>
	  <OMS cd="relation1" name="eq"/>
	  <OMA>
	    <OMS cd="arith1" name="power"/>
	    <OMV name="j"/>
	    <OMI> 2 </OMI>
	  </OMA>
	  <OMA>
	    <OMS cd="arith1" name="unary_minus"/>
	    <OMS cd="alg1" name="one"/>
	  </OMA>
	</OMA>
	<OMA>
	  <OMS cd="relation1" name="eq"/>
	  <OMA>
	    <OMS cd="arith1" name="power"/>
	    <OMV name="k"/>
	    <OMI> 2 </OMI>
	  </OMA>
	  <OMA>
	    <OMS cd="arith1" name="unary_minus"/>
	    <OMS cd="alg1" name="one"/>
	  </OMA>
	</OMA>
	<OMA>
	  <OMS cd="relation1" name="eq"/>
	  <OMA>
	    <OMS cd="arith1" name="times"/>
	    <OMV name="i"/>
	    <OMV name="j"/>
	    <OMV name="k"/>
	  </OMA>
	  <OMA>
	    <OMS cd="arith1" name="unary_minus"/>
	    <OMS cd="alg1" name="one"/>
	  </OMA>
	</OMA>
	<OMA>
	  <OMS cd="relation1" name="neq"/>
	  <OMA>
	    <OMS cd="arith1" name="abs"/>
	    <OMV name="i"/>
	  </OMA>
	  <OMS cd="alg1" name="one"/>
	</OMA>
	<OMA>
	  <OMS cd="relation1" name="neq"/>
	  <OMA>
	    <OMS cd="arith1" name="abs"/>
	    <OMV name="j"/>
	  </OMA>
	  <OMS cd="alg1" name="one"/>
	</OMA>
	<OMA>
	  <OMS cd="relation1" name="neq"/>
	  <OMA>
	    <OMS cd="arith1" name="abs"/>
	    <OMV name="k"/>
	  </OMA>
	  <OMS cd="alg1" name="one"/>
	</OMA>
	<OMBIND>
	  <OMS cd="quant1" name="forall"/>
	  <OMBVAR>
	    <OMV name="q"/>
	  </OMBVAR>
	  <OMA>
	    <OMS cd="logic1" name="implies"/>
	    <OMA>
	      <OMS cd="set1" name="in"/>
	      <OMV name="q"/>
	      <OMS cd="setname2" name="H"/>
	    </OMA>
	    <OMBIND>
	      <OMS cd="quant1" name="exists"/>
	      <OMBVAR>
	        <OMV name="r0"/>
	        <OMV name="r1"/>
	        <OMV name="r2"/>
	        <OMV name="r3"/>
	      </OMBVAR>
	      <OMA>
		<OMS cd="logic1" name="and"/>
		<OMA>
		  <OMS cd="set1" name="in"/>
		  <OMV name="r0"/>
		  <OMS cd="setname1" name="R"/>
		</OMA>
		<OMA>
		  <OMS cd="set1" name="in"/>
		  <OMV name="r1"/>
		  <OMS cd="setname1" name="R"/>
		</OMA>
		<OMA>
		  <OMS cd="set1" name="in"/>
		  <OMV name="r2"/>
		  <OMS cd="setname1" name="R"/>
		</OMA>
		<OMA>
		  <OMS cd="set1" name="in"/>
		  <OMV name="r3"/>
		  <OMS cd="setname1" name="R"/>
		</OMA>
	        <OMA>
	          <OMS cd="relation1" name="eq"/>
		  <OMV name="q"/>
		  <OMA>
		    <OMS cd="arith1" name="plus"/>
		    <OMV name="r0"/>
		    <OMA>
		      <OMS cd="arith1" name="times"/>
		      <OMV name="r1"/>
		      <OMV name="i"/>
		    </OMA>
		    <OMA>
		      <OMS cd="arith1" name="times"/>
		      <OMV name="r2"/>
		      <OMV name="j"/>
		    </OMA>
		    <OMA>
		      <OMS cd="arith1" name="times"/>
		      <OMV name="r3"/>
		      <OMV name="k"/>
		    </OMA>
		  </OMA>
	        </OMA>
	      </OMA>
	    </OMBIND>
	  </OMA>
	</OMBIND>
      </OMA>
    </OMBIND>
  </OMA>
</OMOBJ>

and (in (one, H) , exists [ i j k ] . (and (in ( i, H) , in ( j, H) , in ( k, H) , eq (power ( i, 2 ) , unary_minus (one) ) , eq (power ( j, 2 ) , unary_minus (one) ) , eq (power ( k, 2 ) , unary_minus (one) ) , eq (times ( i, j, k) , unary_minus (one) ) , neq (abs ( i) , one) , neq (abs ( j) , one) , neq (abs ( k) , one) , forall [ q ] . (implies (in ( q, H) , exists [ r0 r1 r2 r3 ] . (and (in ( r0, R) , in ( r1, R) , in ( r2, R) , in ( r3, R) , eq ( q, plus ( r0, times ( r1, i) , times ( r2, j) , times ( r3, k) ) ) ) ) ) ) ) ) )

$$1\in \mathbb{H}\wedge \exists \hspace{0.17em}i,j,k.i\in \mathbb{H}\wedge j\in \mathbb{H}\wedge k\in \mathbb{H}\wedge i^2=-1\wedge j^2=-1\wedge k^2=-1\wedge ijk=-1\wedge \left|i\right|\ne 1\wedge \left|j\right|\ne 1\wedge \left|k\right|\ne 1\wedge \forall \hspace{0.17em}q.q\in \mathbb{H}\Rightarrow \exists \hspace{0.17em}{r}_0,r_1,r_2,r_3.r_0\in \mathbb{R}\wedge r_1\in \mathbb{R}\wedge r_2\in \mathbb{R}\wedge r_3\in \mathbb{R}\wedge q=r_0+r_{1}i+r_{2}j+r_{3}k$$

Example:

There exists a,b in the quaternions s.t. a*b neq b*a

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMBIND>
    <OMS cd="quant1" name="exists"/>
    <OMBVAR>
      <OMV name="a"/>
      <OMV name="b"/>
    </OMBVAR>
    <OMA>
      <OMS cd="relation1" name="neq"/>
      <OMA>
        <OMS cd="arith1" name="times"/>
	<OMV name="a"/>
	<OMV name="b"/>
      </OMA>
      <OMA>
        <OMS cd="arith1" name="times"/>
	<OMV name="b"/>
	<OMV name="a"/>
      </OMA>
    </OMA>
  </OMBIND>
</OMOBJ>

exists [ a b ] . (neq (times ( a, b) , times ( b, a) ) )

$$\exists \hspace{0.17em}a,b.ab\ne ba$$

Signatures:

sts