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)

Symmetry:

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

The next two are new:

Idempotence:

X\sqcup X\ \equiv\ X

Distributivity/Factoring:

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)

Proof

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

\equiv\quad\{associativity\}

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

\equiv\quad\{symmetry\}

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

\equiv\quad\{associativity\}

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

\equiv\quad\{idempotence\}

\quad X\sqcup (Y\sqcup Z)


Our next rule isFixed point:

X\sqcup\top\ \equiv\ \top

Proof

\quad X\sqcup\top

\equiv\quad\{(2)\}

\quad X\sqcup(Y\equiv Y)

\equiv\quad\{distributivity\}

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

\equiv\quad\{reflexivity\}

\quad\top

Advertisements

Leave a Reply

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

WordPress.com Logo

You are commenting using your WordPress.com 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: