The universe of a relation is the set of all objects occurring in some list contained in that relation.
(deffunction universe (?r) := (if (relation ?r) (setofall ?x (exists (?l) (and (member ?l ?r) (item ?x ?l))))))
A unary relation is a non-empty relation in which all lists have exactly one item.
(defrelation unary-relation (?r) := (and (not (empty ?r)) (forall (?l) (=> (member ?l ?r) (single ?l)))))
A binary relation is a non-empty relation in which all lists have exactly two
items. The inverse of a binary relation is a binary relation with all
tuples reversed. The composition of a binary relation 
and a binary
relation 
is a binary relation in which an object 
is related to an
object 
if and only if there is an object 
such that is related to
by and is related to by .
(defrelation binary-relation (?r) := (and (not (empty ?r)) (forall (?l) (=> (member ?l ?r) (double ?l)))))
(deffunction inverse (?r) := (if (binary-relation ?r) (setofall (listof ?y ?x) (holds ?r ?x ?y))))
(deffunction composition (?r1 ?r2) := (if (and (binary-relation ?r1) (binary-relation ?r2) (setofall (listof ?x ?z) (exists (?y) (and (holds ?r1 ?x ?y) (holds ?r2 ?y ?z)))))))
(defrelation one-one (?r) := (and (binary-relation ?r) (function ?r) (function (inverse ?r))))
(defrelation many-one (?r) := (and (binary-relation ?r) (function ?r)))
(defrelation one-many (?r) := (and (binary-relation ?r) (function (inverse ?r))))
(defrelation many-many (?r) := (and (binary-relation ?r) (not (function ?r)) (not (function (inverse ?r)))))
A unary function is a function with a single argument and a single value. Hence, it is also a binary relation.
(defrelation unary-function (?f) := (and (function ?f) (binary-relation ?f)))
A binary function is a function with two arguments and one value. Hence, it is a relation with three arguments.
(defrelation binary-function (?f) := (and (function ?f) (not (empty ?f)) (forall (?l) (=> (member ?l ?f) (triple ?l)))))