Connectives

From Girard Reading Group

A connective builds a formula from subformulae.

Dag Prawitz resurrected Genzten's natural deduction, and was the first to explore seriously Gentzen's incidental remark that the introduction rules for a connective are "a definition" of that connective. For this idea to work out, the introduction and elimination rules have to obey certain symmetries. For example, the elimination rules cannot be "too strong" given the introduction rules, nor should they be "too weak". This idea of "harmony" between the introduction and elimination rules for a connective has also been explored by Nuel Belnap, Michael Dummett, and Per Martin-Löf, among others. Pfenning and Davies formalize the notion of "not too strong and not too weak" as local soundness and completeness.

On the other hand, saying that the introduction rules define a connective can be seen as establishing a certain bias. Dummett calls this a verificationist meaning-theory, and contrasts it with a pragmatist meaning-theory, in which the bias is towards the elimination rules (still requiring harmony with the introduction rules). This change of perspective may seem to be just a matter of taste, but Andreoli's discovery of focusing for linear logic turned it into an observable phenomena: the positive/negative polarity of a connective. Loosely speaking, positive connectives are biased towards their introduction/right rules, while negative connectives are biased towards their elimination/left rules. Formally, in a focused sequent calculus, positive connectives are invertible on the left and focused on the right, while negative connectives are invertible on the right and focused on the left.

In Ludics, all formulas are polarized. Positive formulas (P, Q, R) can be built out of positive formulas using positive connectives such as ⊕ ("plus") and ⊗ ("tensor"). Atoms (X, Y, Z) are also positive, as is the negation N^⊥ or shift ↓N of a negative formula. Negative formulas (N, M, L) can be built out of negative formulas using negative connectives such as & ("with") and ⅋ ("par"), as well as by negating P^⊥ or shifting ↑P a positive formula. There are no negative atoms, but they can be simulated with X^⊥.

Because formulas are also localized in Ludics, connectives can be additionally classified based on their action on loci. They typically come in three layers: the strictly associative connective, the partial connective, and the total connective.