[pt] CÁLCULO DE SEQÜENTES DE SUCEDENTE MÚLTIPLO PARA LÓGICA INTUICIONISTA DE PRIMEIRA ORDEM

• Ano de defesa: 2008
• Autor(a) principal: MARIA FERNANDA PALLARES COLOMAR
• Tipo de documento: Tese
• Tipo de acesso: Acesso aberto
• Idioma: por
• Instituição de defesa: MAXWELL
• Palavras-chave em Português: [pt] TEORIA DA PROVA; [pt] SUCEDENTE MULTIPLO; [pt] CALCULO DE SEQUENCIAS; [pt] GENTZEN; [en] PROOF THEORY; [en] MULTIPLE SUCCEDENT; [en] SEQUENT CALCULUS; [en] GENTZEN
• Link de acesso: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=11144&idi=1; https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=11144&idi=2; http://doi.org/10.17771/PUCRio.acad.11144

[pt] 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 radicardinalidade 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 forte na cardinalidade do sucedente. Na década de 1990, estudou-se a relação de conexão ou dependência entre as fórmulas visando assegurar o caráter intuicionista dos sistemas. Nós realizamos uma revisão dos sistemas de se seqüentes intuicionistas e algumas das suas aplicações. Apresentamos a versão do sistema FIL (feita para o caso proposicional por De Paiva e Pereira) para a lógica intuicionista de primeira ordem provando que o mesmo é correto, completo e satisfaz eliminação de corte.