OpenMath Content Dictionary: relation3

Canonical URL:

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

CD File:

relation3.ocd

CD as XML Encoded OpenMath:

relation3.omcd

Defines:

class, classes, equivalence_closure, is_equivalence, is_reflexive, is_relation, is_symmetric, is_transitive, reflexive_closure, symmetric_closure, transitive_closure

Date:

2001-03-12

Version:

2

Review Date:

2003-04-01

Status:

official

Uses CD:

arith1, logic1, nums1, set1, relation1

This CD holds the basic equivalence relation notions.

is_relation

Description:

This symbol is a boolean function of two arguments, S and R. The first argument should be a set. When applied to S and R, the function returns true if and only if the second argument is a subset of the Cartesian product of S with itself.

Commented Mathematical property (CMP):

R a subset of S x S if and only if is_relation (S,R).

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA><OMS cd="logic1" name="equivalent"/>
     <OMA><OMS cd="set1" name="subset"/>
          <OMV name="R"/>
          <OMA><OMS cd="set1" name="cartesian_product"/>
               <OMV name="S"/>
          </OMA>
     </OMA>
     <OMA><OMS cd="relation3" name="is_relation"/>
          <OMV name="S"/>
          <OMV name="R"/>
     </OMA>
</OMA>
</OMOBJ>

equivalent (subset ( R, cartesian_product ( S) ) , is_relation ( S, R) )

$$R\subset S\equiv \mathrm{is\_relation}(S,R)$$

Signatures:

sts

equivalence_closure

Description:

This symbol represents a binary function whose first argument is a set S, whose second argument is a relation R on S. When applied to S and R, it represents the smallest equivalence relation (with respect to inclusion) on S containing R.

Signatures:

sts

transitive_closure

Description:

This symbol represents a binary function whose first argument is a set S, whose second argument is a relation R on S. When applied to S and R, it represents the smallest transitive relation (with respect to inclusion) on S containing R.

Signatures:

sts

reflexive_closure

Description:

This symbol represents a binary function whose first argument is a set S, whose second argument is a relation R on S. When applied to S and R, it represents the smallest reflexive relation (with respect to inclusion) on S containing R.

Signatures:

sts

symmetric_closure

Description:

This symbol represents a binary function whose first argument is a set S, whose second argument is a relation R on S. When applied to S and R, it represents the smallest symmetric relation (with respect to inclusion) on S containing R.

Signatures:

sts

is_transitive

Description:

This symbol represents the boolean binary function which returns true if and only if the second argument is a transitive relation on the first.

Commented Mathematical property (CMP):

R is transitive on S if and only if, for all a,b,c in S with (a,b) in R and (b,c) in R, wehave (a,c) in R.

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA><OMS cd="logic1" name="equivalent"/>
     <OMA><OMS cd="relation3" name="is_transitive"/>
          <OMV name="S"/>    <OMV name="R"/>
     </OMA>
     <OMBIND><OMS cd="quant1" name="forall"/>
          <OMBVAR> <OMV name="a"/> <OMV name="b"/><OMV name="c"/>
          </OMBVAR>
          <OMA><OMS cd="logic1" name="implies"/>
               <OMA><OMS cd="logic1" name="and"/>
                    <OMA><OMS cd="set1" name="in"/>
                         <OMV name="a"/>
                         <OMV name="S"/>
                    </OMA>
                    <OMA><OMS cd="set1" name="in"/>
                         <OMV name="b"/>
                         <OMV name="S"/>
                    </OMA>
                    <OMA><OMS cd="set1" name="in"/>
                         <OMV name="c"/>
                         <OMV name="S"/>
                    </OMA>
                    <OMA><OMS cd="set1" name="in"/>
                         <OMA><OMS cd="list1" name="list"/>
                              <OMV name="a"/>  <OMV name="b"/>
                         </OMA>
                         <OMV name="R"/>
                    </OMA>
                    <OMA><OMS cd="set1" name="in"/>
                         <OMA><OMS cd="list1" name="list"/>
                              <OMV name="b"/>  <OMV name="c"/>
                         </OMA>
                         <OMV name="R"/>
                    </OMA>
               </OMA>
               <OMA><OMS cd="set1" name="in"/>
                    <OMA><OMS cd="list1" name="list"/>
                         <OMV name="a"/>  <OMV name="c"/>
                    </OMA>
                    <OMV name="R"/>
               </OMA>
          </OMA>
    </OMBIND>
</OMA>
</OMOBJ>

equivalent (is_transitive ( S, R) , forall [ a b c ] . (implies (and (in ( a, S) , in ( b, S) , in ( c, S) , in (list ( a, b) , R) , in (list ( b, c) , R) ) , in (list ( a, c) , R) ) ) )

$$\mathrm{is\_transitive}(S,R)\equiv \forall \hspace{0.17em}a,b,c.a\in S\wedge b\in S\wedge c\in S\wedge (a,b)\in R\wedge (b,c)\in R\Rightarrow (a,c)\in R$$

Signatures:

sts

is_reflexive

Description:

This symbol represents the boolean binary function which returns true if and only if the second argument is a reflexive relation on the first.

