Someone answered that negative means we are ""Using"" them .

But the point is for all of these there is an Introduction rule too. So why call them negative?

I don't know whether it's computer science or Mathematical question, but still this doubt persists.

  • 2
    $\begingroup$ At a guess, I'd say because $\top$, $\land$, and $\to$ are all coinductive (whereas $\bot$ and $\lor$ are inductive). $\endgroup$
    – Zhen Lin
    Nov 19, 2014 at 11:34

2 Answers 2


Coming at this from the perspective of Martin-Löf Type Theory, I'd say it's because they are implemented by negative types. What this means in a more general setting is that their elimination rule(s) uniquely determine(s) their introduction rule(s), as opposed to a positive type (or operator, or connective), whose introduction rule(s) uniquely determine(s) its elimination rule(s).

To explain concretely for your particular case:

  • $\land$ is a negative connective because its elimination rules $\forall P, \forall Q, P \land Q \to P$ and $\forall P, \forall Q, P \land Q \to Q$ uniquely determine its introduction rule $\forall P, \forall Q, P \to (Q \to P \land Q)$.
  • $\lor$ is a positive connective because its introduction rules $\forall P, \forall Q, P \to P \lor Q$ and $\forall P, \forall Q, P \to P \lor Q$ uniquely determine its elimination rule $\forall P, \forall Q, \forall R, (P \to R) \to ((Q \to R) \to (P \lor Q \to R))$.

Similar things apply to $\top$, $\bot$, and $\to$. That being said, $\top$ and $\land$ can both be considered positive as well, and they bifurcate when one considers linear logic.

  • 1
    $\begingroup$ In homotopy type theory lecture there was reference to a mapping out property ? How's that related in this regards . $\endgroup$
    – Pushpa
    Nov 27, 2014 at 11:21
  • $\begingroup$ A "mapping out (universal) property" is the category-theoretic way of referring to an elimination rule. Similarly, "mapping in (universal) properties" are introduction rules. This naming convention makes more sense in the context of connectives/operators/types being initial or final objects in an appropriate category (as all of them are in most reasonable incarnations of dependent type theory). $\endgroup$ Nov 27, 2014 at 19:06

Each of implication, conjunction, and truth is a "right adjoint" in categorial semantics. This means that to each of these operations is associated a category in which the operation is a final object.

Truth is final in the base category.

Conjunction of A and B is final among propositions implying both A and B separately.

Logical implication from C to D is final among propositions Z such that the conjunction of Z and C implies D.

Visually, final objects look like sinks in a category, hence they're "negative."

Positive connctives are left adjoints, hence initial, hence they look like sources in a category.

Generally speaking, the negative component is more expressive than the positive component because conjunction has a right adjoint, logical implication, while disjunction only has a left adjoint if the logic satisfies excluded middle (correct me if I'm wrong, please).


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .