3
$\begingroup$

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?

$\endgroup$
1
  • $\begingroup$ 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? $\endgroup$ – tcamps Apr 28 '15 at 21:01
2
$\begingroup$

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.

The terminology may be linked to the school of Logical Positivism in philosophy, because examples prove positive formulas and refute negative formulas.

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

$\endgroup$
2
  • $\begingroup$ I did have the sense that I might have reversed the labels. Interesting! $\endgroup$ – Zhen Lin Apr 23 '15 at 23:01
  • $\begingroup$ If you could add more details about the translation of intuitionistic logic into linear logic and explain the positive/negative distinction in linear logic, that would be much appreciated. $\endgroup$ – Zhen Lin Apr 28 '15 at 21:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.