Commented Mathematical property (CMP):

is_reflexive(S,R) if and only if, for all, a in S, we have (a,a) in R.

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA><OMS cd="logic1" name="equivalent"/>
     <OMA><OMS cd="relation3" name="is_reflexive"/>
          <OMV name="S"/>    <OMV name="R"/>
     </OMA>
     <OMBIND><OMS cd="quant1" name="forall"/>
          <OMBVAR> <OMV name="a"/>
          </OMBVAR>
          <OMA><OMS cd="logic1" name="implies"/>
               <OMA><OMS cd="set1" name="in"/>
                    <OMV name="a"/>
                    <OMV name="S"/>
              </OMA>
              <OMA><OMS cd="set1" name="set"/>
                   <OMA><OMS cd="list1" name="list"/>
                        <OMV name="a"/>  <OMV name="a"/>
                   </OMA>
                   <OMV name="R"/>
              </OMA>
         </OMA>
    </OMBIND>
</OMA>
</OMOBJ>

equivalent (is_reflexive ( S, R) , forall [ a ] . (implies (in ( a, S) , set (list ( a, a) , R) ) ) )

$$\mathrm{is\_reflexive}(S,R)\equiv \forall \hspace{0.17em}a.a\in S\Rightarrow \{(a,a),R\}$$

Signatures:

sts

is_symmetric

Description:

This symbol represents the boolean binary function which returns true if and only if the second argument is a symmetric relation on the first.

Commented Mathematical property (CMP):

is_symmetric(S,R) if and only if, for all a, b in S with (a,b) in R, we have (b,a) in R.

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA><OMS cd="logic1" name="equivalent"/>
     <OMA><OMS cd="relation3" name="is_symmetric"/>
          <OMV name="S"/>    <OMV name="R"/>
     </OMA>
     <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"/>
                         <OMV name="S"/>
                    </OMA>
                    <OMA><OMS cd="set1" name="in"/>
                         <OMV name="b"/>
                         <OMV name="S"/>
                    </OMA>
                    <OMA><OMS cd="set1" name="in"/>
                         <OMA><OMS cd="list1" name="list"/>
                              <OMV name="a"/>  <OMV name="b"/>
                         </OMA>
                         <OMV name="R"/>
                    </OMA>
               </OMA>
               <OMA><OMS cd="set1" name="in"/>
                    <OMA><OMS cd="list1" name="list"/>
                         <OMV name="b"/>  <OMV name="a"/>
                    </OMA>
                    <OMV name="R"/>
               </OMA>
          </OMA>
    </OMBIND>
</OMA>
</OMOBJ>

equivalent (is_symmetric ( S, R) , forall [ a b ] . (implies (and (in ( a, S) , in ( b, S) , in (list ( a, b) , R) ) , in (list ( b, a) , R) ) ) )

$$\mathrm{is\_symmetric}(S,R)\equiv \forall \hspace{0.17em}a,b.a\in S\wedge b\in S\wedge (a,b)\in R\Rightarrow (b,a)\in R$$

Signatures:

sts

is_equivalence

Description:

This symbol represents the boolean binary function which returns true if and only if the second argument is a symmetric relation on the first.

Commented Mathematical property (CMP):

R is an equivalence relation on S if and only if R is a symmetric, reflexive, transitive relation on S.

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA><OMS cd="logic1" name="equivalent"/>
     <OMA><OMS cd="relation3" name="is_symmetric"/>
          <OMV name="S"/>    <OMV name="R"/>
     </OMA>
     <OMA><OMS cd="logic1" name="and"/>
          <OMA><OMS cd="relation3" name="is_relation"/>
               <OMV name="S"/>    <OMV name="R"/>
          </OMA>
          <OMA><OMS cd="relation3" name="is_symmetric"/>
               <OMV name="S"/>    <OMV name="R"/>
          </OMA>
          <OMA><OMS cd="relation3" name="is_reflexive"/>
               <OMV name="S"/>    <OMV name="R"/>
          </OMA>
          <OMA><OMS cd="relation3" name="is_transitive"/>
               <OMV name="S"/>    <OMV name="R"/>
          </OMA>
     </OMA>
</OMA>
</OMOBJ>

equivalent (is_symmetric ( S, R) , and (is_relation ( S, R) , is_symmetric ( S, R) , is_reflexive ( S, R) , is_transitive ( S, R) ) )

$$\mathrm{is\_symmetric}(S,R)\equiv (\mathrm{is\_relation}(S,R)\wedge \mathrm{is\_symmetric}(S,R)\wedge \mathrm{is\_reflexive}(S,R)\wedge \mathrm{is\_transitive}(S,R))$$

Signatures:

sts

class

Description:

This symbol represents a ternary function whose first argument is a set S, whose second argument is a relation R on S, and whose third argument is an element a of S. When applied to S, R, and a, it represents the set of all elements in S related to a by R, that is, the set {b in S | (a,b) in R}.

Commented Mathematical property (CMP):

