[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. / [en] 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.
| Identifer | oai:union.ndltd.org:puc-rio.br/oai:MAXWELL.puc-rio.br:11144 |
| Date | 08 January 2008 |
| Creators | MARIA FERNANDA PALLARES COLOMAR |
| Contributors | LUIZ CARLOS PINHEIRO DIAS PEREIRA |
| Publisher | MAXWELL |
| Source Sets | PUC Rio |
| Language | Portuguese |
| Detected Language | English |
| Type | TEXTO |
Page generated in 0.0024 seconds