4
$\begingroup$

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.

$\endgroup$
1
  • 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

Reset to default
3
$\begingroup$

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.

$\endgroup$
2
  • 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$
    – Ptharien's Flame
    Nov 27, 2014 at 19:06
1
$\begingroup$

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).

$\endgroup$
1

You must log in to answer this question.

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