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

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.

• I'm new to math.stackexchange -- if someone could help with formatting the title that would be great!
– Roly
Feb 5, 2022 at 14:16
• Fixed title formatting
– Roly
Feb 5, 2022 at 14:29

$$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.

• Thanks for your comment. $¬\text{ff}_2 = \text{ff}_{2^{\text{op}}}$ refers to the action of $id_{\{\text{tt},\text{ff}\}}$ interpreted as $\neg: 2 \to 2^{\text{op}}$.
– Roly
Feb 5, 2022 at 14:57
• @Roly Well, then of course the two functions will be different, as you correctly observed. The question is then, why do you want to use the notation $\neg_{\mathbf{2}^{op}}$ to denote the identity function, rather than either the order-inverting map $\mathbf{2}^{op} \to \mathbf{2}^{op}$ or the order-preserving map $\mathbf{2} \to \mathbf{2}^{op}$? Feb 5, 2022 at 15:10
• Suppose $\neg_{A}$ by convention denotes a "covariant" endofunctor (on a poset category) of type $A^{\text{op}} \to A$. By the same convention (and the involutivity of $^\text{op}$), $\neg_{A^{\text{op}}}$ will denote a "covariant" endofunctor of type $A \to A^{\text{op}}$. I believe this is a fairly common convention. In this instance, the "implementation" of such a functor (= monotone function) is given by the identity function on the carrier set that (as you identified) is shared by $A$ and $A^{\text{op}}$.
– Roly
Feb 5, 2022 at 15:41
• @Roly But the identity map (which is what you said you want to interpret $\neg_{\mathbf{A}}$ as) is not covariant as a map $\mathbf{A}^{op} \to \mathbf{A}$. The negation is the natural covariant map $\mathbf{A}^{op} \to \mathbf{A}$. Feb 5, 2022 at 15:50
• Sorry, I meant "contravariant" in both cases in my previous comment. My bad. I'm out of my 5 mins editing time so I can't fix it.
– Roly
Feb 5, 2022 at 15:51