Defining De Morgan dual using $\neg: \mathbf{A}^{\text{op}} \to \mathbf{A}$

36 Views Asked by At

Preamble. Suppose $\textbf{A} = \langle A,\bot,\top,\vee,\wedge,\neg\rangle$ is a Boolean algebra. The "opposite" Boolean algebra $\textbf{A}^\text{op} = \langle A,\top,\bot,\wedge,\vee,\neg\rangle$ has the same carrier $A$ but transposes the operations, so that $\top_{\textbf{A}^\text{op}} = \bot_{\textbf{A}}$, etc. We can also adapt the standard definition of opposite functor to monotone maps between Boolean algebras: for any $f: \textbf{A} \to \textbf{B}$, define $f^\text{op}: \textbf{A}^\text{op} \to \textbf{B}^\text{op}$ to simply be $f$, understood as a function of type $A \to B$ between the carriers. This definition is "well-typed" because $\textbf{A}$ and $\textbf{A}^\text{op}$ have the same carrier.

$^\text{op}$ allows us to think of negation in two ways. First, as an order-inverting isomorphism $\neg: \textbf{A} \to \textbf{A}$ which takes $a \in A$ to its negation $\neg a \in A$. Second (for example here), as an order-preserving isomorphism of type $\textbf{A}^\text{op} \to \textbf{A}$ (or $\textbf{A} \to \textbf{A}^\text{op}$) which takes $a \in A$ to itself. In this latter case $a \in \textbf{A}$ represents its own complement in $\textbf{A}^\text{op}$ and vice versa.

Problem. Now, for any function $g: \textbf{A} \to \textbf{B}$ between Boolean algebras, we can define its De Morgan dual:

$g^\circ: \textbf{A} \to \textbf{B} := \neg_{\textbf{B}} \circ g \circ \neg_{\textbf{A}}$

Here we mean $\neg_{\textbf{A}}$ and $\neg_{\textbf{B}}$ in the order-inverting ($\textbf{A} \to \textbf{A}$) sense rather than the order-preserving $(\textbf{A}^\text{op} \to \textbf{A})$ sense. However, I often prefer the $\textbf{A}^\text{op} \to \textbf{A}$ interpretation, and was expecting to be able to use it to define the De Morgan dual in the following way (writing $\dagger$ rather than $^\circ$ to distinguish the definitions):

$g^\dagger: \textbf{A} \to \textbf{B} := \neg_{\textbf{B}} \circ g^\text{op} \circ \neg_{\textbf{A}^\text{op}}$

Here we mean $\neg_{\textbf{B}}$ in the order-preserving ($\textbf{B} \to \textbf{B}^\text{op}$) sense where it acts as the identity on the carrier $B$. Similarly $\neg_{\textbf{A}^\text{op}}$ is the identity function on $A$ interpreted at the type $\textbf{A} \to \textbf{A}^\text{op}$.

However (and perhaps this is obvious), $\dagger$ doesn't seem to yield the same operation as $^\circ$. Indeed, $g^\dagger$ is simply another way of expressing $g$.

Consider for example the (constant) monotonic function $f: \textbf{2} \to \textbf{2}$ which maps its argument to $\text{tt}$. Here $\text{2}$ denotes the set $\{\text{ff}, \text{tt}\}$ and $\textbf{2} = \langle \text{2}, \bot, \top, \vee, \wedge, \neg\rangle$ denotes the Boolean algebra where $\bot = \text{tt}$ and $\top = \text{tt}$ and $\neg$, $\wedge$ and $\vee$ are defined in the usual way. It is easy to see that $f^\circ \neq f^{\dagger}$. Writing the type of $\text{tt}$ or $\text{ff}$ as a subscript, but omitting the subscripts on $\neg$, we have:

$f^\circ(\text{ff}_{\textbf{2}}) = \neg f(\neg \text{ff}_{\textbf{2}}) = \neg f(\text{tt}_{\textbf{2}}) = \neg\text{tt}_{\textbf{2}} = \text{ff}_{\textbf{2}}$

On the other hand:

$f^\dagger(\text{ff}_{\textbf{2}}) = \neg f^\text{op}(\neg\text{ff}_{\textbf{2}}) = \neg f^\text{op}(\text{ff}_{\textbf{2}^\text{op}}) = \neg f(\text{ff}_{\textbf{2}}) = \neg\text{tt}_{\textbf{2}} = \neg\text{tt}_{\textbf{2}^\text{op}} = \text{tt}_{\textbf{2}}$

Maybe I'm misunderstanding $f^\text{op}$. The steps above contain some suspect implicit coercions: on the way into $f^\text{op}$ we coerce $\text{ff}$ from $\textbf{2}^\text{op}$ to $\textbf{2}$ so we can pass it to $f$, and on the way out of $f^\text{op}$ we coerce the $\text{tt}$ returned by $f$ from $\textbf{2}$ to $\textbf{2}^\text{op}$. These are well-typed because $\textbf{2}^\text{op}$ and $\textbf{2}$ have the same carrier, and they make everything fit together "correctly", but not in a way that yields the De Morgan dual. Indeed, given that the identity map from $\textbf{2}^\text{op} \to \textbf{2}$ is effectively negation, we might note that $f^\text{op}$ already resembles a De Morgan dual, but at the type $\textbf{A}^\text{op} \to \textbf{B}^\text{op}$ rather than $\textbf{A} \to \textbf{B}$.

Is there a way to define the De Morgan dual of $f$ at the type $\textbf{A} \to \textbf{B}$ using negations of the form $\neg_{\textbf{A}}: \textbf{A}^\text{op} \to \textbf{A}$ and the (appropriately defined) opposite of $f$? Any corrections to my analysis above would be appreciated.

1

There are 1 best solutions below

7
On

$g^{op}$, viewed as a plain set-theoretic function from a set $A$ to a set $B$, is the same function as $g$. Similarly, $\neg_{\mathbf{A}^{op}}$ is the same function as $\neg_{\mathbf{A}}$. So $g^{\circ}$ and $g^{\dagger}$ are the same function.

Your confusion arises from the notation $\mathrm{ff}_{\mathbf{2}}$ and $\mathrm{ff}_{\mathbf{2}^{op}}$, which does not make much sense. The universe of the two algebras $\mathbf{2}$ and $\mathbf{2}^{op}$ is the same, namely $\{ \mathrm{ff}, \mathrm{tt} \}$. There is no $\mathrm{ff}_{\mathbf{2}}$ versus $\mathrm{ff}_{\mathbf{2}^{op}}$.

What does make sense is distinguishing the interpretation of the constant symbol $\bot$ in $\mathbf{2}$, which is $\mathrm{ff}$, from the interpretation of the constant symbol $\bot$ in $\mathbf{2}^{op}$, which is $\mathrm{tt}$. So one can write something like $\bot_{\mathbf{2}} = \top_{\mathbf{2}^{op}}$, but $\neg \mathrm{ff}_{\mathbf{2}} = \mathrm{ff}_{\mathbf{2}^{op}}$ is confused.