1 |
[en] APPLICATIONS OF THE FIRST CONSISTENCY PROOF PRESENTED BY GENTZEN FOR PEANO ARITHMETIC / [pt] APLICAÇÕES DA PRIMEIRA PROVA DE CONSISTÊNCIA APRESENTADA POR GENTZEN PARA A ARITMÉTICA DE PEANOMARIA FERNANDA PALLARES COLOMAR 14 November 2003 (has links)
[pt] Na antologia que M.E. Szabo realizara dos trabalhos de
Gentzen e publicara em 1969 se transcrevem, em um apêndice,
algumas passagens apresentadas por Bernays ao editor
pertencentes a uma primeira prova de consistência para a
Aritmética de Peano realizada por Gentzen que não tinha
sido publicada até então. À diferença das outras provas de
consistência realizadas por Gentzen e já conhecidas na
década de trinta, esta prova não utiliza o procedimento de
indução transfinita até e0. Ao contrário, baseia-se na
definição de um processo de redução de seqüentes que se
associa sistematicamente a todo seqüente derivável
permitindo reconhecê-lo como verdadeiro. Nós reconstruímos
essa prova realizando algumas variações e estudamos o modo
pelo qual a técnica principal utilizada (a definição do
processo de redução de seqüentes) pode ser vista em
relação a resultados da lógica clássica de primeira ordem
tais como provas de completude. A parte central da nossa
dissertação é a realização de uma versão desta prova de
consistência para um sistema formal para a Aritmética de
Heyting. / [en] In the antology of Gentzens works made by M.E.Szabo and
published in 1969, we find out in an appendix, some
passages presented by Bernays to the editor. These texts
belong to a first proof of Peanos Arithmetic consistency
that Gentzen did not publish. In a different way from the
other proofs of consistency made by Gentzen and already
known in the thirties, this proof does not use the
procedure of transfinite induction up to e0. On the
contrary, it is based on the definition of a reduction
process for sequents that is systematically associated to
every derivable sequent allowing us to recognize it as a
true sequent. We reconstructed this proof making some
variations and we studied how the main technique used (the
definition of the reduction process) could be seen in
relation with other results of first order logic like
proofs of completness. The main part of our dissertation is
another version of this consistency proof for a formal
system for Heyting Arithmetic.
|
2 |
[en] MULTIPLE SUCCEDENT SEQUENT CALCULUS FOR INTUITIONISTIC FIRST-ORDER LOGIC / [pt] CÁLCULO DE SEQÜENTES DE SUCEDENTE MÚLTIPLO PARA LÓGICA INTUICIONISTA DE PRIMEIRA ORDEMMARIA FERNANDA PALLARES COLOMAR 08 January 2008 (has links)
[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.
|
Page generated in 0.0218 seconds