Here are some of my latest thoughts on order-theory… such as thread-first and loop (•̀ᴗ•́)و
Discovering Heyting Algebra
We attempt to motivate the structure of a Heyting Algebra by considering ‘inverse problems’.
For example,
- You have a secret number \(x\) and your friend has a secret number \(y\), which you've communicated to each other in person.
- You communicate a ‘message’ to each other by adding onto your secret number.
- Hence, if I receive a number \(z\), then I can undo the addition operation to find the ‘message’ \(m = z - y\).
What if we decided, for security, to change our protocol from using addition to using minimum. That is, we encode our message \(m\) as \(z = x ↓ m\). Since minimum is not invertible, we decide to send our encoded messages with a ‘context’ \(c\) as a pair \((z, c)\). From this pair, a unique number \(m′\) can be extracted, which is not necessarily the original \(m\). Read on, and perhaps you'll figure out which messages can be communicated 😉
This exploration demonstrates that relative pseudo-complements
- Are admitted by the usual naturals precisely when infinity is considered a number;
- Are exactly implication for the Booleans;
- Internalises implication for sets;
- Yield the largest complementary subgraph when considering subgraphs.
In some sense, the pseudo-complement is the “best approximate inverse” to forming meets, minima, intersections.
Along the way we develop a number of the theorems describing the relationships between different structural components of Heyting Algebras; most notably the internalisation of much of its own structure.
The article aims to be self-contained, however it may be helpful to look at this lattice cheat sheet (•̀ᴗ•́)و
Life & Computing Science by Musa Al-hassy is licensed under a Creative Commons Attribution-ShareAlike 3.0 Unported License