MULTIPLE SUCCEDENT SEQUENT CALCULUS FOR INTUITIONISTIC FIRST-ORDER LOGIC

COORDENAÇÃO DE APERFEIÇOAMENTO DO PESSOAL DE ENSINO SUPERIOR === 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 fo...

Full description

Bibliographic Details
Main Author: MARIA FERNANDA PALLARES COLOMAR
Other Authors: LUIZ CARLOS PINHEIRO DIAS PEREIRA
Language:Portuguese
Published: PONTIFÍCIA UNIVERSIDADE CATÓLICA DO RIO DE JANEIRO 2007
Online Access:http://www.maxwell.vrac.puc-rio.br/Busca_etds.php?strSecao=resultado&nrSeq=11144@1
http://www.maxwell.vrac.puc-rio.br/Busca_etds.php?strSecao=resultado&nrSeq=11144@2
id ndltd-IBICT-oai-MAXWELL.puc-rio.br-11144
record_format oai_dc
spelling ndltd-IBICT-oai-MAXWELL.puc-rio.br-111442019-03-01T15:37:24Z MULTIPLE SUCCEDENT SEQUENT CALCULUS FOR INTUITIONISTIC FIRST-ORDER LOGIC CÁLCULO DE SEQÜENTES DE SUCEDENTE MÚLTIPLO PARA LÓGICA INTUICIONISTA DE PRIMEIRA ORDEM MARIA FERNANDA PALLARES COLOMAR LUIZ CARLOS PINHEIRO DIAS PEREIRA EDWARD HERMANN HAEUSLER LUIZ CARLOS PINHEIRO DIAS PEREIRA OSWALDO CHATEAUBRIAND FILHO WAGNER DE CAMPOS SANZ MARIA DA PAZ NUNES DE MEDEIROS COORDENAÇÃO DE APERFEIÇOAMENTO DO PESSOAL DE ENSINO SUPERIOR 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. The first Sequent Calculus was presented by Gerhard Gentzen in the thirties. In this system, the difference between intuitionistic logic and classical logic is based on the cardinality of the succedent. Traditionally, the multiple succedent was considered the element that preserved the classical aspect of the system, while intuitionistic sequents have, at most, one formula in the succedent. In the following decades, several multiple succedent intuitionistic calculus were presented that diminish shed this st strong restriction in the cardinality of the su succedent. In the decade of 1990, this cardinality restriction was replaced by a dependency relation between the formula ocurrences in the antecedent and in the succedent of a sequent in order to ensure the intuitionistic character of the system. We make a revision of the intuitionistic systems and some of their applications. We present a version of the system FIL (accomplish shed for the propositional case by De Paiva and Pereira) for first-order logic proving that it is sound, complete and that it satisfies the cut-elimination theorem. 2007-06-26 info:eu-repo/semantics/publishedVersion info:eu-repo/semantics/doctoralThesis http://www.maxwell.vrac.puc-rio.br/Busca_etds.php?strSecao=resultado&nrSeq=11144@1 http://www.maxwell.vrac.puc-rio.br/Busca_etds.php?strSecao=resultado&nrSeq=11144@2 por info:eu-repo/semantics/openAccess PONTIFÍCIA UNIVERSIDADE CATÓLICA DO RIO DE JANEIRO PPG EM FILOSOFIA PUC-Rio BR reponame:Repositório Institucional da PUC_RIO instname:Pontifícia Universidade Católica do Rio de Janeiro instacron:PUC_RIO
collection NDLTD
language Portuguese
sources NDLTD
description COORDENAÇÃO DE APERFEIÇOAMENTO DO PESSOAL DE ENSINO SUPERIOR === 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. === The first Sequent Calculus was presented by Gerhard Gentzen in the thirties. In this system, the difference between intuitionistic logic and classical logic is based on the cardinality of the succedent. Traditionally, the multiple succedent was considered the element that preserved the classical aspect of the system, while intuitionistic sequents have, at most, one formula in the succedent. In the following decades, several multiple succedent intuitionistic calculus were presented that diminish shed this st strong restriction in the cardinality of the su succedent. In the decade of 1990, this cardinality restriction was replaced by a dependency relation between the formula ocurrences in the antecedent and in the succedent of a sequent in order to ensure the intuitionistic character of the system. We make a revision of the intuitionistic systems and some of their applications. We present a version of the system FIL (accomplish shed for the propositional case by De Paiva and Pereira) for first-order logic proving that it is sound, complete and that it satisfies the cut-elimination theorem.
author2 LUIZ CARLOS PINHEIRO DIAS PEREIRA
author_facet LUIZ CARLOS PINHEIRO DIAS PEREIRA
MARIA FERNANDA PALLARES COLOMAR
author MARIA FERNANDA PALLARES COLOMAR
spellingShingle MARIA FERNANDA PALLARES COLOMAR
MULTIPLE SUCCEDENT SEQUENT CALCULUS FOR INTUITIONISTIC FIRST-ORDER LOGIC
author_sort MARIA FERNANDA PALLARES COLOMAR
title MULTIPLE SUCCEDENT SEQUENT CALCULUS FOR INTUITIONISTIC FIRST-ORDER LOGIC
title_short MULTIPLE SUCCEDENT SEQUENT CALCULUS FOR INTUITIONISTIC FIRST-ORDER LOGIC
title_full MULTIPLE SUCCEDENT SEQUENT CALCULUS FOR INTUITIONISTIC FIRST-ORDER LOGIC
title_fullStr MULTIPLE SUCCEDENT SEQUENT CALCULUS FOR INTUITIONISTIC FIRST-ORDER LOGIC
title_full_unstemmed MULTIPLE SUCCEDENT SEQUENT CALCULUS FOR INTUITIONISTIC FIRST-ORDER LOGIC
title_sort multiple succedent sequent calculus for intuitionistic first-order logic
publisher PONTIFÍCIA UNIVERSIDADE CATÓLICA DO RIO DE JANEIRO
publishDate 2007
url http://www.maxwell.vrac.puc-rio.br/Busca_etds.php?strSecao=resultado&nrSeq=11144@1
http://www.maxwell.vrac.puc-rio.br/Busca_etds.php?strSecao=resultado&nrSeq=11144@2
work_keys_str_mv AT mariafernandapallarescolomar multiplesuccedentsequentcalculusforintuitionisticfirstorderlogic
AT mariafernandapallarescolomar calculodesequentesdesucedentemultiploparalogicaintuicionistadeprimeiraordem
_version_ 1718987094467018752