Trace in the category of propositional statements

Question

By the result in this paper, there exists a categorification of the trace of a linear operator that generalizes to any endomorphism of a dualizable object in a symmetric monoidal category ($\textbf{Vect}^\text{Fin Dim}_k$ obviously satisfies these requirements, with every object dualizable).

Consider the category $\textbf{Prop}$ of propositional statements where the objects are statements with a well-defined truth value, and the morphisms are implication (in particular, $\operatorname{Hom}_{\textbf{Prop}}(A,B)$ is either a singleton set, when $A$ implies $B$, or empty when $A$ does not imply $B$). The categorical product of $A$ and $B$ is $A \land B$, the coproduct is $A \lor B$. The initial object of the category is $0$, the canonical false statement, which implies everything by the principle of explosion, and the terminal object is $1$, the tautology.

$\textbf{Prop}$ can be made symmetric monoidal with either $\land$ or $\lor$ as the "tensor product," with $1$ as the identity in the former, and $0$ in the latter. Objects in $\textbf{Prop}$ are dualizable in the obvious way, using $\lnot$. Every object has exactly one endomorphism, its identity. What is the trace of the identity operator of a given statement in either case?

I've tried to work this out from the definitions in the paper, but haven't had any luck. Is there some issue with the definition of this category? It's entirely possible that $\textbf{Prop}$ is not well-defined as I've defined it.

Answer 1

To start with, I just want to make sure no one gets the impression that the categorical notion of trace was introduced by the paper you linked to; however "semi-famous" it might or might not be, it's only an exposition of material that's been well-known for some time.

As to your question, your category $\bf Prop$ is also known as the Lindenbaum-Tarski algebra of the underlying logic. Assuming classical logic, it is a Boolean algebra. However, it has no interesting traces relative to either $\wedge$ or $\vee$, since it has no interesting dualizable objects: the only $\wedge$-dualizable object is $1$ and the only $\vee$-dualizable object is $0$. More generally, as noted in Example 3.6 of the paper you linked to, the only dualizable object in a cartesian monoidal category is the terminal object, and dually the only dualizable object in a cocartesian monoidal category is the initial object.

In particular, $\neg A$ is not a dual of $A$ in this categorical sense. There is a categorical sense in which $\neg A$ is a dual of $A$, but it requires treating $\bf Prop$ not as a monoidal category with respect to $\wedge$ or $\vee$ separately, but as a linearly distributive category that involves both $\wedge$ and $\vee$ together. This more general sort of dualizability is also important, but unfortunately it doesn't come along with a corresponding notion of trace.