Z Mathematical Tool-kit

This page looks best when this and this X are about the same size: X. See these viewing tips.

The Z mathematical tool-kit is a collection of types and operators somewhat like a standard library of types and functions in a programming language.

The definitions in the tool-kit build up all the Z operators from a few fundamental constructs in logic and set theory.

The tool-kit uses generic definitions very heavily: X, Y, and Z stand for any type, S and T are sets of any type, and Q and R are binary relations between any two types. The toolkit also makes extensive use of patterns in abbreviation definitions, for example it defines the binary relation symbol by X Y == (X Y).

In a few places I've used English paraphrases for predicates, where the formal definition uses constructs or concepts not defined here.

These selections from the tool-kit are based on the Reference Manual, which defines additional types and operators.

Sets

Glossary

	-	Empty set: a set that has no elements
`x S`	-	Non-membership: `x` is not an element of `S`
`S T`	-	Subset: all elements of `S` belong to `T`
`S T`	-	Proper subset: `S` is a subset of `T` and `S` is not equal to `T`
`S T`	-	Union: the set of elements in either `S` or `T`
`S T`	-	Intersection: the set of elements in both `S` and `T`
`S \ T`	-	Set difference: the set of elements in `S` that are not in `T`

Definitions

$\emptyset$ [X] == { x: X | false }

$\begin{gendef}$		[X]





		_ $\notin$ _ : X $\rel$ $\power$ X
		_ $\subseteq$ _, _ $\subset$ _ : $\power$ X $\rel$ $\power$ X
		_ $\cup$ _ , _ $\cap$ _, _ \ _: $\power$ X $\cross$ $\power$ X $\fun$ $\power$ X

	$\where$

		$\forall$ x: X; S, T: $\power$ X

		x $\notin$ S $\iff$ $\lnot$ (x $\in$ X) $\land$

		(S $\subseteq$ T $\iff$ ( $\forall$ x: X x $\in$ S $\implies$ x $\in$ T)) $\land$

		(S $\subset$ T $\iff$ S $\subseteq$ T $\land$ S $\neq$ T) $\land$

		S $\cup$ T = { x: X \| x $\in$ S $\lor$ X $\in$ T } $\land$

		S $\cap$ T = { x: X \| x $\in$ S $\land$ X $\in$ T } $\land$

		S \ T = { x: X \| x $\in$ S $\land$ X $\notin$ T }


	$\end{gendef}$

Pairs and binary relations I

Glossary

`(x,y)`	-	The pair `x`,`y`
`x y`	-	Maplet: `x` maps to `y`, same as `(x,y)`
`first p`	-	First element of pair `p`
`second p`	-	Second element of pair `p`
`id X`	-	Identity relation
`X Y`	-	Binary relation
`dom R`	-	Domain: the set of first elements of all pairs in `R`
`ran R`	-	Range: the set of second elements of all pairs in `R`

Definitions

X $\rel$ Y == $\power$ (X $\cross$ Y)

id X == { x: X

x $\mapsto$ x }

$\begin{gendef}$		[X,Y]





		first: X $\cross$ Y $\fun$ X
		second: X $\cross$ Y $\fun$ Y
		_ $\mapsto$ _ : X $\cross$ Y $\fun$ X $\cross$ Y
		dom: (X $\rel$ Y) $\fun$ $\power$ X
		ran: (X $\rel$ Y) $\fun$ $\power$ Y

	$\where$

		$\forall$ x: X; y: Y; R: X $\rel$ Y

		first(x,y) = x $\land$

		second(x,y) = y $\land$

		x $\mapsto$ y = (x,y) $\land$

		dom R = { x: X; y: Y \| x R y x } $\land$

		ran R = { x: X; y: Y \| x R y y }


	$\end{gendef}$

Pairs and binary relations II

Glossary

