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...
Main Author: | |
---|---|
Other Authors: | |
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 |