class(S,R,a) = {b in S | (a,b) in R}.

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA><OMS cd="relation1" name="eq"/>
     <OMA><OMS cd="relation3" name="class"/>
          <OMV name="S"/>    <OMV name="R"/> <OMV name="a"/>
     </OMA>
     <OMA><OMS cd="set1" name="suchthat"/>
          <OMV name="S"/>
          <OMBIND><OMS cd="fns1" name="lambda"/>
               <OMBVAR> <OMV name="b"/></OMBVAR>
               <OMA><OMS cd="set1" name="in"/>
                    <OMA><OMS cd="list1" name="list"/>
                         <OMV name="a"/>  <OMV name="b"/>
                    </OMA>
                    <OMV name="R"/>
               </OMA>
          </OMBIND>
     </OMA>
</OMA>
</OMOBJ>

eq (class ( S, R, a) , suchthat ( S, lambda [ b] . (in (list ( a, b) , R) ) ) )

$$\mathrm{class}(S,R,a)=\left\{b\in S\right|(a,b)\in R\}$$

Signatures:

sts

classes

Description:

This symbol represents a binary function whose first argument is a set S, whose second argument is a relation R on S. When applied to S and R, it represents the set of all elements in S of the form class(S,R,a) for a in S.

Commented Mathematical property (CMP):

The classes of an equivalence relation R on S partition S.

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA><OMS cd="logic1" name="implies"/>
     <OMA><OMS cd="relation3" name="is_equivalence"/>
          <OMV name="S"/>    <OMV name="R"/> 
     </OMA>
     <OMBIND><OMS cd="quant1" name="forall"/>
          <OMBVAR> <OMV name="a"/> <OMV name="b"/></OMBVAR>
          <OMA><OMS cd="logic1" name="implies"/>
               <OMA><OMS cd="set1" name="in"/>
                    <OMA><OMS cd="list1" name="list"/>
                         <OMV name="a"/>  <OMV name="b"/>
                    </OMA>
                    <OMA><OMS cd="set1" name="cartesian_product"/>
                         <OMV name="S"/>  <OMV name="S"/>
                    </OMA>
               </OMA>
               <OMA><OMS cd="logic1" name="or"/>
                    <OMA><OMS cd="relation1" name="eq"/>
                         <OMA><OMS cd="set1" name="intersect"/>
                              <OMA><OMS cd="relation3" name="class"/>
                                   <OMV name="S"/><OMV name="R"/><OMV name="a"/>
                              </OMA>
                              <OMA><OMS cd="relation3" name="class"/>
                                   <OMV name="S"/>  <OMV name="R"/>  <OMV name="b"/>
                              </OMA>
                         </OMA>
                         <OMS cd="set1" name="emptyset"/>
                    </OMA>

                    <OMA><OMS cd="relation1" name="eq"/>
                         <OMA><OMS cd="relation3" name="class"/>
                              <OMV name="S"/><OMV name="R"/><OMV name="a"/>
                         </OMA>
                         <OMA><OMS cd="relation3" name="class"/>
                              <OMV name="S"/>  <OMV name="R"/>  <OMV name="b"/>
                         </OMA>
                    </OMA>
               </OMA>
          </OMA>
     </OMBIND>
 </OMA>
</OMOBJ>

implies (is_equivalence ( S, R) , forall [ a b] . (implies (in (list ( a, b) , cartesian_product ( S, S) ) , or (eq (intersect (class ( S, R, a) , class ( S, R, b) ) , emptyset) , eq (class ( S, R, a) , class ( S, R, b) ) ) ) ) )

$$\mathrm{is\_equivalence}(S,R)\Rightarrow \forall \hspace{0.17em}a,b.(a,b)\in S\times S\Rightarrow (\mathrm{class}(S,R,a)\cap \mathrm{class}(S,R,b)=\varnothing )\vee (\mathrm{class}(S,R,a)=\mathrm{class}(S,R,b))$$

Commented Mathematical property (CMP):

The classes of a reflexive relation R on S cover S, as a in S belongs to class(S,R,a).

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA><OMS cd="logic1" name="implies"/>
     <OMA><OMS cd="relation3" name="is_reflexive"/>
          <OMV name="S"/>    <OMV name="R"/> 
     </OMA>
     <OMBIND><OMS cd="quant1" name="forall"/>
          <OMBVAR> <OMV name="a"/></OMBVAR>
          <OMA><OMS cd="logic1" name="implies"/>
               <OMA><OMS cd="set1" name="in"/>
                    <OMV name="a"/> <OMV name="S"/> 
               </OMA>
               <OMA><OMS cd="set1" name="in"/>
                    <OMV name="a"/>
                    <OMA><OMS cd="relation3" name="class"/>
                         <OMV name="S"/><OMV name="R"/><OMV name="a"/>
                    </OMA>
               </OMA>
          </OMA>
     </OMBIND>
 </OMA>
</OMOBJ>

implies (is_reflexive ( S, R) , forall [ a] . (implies (in ( a, S) , in ( a, class ( S, R, a) ) ) ) )

$$\mathrm{is\_reflexive}(S,R)\Rightarrow \forall \hspace{0.17em}a.a\in S\Rightarrow a\in \mathrm{class}(S,R,a)$$

Signatures:

sts