Utilisateur:JeanCASPAR/Brouillon/logique linéaire

Les connecteurs

Les connecteurs de la logique linéaire propositionnelle classique (CLL) sont :

la négation linéaire notée $A^{\bot }$ ;
une conjonction et une disjonction multiplicative : le tenseur ( $\otimes$ ) et le par ( $⅋$ ) ;
une conjonction et une disjonction additive : le avec (&) et le plus ( $\oplus$ ) ;
la flèche linéaire est définie au moyen de la négation linéaire et de la disjonction multiplicative : $A ⊸ B = A ⊥ ⅋ B$ .

Groupe identité

⊢ A, A ⊥

(axiome)

$⊢ Γ, A$	$⊢ A ⊥, Δ$
$⊢ Γ, Δ$

(coupure)

Groupe multiplicatif

$⊢ Γ, A$	$⊢ B, Δ$
$⊢ Γ, Δ$

(⊗)

⊢ Γ, A, B

⊢ Γ, A ⅋ B

(⅋)

Groupe additif

$⊢ Γ, A$	$⊢ Γ, B$
$⊢ Γ, A & B$

(&)

⊢ Γ, A i

⊢ Γ, A 1 \oplus A 1

(⊕_i)

Groupe exponentiel

⊢ Γ, ? A, ? A

⊢ Γ, ? A

(contraction)

⊢ Γ, A

⊢ Γ, ? A

(déréliction)

⊢ Γ

⊢ Γ, ? A

(affaiblissement)

⊢ ?Γ, A

⊢ ?Γ, ! A

(promotion)

Lois de De Morgan

$(A ⊥) ⊥ \equiv A$
$(A \otimes B) ⊥ \equiv A ⊥ ⅋ B ⊥$
$(A \oplus B) ⊥ \equiv A ⊥ & B ⊥$
$(! A) ⊥ \equiv ? A ⊥$

Distributivité: $A \otimes (B \oplus C) \equiv (A \otimes B) \oplus (A \otimes C)$
Isomorphisme exponentiel: $!(A & B) \equiv ! A \otimes ! B$

Remarquons que grâce aux lois de De Morgan, chacune de ces équivalences a une duale, par exemple la négation d'un pourquoi pas est le bien sûr de la négation, le par distribue sur le avec...

Pour finir voici une tautologie linéaire importante, qui n'est toutefois pas une équivalence :

Semi-distributivité: $(A \otimes (B ⅋ C)) ⊸ ((A \otimes B) ⅋ C)$

Certains des connecteurs linéaires $\otimes$ , $⅋$ et $\multimap$ ont été définis par Girard en rejetant cette propriété^{[Laquelle ?]}.

le par : $⅋$ signifie que les ressources $A$ et $B$ sont utilisables mais pas de façon conjointe ;