La lògica lineal és una lògica subestructural proposada pel lògic francès Jean-Yves Girard com un refinament de la lògica clàssica i intuïcionista, que uneix les dualitats de la primera amb moltes de les propietats constructives de la segona. Tot i que la lògica també s'ha estudiat per si mateixa, en termes més generals, les idees de la lògica lineal han influït en camps com els llenguatges de programació, la semàntica de jocs i la física quàntica (perquè la lògica lineal es pot veure com la lògica de la teoria de la informació quàntica), així com en la lingüística, particularment per la seva èmfasi en la limitació de recursos, la dualitat i la interacció. miniatura|Lògica lineal vs. lògica clàssica La lògica lineal es presta a moltes presentacions, explicacions i intuïcions diferents. Des del punt de vista de la demostració, deriva d'una anàlisi del càlcul seqüencial clàssic en què els usos de la contracció i l'afebliment (les regles estructurals) es controlen acuradament. Operacionalment, això significa que la deducció lògica ja no es tracta simplement d'una col·lecció en constant expansió de "veritats" persistents, sinó també d'una manera de manipular recursos que no sempre es poden duplicar o llençar a voluntat. En termes de models denotacionals simples, la lògica lineal es pot veure com un refinament de la interpretació de la lògica intuïcionista substituint les categories cartesianes (tancades) per categories monoïdals simètriques (tancades), o la interpretació de la lògica clàssica substituint les àlgebres booleanes per C*-àlgebres.
Connectors, dualitat i polaritat Sintaxi El llenguatge de la lògica lineal clàssica (CLL) es defineix inductivament mitjançant la notació BNF
Aquí i s'estenen sobre àtoms lògics . Per les raons que s'explicaran més endavant, els connectors ⊗, ⅋, 1 i ⊥ s'anomenen multiplicatius, els connectors &, ⊕, ⊤ i 0 s'anomenen additius, i els connectors ! i ? s'anomenen exponencials . Podem utilitzar també la terminologia següent: SímbolNom⊗conjunció multiplicativavegadestensor⊕disjunció additivamésiconjunció additivaamb⅋disjunció multiplicativaparell!és clarcop?per què nomissió Els connectors binaris ⊗, ⊕, & i ⅋ són associatius i commutatius; 1 és la unitat de ⊗, 0 és la unitat de ⊕, ⊥ és la unitat de ⅋ i ⊤ és la unitat de &.
Cada proposició en CLL té un dual , definit de la següent manera:
Classificació dels connectors: afegirmulexpposició⊕ 0⊗ 1!negatiu& ⊤⅋ ⊥? Observeu que és una involució, és a dir, per a totes les proposicions. també s'anomena la negació lineal d'.
Presentació de càlcul seqüencial Una manera de definir la lògica lineal és com un càlcul seqüencial. Fem servir les lletres i per recórrer llistes finites de proposicions , també anomenades contextos . Un seqüencial situa un context a l'esquerra i a la dreta del torniquet, escrit Γ Δ . Intuïtivament, el seqüent afirma que la conjunció de implica la disjunció de (tot i que ens referim a la conjunció i disjunció "multiplicatives", com s'explica més endavant). Girard descriu la lògica lineal clàssica utilitzant només seqüents unilaterals (on el context de l'esquerra és buit), i aquí seguim aquesta presentació més econòmica. Això és possible perquè qualsevol premissa a l'esquerra d'un torniquet sempre es pot moure a l'altre costat i dualitzar.
Referències
Categoria:Lògica Categoria:Matemàtica aplicada