This paper contains detailed description of two consistency proofs, which state that in the system called Peano arithmetic no contradiction can be obtained. The proofs were first published in 1936 and 1938 by the German mathematician Gerhard Gentzen. For the purpose of this paper, the proofs were read and studied from the original articles called "Die Widerspruchsfreiheit der reinen Zahlentheorie" and "Neue Fassung des Widerspruchsfreiheitsbeweises für die reine Zahlentheorie". The first mentioned proof is interesting from the historical point of view. Gentzen used a natural deduction sequent calculus and ordinal numbers in an unusual form he invented. The second proof is similar to the consistency proof, which is commonly known as a consistency proof for Peano arithmetic nowadays.

Esta tesis tiene como objeto el estudio de dos temas principales: en primer lugar nos abocamos al estudio de una clase de cálculos de Gentzen, los hipersecuentes; y en segundo lugar, abordamos el estudio de ciertas lógicas a las que dan lugar las álgebras tetravalentes modales. Ambos temas quedarán relacionados, como veremos en el Capítulo III. Los hipersecuentes son una generalización natural de los secuentes ordinarios que resultan ser una herramienta muy adecuada para presentar formulaciones estilo Gentzen de diversas l´ogicas con la muy deseable propiedad de eliminación de corte (cut-elimination property). En los años recientes, el desarrollo de métodos para combinar lógicas ha recibido mucha atención, y las motivaciones para que esto suceda provienen de áreas tan disímiles como la Filosofía y las Ciencias de la Computación (ver, por ejemplo, [13] y [15]). El fibring categorial (tambi´en conocido como fibring algebraico) introducido en [55], ha demostrado ser una herramienta amplia y poderosa para combinar lógicas. Por otro lado, la clase TMA de las álgebras tetravalentes modales fue considerada por primera vez por Antonio Monteiro, y fueron estudiadas principalmente por I. Loureiro, A.V. Figallo, A. Ziliani y P. Landini. Posteriormente, J.M. Font y M. Rius en [31] se interesaron en las lógicas a las que dan lugar los aspectos reticulares de estas ´ágebras.Estos mismos autores introdujeron un cálculo de secuentes para una de estas lógicas, a saber, T ML. En el Capítulo II, presentamos un modo alternativo de formular cálculos de hipersecuentes mediante la introducción de metavariables para fórmulas, secuentes e hipersecuentes respectivamente, en el lenguaje objeto. Se introduce una categoría adecuada de cálculos de hipersecuentes y se definen ambos tipos de fibring: restringido y no restringido. Los morfismos introducidos resultar´an ser una novedosa noción de traducción entre lógicas la cual preserva meta-propiedades en un sentido fuerte. Finalmente, exploraremos algunas características de preservación, en particular mostraremos un resultado sobre la preservación por fibring de la propiedad de interpolación de Craig (CIP). En el Capítulo III, retomamos la cuestion de investigar diferentes aspectos lógicos de las TMAs. Considerando la implicación contrapositiva introducida por A. Figallo y P. Landini en [28], introducimos tres cálculos de Hilbert distintos para la lógica T ML, como así tambien, un sistema de tableau correcto y completo para la semántica de las TMAs. Los aspectos paraconsistentes de T ML tambi´en son analizados desde el punto de vista de las Logicas de la Inconsistencia Formal, introducidas por W. Carnielli y J. Marcos en [18], y posteriormente estudiadas en [17]. La lógica tetravalente modal normal T MLN es luego estudiada. Finalmente, probamos que ambas lógicas son sublógicas propias del cálculo proposicional clásico que no son maximales. En el Capitulo IV, mostramos que el cálculo de secuentes presentado por Font y Rius en [31] para T ML no tiene la propiedad de eliminación de corte. Formulamos, entonces, un cálculo de hipersecuentes correcto y completo con respecto a T ML que si tiene esta tan deseable propiedad. Finalmente, en el Capítulo V, motivados por el problema de enriquecer a T ML con una implicación deductiva, probamos que las álgebras tetravalentes modales de A. Monteiro enriquecidas con un complemento booleano coinciden con las álgebras de De Morgan enriquecidas con un complemento booleano, o equivalentemente, con las álgebras de Boole enriquecidas con una negación de De Morgan. Estas últimas son denominadas álgebras de Boole involutivas (o simétricas) (IBAs), introducidas por Gr. Moisil y principalmente estudiadas por A. Monteiro. Probamos que las IBAs son la contrapartida algebraica de la lógica modal S5 que satisface ecuaciones adicionales. De esta manera, la lógica que puede asociarse naturalmente a las IBAs es una extensión modal propia de S5. Presentamos un cálculo de Hilbert correcto y completo para esta extensión de S5 en el lenguaje de las IBAs, esto es, sin modalidades. / The aim of this thesis is the study of two main topics. In the first place we focus on the study of a particular class of Gentzen systems, the so called hypersequents; and in the second place, we address the study of certain logics which are given raised by tetravalent modal algebras. Both topics will be relate as we will see in Chapter III. Hypersequents are a natural generalization od ordinary sequents and turned out to be a very suitable tool for presenting Gentzen style formulations of diverse logics with the very desirable cut-elimination property. In recent years, methods for combining logics have gained a lot of attention, and motivations come from different areas such as Philosophy and Computer Science (see for instance [13] y [15]). Categorical fibring (also known as algebraic fibring) introduced in [55], has shown to be a very wide and powerful tool for combining logics. On the other hand, the class TMA of tetravalent modal algebras was first considered by Antonio Monteiro, and were studied mainly by I. Loureiro, A.V. Figallo, A. Ziliani and P. Landini. Later, J.M. Font and M. Rius en [31] were interested in the logics that can be defined taking into account the lattice–theoretical aspects of these algebras. These same authors introduced a sequent calculus for one of these logics, namely, T ML. In Chapter II, we present an alternative way to formulate hypersequent calculi introducing meta–variables for formulas, sequents and hypersequents, respectively, in the language. A suitable category of hypersequent calculi and both kind of fibring: constrained and unconstrained. The introduced morphisms turned out to bea novel notion of translation between logics which preserve meta–properties in a strong sense. Finally, we explore some preservation features,in particular we show a preservation result by fibring of the Craig interpolation property (CIP). In Chapter III, we retake the study of different logical aspects of TMAs. Considering the contrapositive implication introduced by A. Figallo and P. Landini in [28], we introduce three different Hilbert calculus for the logic T ML, as well as, a tableau system sound and complete with respect to the semantics of TMAs. The paraconsistent aspects of T ML also are analyzed under the point of view of Logics of Formal Inconsistency, introduced by W. Carnielli and J. Marcos in [18], and later studied in [17]. Normal modal tetravalent logic T MLN is also studied. Finally, we prove that both logics are proper sublogics of classical propositional calculus that are not maximal. In Chapter IV, we show that the sequent calculus presented by Font and Rius en [31] for T ML does not admit the cut–elimination property. So, we formulate a hypersequent calculus sound and complete with respect to T ML which does admit the so longed property. Finally, in Chapter V, motivated by the question of enrich T ML with a deductive implication, we prove that Monteiro’s tetravalent modal algebras enriched with a boolean complement coincide with De Morgan enriched with a boolean complement, or equivaxiv lently, they coincide with Boolean algebras enriched with a De Morgan negation. The latter are called involutive Boolean algebras (or symetric Boolean algebras) (IBAs), introduced by Gr. Moisil and mainly studied by A. Monteiro. We prove that IBAs are an algebraic counterpart to yhe modal logic S5 that satisfies some additional equations. So, the logic that naturally can be associated to IBAs is a proper modal extension of S5. We present a Hilbert calculus sound and complete with respect to this extension of S5 in the language of IBAs, i.e., without modalities.

