The supremum

We have seen how to use the \equiv operator to calculate with booleans. It is time to investigate another operator, the supremum, written as `\sqcup‘ and pronounced `cup’.
\sqcup has a higher binding power than \equiv which means that the expression

X\sqcup Y\ \equiv\ Z

is read as

(X\sqcup Y)\equiv Z

(Notice the greater space around \equiv in the first expression).

The first two properties of the supremum are familiar:Associativity:(X\sqcup Y)\sqcup Z\ \equiv\ X\sqcup(Y\sqcup Z)


X\sqcup Y\ \equiv\ Y\sqcup X

The next two are new:


X\sqcup X\ \equiv\ X


X\sqcup (Y\equiv Z)\ \equiv\ X\sqcup Y\ \equiv\ X\sqcup Z

Armed with these rules, we can now prove our first property concerning the supremum:Distributivity/Factoring:

X\sqcup (Y\sqcup Z)\ \equiv\ (X\sqcup Y)\sqcup (X\sqcup Z)


\quad(X\sqcup Y)\sqcup (X\sqcup Z)


\quad X\sqcup (Y\sqcup X)\sqcup Z


\quad X\sqcup (X\sqcup Y)\sqcup Z


\quad(X\sqcup X)\sqcup (Y\sqcup Z)


\quad X\sqcup (Y\sqcup Z)

Our next rule isFixed point:

X\sqcup\top\ \equiv\ \top


\quad X\sqcup\top


\quad X\sqcup(Y\equiv Y)


\quad X\sqcup Y\ \equiv\ X\sqcup Y




Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: