Cálculo de seqüentes de sucedente múltiplo para lógica intuicionista de primeira ordem

A primeira apresentação de um Cálculo de Seqüentes foi feita por Gerhard Gentzen na década de 1930. Neste tipo de sistema, a diferença entre as versões clássica e intuicionista radica na cardinalidade do sucedente. O sucedente múltiplo foi tradicionalmente considerado como o elemento que representava o aspecto clássico do sistema, enquanto os seqüentes intuicionistas podiam ter, no máximo, uma fórmula no sucedente. Nas décadas seguintes foram formulados diversos cálculos intuicionistas de sucedente múltiplo que atenuaram essa restrição na cardinalidade. Na década de 1990, estudou-se a relação de conexão ou dependência entre as fórmulas de modo de assegurar o caráter intuicionista dos sistemas. Nós realizamos uma revisão dos sistemas de seqüentes intuicionistas e algumas de suas aplicações. Apresentamos a versão do sistema FIL (feita para o caso proposicional por De Paiva e Pereira) para a lógica de primeira ordem provando que o mesmo é correto, completo e satisfaz eliminação de corte.