# Positive and negative logical connectives

By inspecting the rules of inference for (intuitionistic) predicate calculus (or, alternatively, thinking about double negation translation), one sees that there is a certain dichotomy between two groups of logical connectives:

• $\top$, $\land$, $\to$, $\forall$
• $\bot$, $\lor$, $\exists$

For some reason, I have it in my mind that the first group is called positive and the second group is called negative, but I cannot find any source for this. Are these the commonly accepted names? Or at least, does it not conflict with existing terminology?

• These slides use "positive" to mean a formula built up from $\wedge,\vee,\forall,\exists$. I don't have a good sense for the context and whether this usage is supposed to be standard. Isn't "positive" used in categorical logic in your sense? – tcamps Apr 28 '15 at 21:01

In the literature on constructive and linear logic it is the other way around, although $\to$ doesn't strictly belong to either group because it isn't monotone. Troelstra's Contructivism in Mathematics defines the almost negative formulas of Heyting arithmetic as formulas that have no $\vee$ and limited use of $\exists$.
In linear logic the terminology made Wikipedia (http://en.wikipedia.org/wiki/Linear_logic). The standard translation of intuitionist logic into linear logic confirm that $\bot$,$\vee$ and $\exists$ are positive.
Linear logic started with Girard's observation that intuitionistic implication is the composition of two substructural connectives in the following way. $$A\to B\iff !A\multimap B$$ Here $!$ is a connective that allows weakening and contraction, while linear implication $\multimap$ requires that every antecedent is used exactly once in the derivation of the consequent.
The category-theoretic explanation of the polarities in linear logic is that positive connectives are left adjoints and negative connectives are right adjoints between certain categories of formulas and proofs. This works well in linear logic because conjunction $\land$ splits up into two connectives. The negative $\&$ is the Cartesian product--i.e. the right adjoint of the diagonal--while the positive $\otimes$ is the tensor product--i.e. $-\otimes A$ is right adjoint to $A\multimap-$ for each formula $A$. The $!$ connective makes up for the difference: $$!(A\& B)\iff !A\otimes !B$$