Why are Truth, Conjunction, and Implication called "Negative" fragments of IPL (intuitionisti logic Proposition Logic)?

Question

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.

Answer 1

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.