`S R`	-	Domain restriction: the pairs in `R` whose first element is in `S`
`R T`	-	Range restriction: the pairs in `R` whose second element is in `T`
`S R`	-	Domain antirestriction: the pairs in `R` whose first element is not in `S`
`R T`	-	Range antirestriction: the pairs in `R` whose second element is not in `T`
`R ^~`	-	Relational inverse: the pairs in `R`,
		but with first and second elements exchanged
`R S`	-	Relational image: the second elements of pairs
		in `R` whose first element is in `S`.
`R Q`	-	Overriding: all pairs in `R` or `Q`,
		except pairs in `R` whose first element is also in `Q`.
`R ⁺`	-	Transitive closure of `R`

Definitions

$\begin{gendef}$		[X,Y]





		_ $\dres$ _, _ $\ndres$ _ : $\power$ X $\cross$ (X $\rel$ Y) $\fun$ X $\rel$ Y
		_ $\rres$ _, _ $\nrres$ _ : (X $\rel$ Y) $\cross$ $\power$ Y $\fun$ X $\rel$ Y
		_ ^~ : (X $\rel$ Y) $\fun$ (Y $\rel$ X)
		_ $\limg$ _ $\rimg$ : (X $\rel$ Y) $\cross$ $\power$ X $\fun$ $\power$ Y
		_ $\oplus$ _ : (X $\rel$ Y) $\cross$ (X $\rel$ Y) $\fun$ (X $\rel$ Y)
		_ ⁺ : (X $\rel$ X) $\fun$ (X $\rel$ X)

	$\where$

		$\forall$ x: X; y: Y; S: $\power$ X; T: $\power$ Y; Q, R: X $\rel$ Y

		S $\dres$ R = { x: X; y: Y \| x $\in$ S $\land$ x R y x $\mapsto$ y } $\land$

		S $\ndres$ R = { x: X; y: Y \| x $\notin$ S $\land$ x R y x $\mapsto$ y } $\land$

		R $\rres$ T = { x: X; y: Y \| x R y $\land$ y $\in$ T x $\mapsto$ y } $\land$

		R $\nrres$ T = { x: X; y: Y \| x R y $\land$ y $\notin$ T x $\mapsto$ y } $\land$

		R ^~ = { x: X; y: Y \| x R y y $\mapsto$ x } $\land$

		R $\limg$ S $\rimg$ = { x: X; y: Y \| x $\in$ S $\land$ x R y y } $\land$

		Q $\oplus$ R = ((dom R) $\ndres$ Q) $\cup$ R

		... predicate for `_ ⁺` omitted ...


	$\end{gendef}$

Pairs and binary relations III

Glossary

`Q R`	-	Relational composition: `Q` composed with `R`
`R Q`	-	Backward relational composition, same as `Q R`

Definitions

$\begin{gendef}$		[X,Y,Z]





		_ $\comp$ _ : (X $\rel$ Y) $\cross$ (Y $\rel$ Z) $\fun$ (X $\rel$ Z)
		_ $\circ$ _ : (Y $\rel$ Z) $\cross$ (X $\rel$ Y) $\fun$ (X $\rel$ Z)

	$\where$

		$\forall$ Q: X $\rel$ Y; R: Y $\rel$ Z
		Q $\comp$ R = R $\circ$ Q = { x: X; y: Y; z: Z \| x Q y $\land$ y R z x $\mapsto$ z }

	$\end{gendef}$

Numbers and arithmetic

Glossary

	-	The set of integers
	-	The set of natural numbers, starting with zero
`₁`	-	The set of strictly positive numbers, starting with one
`+,-,*`	-	Arithmetic operators: addition, subtraction, multiplication
`div,mod`	-	Arithmetic operators: integer division and remainder (modulus)
`<,`	-	Comparison: less than, less than or equal
`>,`	-	Comparison: greater than, greater than or equal
`i .. j`	-	Number range: the set of numbers starting with `i` up through `j`
`min S`	-	Mininum: the smallest element in `S`, if any
`max S`	-	Maximum: the largest element in `S`, if any
`# S`	-	Size: the number of elements in `S`
`₁`	-	Non-empty sets
	-	Finite sets

Definitions

[ $\num$ ]

$\nat$ == { n: $\num$ | n $\geq$ 0 }

$\nat$ ₁ == $\nat$ \ { 0 }

$\power$ ₁ X == { S: $\power$ X | S $\neq$ $\emptyset$ }

$\finset$ X == { S: $\power$ X | ... S is finite ... }

$\begin{axdef}$
		_ + _, _ - _, _* _ : $\num$ $\cross$ $\num$ $\fun$ $\num$
		_ div _, _ mod _ : $\num$ $\fun$ ( $\num$ \ { 0 }) $\fun$ $\num$
		_ - : $\num$ $\fun$ $\num$
		_ < _, _ $\leq$ _, _ $\geq$ _, _ > _ : $\num$ $\rel$ $\num$
		_ .. _ : $\num$ $\rel$ $\num$ $\fun$ $\power$ $\num$
		#: $\finset$ X $\fun$ $\nat$
		min, max: $\power$ ₁ $\num$ $\pfun$ $\num$

	$\where$

		$\forall$ a,b: $\num$ a .. b = { i: $\num$ \| a $\leq$ i $\leq$ b }

		... predicates for other operators omitted ...
	$\end{axdef}$

Functions

Glossary

`X Y`	-	Partial function: some members of `X` are paired with a member of `Y`
`X Y`	-	Total function: every member of `X` is paired with a member of `Y`
`X Y`	-	Partial injection: some members of `X` are paired with different members of `Y`
`X Y`	-	Total injection: every member of `X` is paired with a different member of `Y`
`X Y`	-	Bijection: every member of `X` is paired with a different member of `Y`,
		covering all `Y`'s

Definitions

X $\pfun$ Y == { f: X $\rel$ Y | Each member of X appears no more than once. }

X $\fun$ Y == { f: X $\pfun$ Y | dom f = X }

X $\pinj$ Y == { f: X $\pfun$ Y | Each member of X is paired with a different member of Y. }

X $\inj$ Y == (X $\pinj$ Y) $\cap$ (X $\fun$ Y)

X $\bij$ Y == ... definition omitted ...

Sequences

Glossary

`seq X`	-	Sequence: the set of all sequences of `X`'s
`seq₁ X`	-	Non-empty sequence: the set of all sequences of `X`'s
		with at least one element
`iseq X`	-	Injective sequence: the set of all sequences of `X`'s
		where each element of `X` appears only once
`s t`	-	Concatenation: sequence `s` with sequence `t` appended
`head s`	-	Head: the first element of sequence `s`
`last s`	-	Last: the last element of sequence `s`
`front s`	-	Front: all but the last element of sequence `s`
`tail s`	-	Tail: all but the first element of sequence `s`
`s in t`	-	Segment relation: the sequence `s` appears in sequence `t`

Definitions

seq X == { f: $\nat$ $\ffun$ X | dom f = 1 .. # f }

seq₁ X == { f: seq X | # f > 0 }

iseq X == seq X $\cap$ ( $\nat$ $\pinj$ X)

$\begin{gendef}$		[X]





		head, last : seq₁ X $\fun$ X
		tail, front : seq₁ X $\fun$ seq X
		_ $\cat$ _ : seq X $\cross$ seq X $\fun$ seq X
		_ in _ : seq X $\rel$ seq X

	$\where$

		$\forall$ s: seq₁ X; u,v: seq X

		head(s) = s(1) $\land$

		last(s) = s(# s) $\land$

		u $\cat$ v = u $\cup$ { i: dom v i + #u $\mapsto$ v(i) }

		u in v $\iff$ ( $\exists$ s,t: seq X s $\cat$ u $\cat$ t = v)

		... predicates for other operators omitted ...


	$\end{gendef}$

Other Z pages

Z2HTML tool for translating LaTeX documents with Z markup to HTML web pages.