CAP
´
ITULO 1. INTRODUC¸
˜
AO 2
apresentam sistemas de dedu¸c˜ao natural para a l´ogica linear. Troelstra, em
seu livro [Tro92], apresentou os sistemas N-CLL e N-ILL. N-CLL indica um
sistema de dedu¸c˜ao natural linear cl´assico e N-ILL um sistema de dedu¸c˜ao
natural linear intuicion´ıstico. Esses dois sistemas incluem os fragmentos adi-
tivo e multiplicativo, apesar de n˜ao oferecerem regras para os conectivos
“Par” () e “Why not” (?). Esses conectivos s˜ao tratados por defini¸c˜ao
usando as dualidades de de Morgan. Troelstra n˜ao apresentou teoremas de
normaliza¸c˜ao para os sistemas N-CLL e N-ILL.
Em [BBHdP92], Benton, Bierman, Hyland e de Paiva propuseram o sis-
tema ILL para a l´ogica linear multiplicativa intuicion´ıstica. Eles abordaram
o fragmento {1, ⊗, , !} dessa l´ogica.
Num trabalho subseq¨uente [Tro95], Troelstra repensou o trabalho apre-
sentado p or Benton et al. e introduziu o sistema ILL
+
. Os sistemas ILL e
ILL
+
diferem apenas em alguns poucos pontos. Ambos foram normalizados.
Entretanto, as provas de normaliza¸c˜ao para o sistema ILL
+
est˜ao mais no
esp´ırito da normaliza¸c˜ao proposta por Prawitz para a l´ogica modal S4.
Em [dPNdM01], de Medeiros apresentou um investiga¸c˜ao profunda sobre
tradu¸c˜oes entre l´ogicas distintas. O principal objetivo do trabalho dela foi
usar teoremas de normaliza¸c˜ao como ponto de partida para definir novas
tradu¸c˜oes. Ela propˆos o sistema NLLM, um c´alculo de dedu¸c˜ao natural para o
fragmento multiplicativo da l´ogica linear. Ela tamb´em provou a equivalˆencia
entre o sistema NLLM e o fragmento multiplicativo do c´alculo de seq¨uentes
de Girard, al´em dos teoremas de normaliza¸c˜ao e tradu¸c˜oes envolvendo esse
fragmento. Todavia, assim como em [Tro92, BBHdP92, Tro95], de Medeiros
n˜ao definiu regras para os conectivos e ?. Esses conectivos s˜ao tratados
por defini¸c˜ao.
Maraist [Mar00] propˆos o sistema NL. Esse sistema abrange quase toda a
l´ogica linear incluindo os fragmentos aditivo e multiplicativo, apesar de n˜ao
oferecer regras para o operador ?. Notavelmente, Maraist propˆos regras para
o conectivo . Contudo, essas regras s˜ao baseadas numa esp´ecie de silogismo
em virtude do fato de que uma f´ormula da forma αβ pode ser lida como
α
⊥
β ou como β
⊥
α.
Como podemos notar, nenhum dos seis sistemas mencionados acima su-
porta todos os conectivos lineares. Apenas trˆes deles (sistemas N-CLL, N-ILL
e NL) abrangem o fragmento aditivo. Por outro lado, o sistema de dedu¸c˜ao
natural que apresentamos no presente trabalho contempla toda a l´ogica li-
near, incluindo os fragmentos aditivo e multiplicativo e novas regras para os
conectivos e ?. N´os tamb´em provamos o teorema de normaliza¸c˜ao para o
nosso sistema NDLL e o princ´ıpio da subf´ormula.
Algumas das id´eias que utilizamos para elaborar nosso sistema NDLL
foram inspiradas pelo trabalho de de Medeiros [dPNdM01]. Pretendemos