[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.

[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.

Akademisk avhandling--Stockholm. Universitet. / Bibliography: p. [106]-109.

Os sistemas Q1 e Q2, desenvolvidos por Andréa Lopari?, perfazem três principais modificações na semântica clássica: primeiramente, o universo do discurso pode não estar limitado aos objetos que pertencem ao domínio de uma dada estrutura; em segundo lugar, a relação de identidade é determinada como a diagonal desse domínio (assim, tal relação pode não ser aplicável a todas as coisas sobre as quais a linguagem possa falar); em terceiro lugar, o quantificador existencial, em Q1, bem como o universal, em Q2, podem alcançar valores que estejam fora do domínio da estrutura. Como consequência, embora definida classicamente, a negação apresenta alguns comportamentos não clássicos - a negação de um predicado numa fórmula atômica, por exemplo, pode caracterizar algo maior que, e não tão bem definido quanto, o complemento da extensão desse predicado relativamente ao domínio. [...]. / The systems Q1 and Q2, developed by Andréa Lopari?, make up three main changes in classical semantics: first, the universe of discourse can be not limited by the objects that belongs to the domain of a given structure; second, the relation of identity is fixed as a diagonal of this domain (so, it may be not applicable to all things about what the language can speak); third, the existential quantifier in Q1, as well as the universal in Q2, may capture values out of the domain of the structure. As a consequence, although classically defined, the negation presents some non-classical behavior - a negated predicate in an atomic formula, for instance, may characterize something larger and not as well defined as the complement of the extension of this predicate relatively to the domain. [...].

Os sistemas Q1 e Q2, desenvolvidos por Andréa Lopari?, perfazem três principais modificações na semântica clássica: primeiramente, o universo do discurso pode não estar limitado aos objetos que pertencem ao domínio de uma dada estrutura; em segundo lugar, a relação de identidade é determinada como a diagonal desse domínio (assim, tal relação pode não ser aplicável a todas as coisas sobre as quais a linguagem possa falar); em terceiro lugar, o quantificador existencial, em Q1, bem como o universal, em Q2, podem alcançar valores que estejam fora do domínio da estrutura. Como consequência, embora definida classicamente, a negação apresenta alguns comportamentos não clássicos - a negação de um predicado numa fórmula atômica, por exemplo, pode caracterizar algo maior que, e não tão bem definido quanto, o complemento da extensão desse predicado relativamente ao domínio. [...]. / The systems Q1 and Q2, developed by Andréa Lopari?, make up three main changes in classical semantics: first, the universe of discourse can be not limited by the objects that belongs to the domain of a given structure; second, the relation of identity is fixed as a diagonal of this domain (so, it may be not applicable to all things about what the language can speak); third, the existential quantifier in Q1, as well as the universal in Q2, may capture values out of the domain of the structure. As a consequence, although classically defined, the negation presents some non-classical behavior - a negated predicate in an atomic formula, for instance, may characterize something larger and not as well defined as the complement of the extension of this predicate relatively to the domain. [...].

The thesis consists of two parts. The first one deals with Gentzen's consistency proof of 1935, especially with the impact of his cut elimination strategy on the complexity of the proof. Our analysis of Gentzen's cut elimi- nation strategy, which eliminates uppermost cuts regardless of their comple- xity, yields that, in his proof, Gentzen implicitly applies transfinite induction up to Φω(0) where Φω is the ω-th Veblen function. This is an upper bound and Φω(0) represents an upper bound on heights of cut-free infinitary deriva- tions that Gentzen constructs for sequents derivable in Peano arithmetic (PA). We currently do not know whether this is a lower bound too. The first part also contains a formalization of Gentzen's proof of 1935. Based on the formalization, we see that the transfinite induction mentioned above is the only principle used in the proof that exceeds PA. The second part compares the performance of Gentzen's and Tait's cut elimi- nation strategy in classical propositional logic. Tait's strategy reduces the cut-rank of the derivation. Since the propositional logic does not use inference rules with eigenvariables, we managed to organize the cut elimination in the way that both strategies yield identical cut-free derivations in classical propositional logic.

No description available.