Sistemas com múltiplas conclusões pra a lógica proposicional intuicionista

Cálculos de sequentes intuicionistas são eralmente obtidos de suas contrapartes clássicas a partir de uma restrição de cardinalidade forte. Os seqüentes de sistemas intuicionistas deveriam permitir no máximo uma fórmula-ocorrência em seus conseqüentes. Mas, essa restrição de cardinalidae forte pode ser substituída por restrições locais. A restrição sobre o tamnho dos conseqüentes não precisa ser imposta sobre o proprio conceito de seqüente, mas pode ser restrita à aplicação de certas regras de inferência. O sistema LJ de Maehara é obtido do sistema LK de Gentzen através do uso deste procedimento. No entanto, mesmo as restrições locais de cardinalidade de LJ' não são essenciais. Elas podem ser substituídas por restrições sobre relações de dependência explícitas, como no cálculo de seqüentes FIL, introduzido por de Paiva e Pereira em 1993. O objetivo do presente trabalho consiste em introduzir uma versão em dedução natural (NFIL) do sistema FIL. NFIL é um sistema de dedução naural dom múltiplas conclusões para a Lógica proposicional intuicionista. Provamos normalização fraca para NFIL e mostramos que NFIL pode ser usado como uma base intuicionista adequada à formalização da Lógica de Dominios Constantes e de uma Lógica Linear intuicionista completa.