[pt] Dedução Natural para a lógica intuicionista tem sido relacionada à Teoria das Categorias através do que agora é conhecido por Lógica Categórica. Essa relação é fortemente baseada no isomorfismo de Curry-Howard entre Dedução Natural e (lambda)-Cálculo Tipado. Esta dissertação descreve alguns aspectos dessa relação com o objetivo de propor uma visão 2-categórica da Lógica Categórica. Mostramos que mesmo numa visão 2-cateórica algumas desvantagens conhecidas na Teoria das Categorias continuam valendo. Concluímos essa dissertação discutindo as vantagens de uma visão 2-categórica a partir de premissas mais fracas. / [en] Natural Deduction for intuitionistic logic has been related to Category Theory by what now is known as Categorical Logic. This relationship is strongly based on the Curry-Howard Isomorphism between Natural Deduction and typed (lambda)-Calculus. This dissertation describes some aspects of these relationship with the aim of proposing a 2-categorical view of categorical logic. We show that even under this 2-categorical view some of the drawbacks already known in ordinary Category Theory remain holding. We conclude this dissertation discussing the advantages of 2-categorical view under some weaker assumptions.

[pt] Garantir que programas são implementados de forma a cumprir uma especificação é uma questão fundamental em computação, por isso, têm sido propostos vários métodos que almejam provar a correção dos programas. Este trabalho apresenta um método, baseado no isomorfismo de Curry-Howard, que extrai conteúdos computacionais de provas intuicionistas, conhecido como síntese construtiva ou proofs-as-programs. É proposto um processo de síntese construtiva de programas, onde a extração do conteúdo computacional gera um programa em linguagem imperativa a partir de uma prova em lógica intuicionista poli-sortida, cujos axiomas definem os tipos abstratos de dados, sendo utilizado como sistema dedutivo a Dedução Natural. Também é apresentada uma prova de correção, bem como uma prova de completude do método atráves do uso de um sistema com regra ômega (computacional) para a aritmética de Heyting, concluindo com uma demonstração da relação entre o uso da indução finita no lugar da regra ômega computacional no processo de síntese. / [en] One of the main problems in computer science is to assure that programs are implemented in such a way that they satisfy a given specification. There are many studies about methods to prove correctness of programs. This work presents a method, belonging to the constructive synthesis or proofs-as-programs paradigm, that comes from the Curry- Howard isomorphism and extracts the computational contents of intuitionist proofs. The synthesis process proposed produces a program in an imperative language from a proof in many-sorted intuitionist logic, where the axioms define the abstract data types using Natural Deduction as deductive system. It is proved the correctness, as well as the completeness of the method regarding the Heyting arithmetic with ômega-rule(in its computational version). A discussion about the use of the finitary induction instead of computational ômega-rule concludes the work.

[pt] Apresentamos uma lógica para a compreensão de condicionais a partir da proximidade (PUC-Logic) que unifica as lógicas Contrafactual e Deôntica propostas por David Lewis. Propomos também um sistema de dedução natural (PUC-ND) associado a essa nova lógica. Esse sistema de inferência é correto, completo, normalizável e decidível. A completude relativa para as lógicas V e CO é apresentada para dar ênfase à abordagem unificada sobre o trabalho de Lewis. Depois disso, apresentamos uma perspectiva construtivista para mostrar que a abstração contrafactual de Lewis não exige a regra do absurdo clássico. / [en] We present a logic for Proximity-based Understanding of Conditionals (PUC-Logic) that unifies the Counterfactual and Deontic logics proposed by David Lewis. We also propose a natural deduction system (PUC-ND) associated to this new logic. This inference system is proven to be sound, complete, normalizing and decidable. The relative completeness for the V and CO logics is shown to emphasize the unified approach over the work of Lewis. We, then, present a constructive approach to counterfactuals to show that the Lewis counterfactual abstraction does not require the classical absurd rule.

[pt] Em 1978, Neil MacCormick publica o livro Legal Reasoning and Legal Theory com o principal objetivo de construir uma teoria do raciocínio jurídico (legal reasoning) descritiva e normativa que fosse compatível com o positivismo jurídico de H. L. A. Hart. O método utilizado para apresentar a teoria parte da reconstrução racional de casos concretos pré- selecionados. A análise das decisões judiciais oferece comprovações empíricas às teses de MacCormick e também indica o foco de sua teoria sobre o raciocínio jurídico: o estudo do processo de justificação judicial. É com base neste enfoque que o autor estabelece a divisão entre justificação de primeira ordem (first-order justification) e justificação de segunda ordem (second-order justification). A presente dissertação analisa apenas a justificação de primeira ordem, que está relacionada com a correção formal do raciocínio judicial. O modelo adotado para avaliar essa característica é a dedução, em especial o silogismo hipotético misto dos lógicos tradicionais. Para o autor escocês, a decisão judicial que lograr subsumir as variáveis do caso concreto nos componentes universais do fato operativo da regra jurídica, derivando como conclusão a conseqüência normativa daquela regra, estará justificada em um Estado que promove a legalidade (Rule of Law). / [en] In 1978, Neil MacCormick published the book Legal Reasoning and Legal Theory with the goal of constructing a descriptive and normative theory of legal reasoning, compatible with the legal positivism of H. L. A. Hart. The author used the rational reconstruction of concrete pre-selected cases as the method to present his theory. The analysis of judicial decisions offers empirical backing to MacCormick s theses and highlights the focus of his theory of legal reasoning: the study of the process of legal justification. Based on this focus, the author establishes the split between first-order justification and second-order justification. This dissertation only analyzes the first- order justification, which is related with the formal correction of legal reasoning. The model adopted to evaluate this characteristic is deduction, especially the mixed hypothetical syllogism of traditional logicians. According to the Scottish author, the judicial decision that attempts to subsume the variables of the concrete case in the universal components of the operative fact of the legal rule, coming to the conclusion of a normative consequence of that same rule, will be justified in a State that promotes the Rule of Law.

[pt] É um fato conhecido que provas clássicas podem ser demasiadamente grandes. Estudos em teoria da prova descobriram diferenças exponenciais entre provas normais (ou provas livres do corte) e suas respectivas provas não normais. Por outro lado, provadores automáticos de teorema usualmente se baseiam na construção de provas normais, livres de corte ou provas de corte atômico, pois tais procedimento envolvem menos escolhas. Provas de algumas tautologias são conhecidamente grandes quanto realizadas sem a regra do corte e curtas quando a utilizam. Queremos com este trabalho apresentar procedimentos para reduzir o tamanho de provas proposicionais. Neste sentido, apresentamos dois métodos. O primeiro, denominado método vertical, faz uso de axiomas de extensão e alguns casos é possível uma redução considerável no tamanho da prova. Apresentamos um procedimento que gera tais axiomas de extensão. O segundo, denominado método horizontal, adiciona fórmulas máximas por meio de unificação via substituição de variáveis proposicionais. Também apresentamos um método que gera tal unificação durante o processo de construção da prova. O primeiro método é aplicado a dedução natural enquanto o segundo à Dedução Natural e Cálculo de Seqüentes. As provas produzidas correspondem de certo modo a provas não normais (com a regra do corte). / [en] It is well-known that the size of propositional classical proofs can be huge. Proof theoretical studies discovered exponential gaps between normal or cut-free proofs and their respective non-normal proofs. The task of automatic theorem proving is, on the other hand, usually based on the construction of normal, cut-free or only-atomic-cuts proofs, since this procedure produces less alternative choices. There are familiar tautologies such that the cut-free proof is huge while the non-cut-free is small. The aim of this work is to reduce the weight of proposicional deductions. In this sense we present two methods. The fi first, namely vertical method, uses the extension axioms. We present a method that generates a such extension axiom. The second, namely horizontal method, adds suitable (propositional) unifi fications modulo variable substitutions.We also present a method that generates a such unifi fication during the proving process. The proofs produced correspond in a certain way to non normal proofs (non cut-free proofs).

[pt] O objetivo do presente texto é demonstrar a impossibilidade da dedução tanto da finitude quanto do movimento no sistema da Ética de Spinoza. O interesse por trás desse objetivo é fornecer razões que justifiquem a pertinência de atualizar a filosofia de Spinoza. Para tal o método empregado será uma leitura imanente desta obra, buscando, sempre que possível afastar compreensões exógenas de seu conteúdo. Assim, o texto se divide em cinco partes. Primeiramente, há uma introdução na qual se apresentam estes objetivos, o método empregado e a estrutura básica do trabalho. Em segundo lugar, há uma apresentação dos pressupostos relevantes para a demonstração pretendida, tais como os conceitos de: substância, atributos, modos infinitos, modos finitos, princípio de razão suficiente e conhecimento verdadeiro. Na terceira parte o problema é delimitado mais precisamente em três etapas. Inicialmente, diferenciando-o da acusação de acosmismo, feita por Hegel contra Spinoza. Em seguida, apontando a troca epistolar entre Spinoza e Tschirnhaus como instância da posição precisa dos problemas considerados, cujas formulações são lapidadas resultando em três questões. Após isso, na terceira etapa desse terceiro capítulo, se busca defender a legitimidade de se colocar tais questões, contra as pretensões de dois comentadores contemporâneos. Então, o texto segue para seu quarto ato, em uma série de etapas. Primeiramente são apresentadas e avaliadas treze tentativas contemporâneas de solucionar o problema. Elas são agrupadas em três conjuntos, cada um relacionado mormente a uma das três questões alcançadas na etapa anterior. Da consideração dessas tentativas, surgem outras críticas no interesse de estabelecer a impossibilidade de demonstrar o movimento e a finitude no sistema da Ética. Depois disso, todos os resultados obtidos nesta etapa são consolidados, num tratamento individualizado das três questões citadas, cada uma submetida a quatro etapas. Inicialmente se explica a legitimidade ou não da questão. Em seguida, se mostram os pressupostos relevantes para a questão considerada. Após isso, se demonstra positivamente o que a interpretação avançada por esta tese julga poder ser demonstrado segundo Spinoza. Por fim, se incluem as demonstrações polêmicas, em que se apresentam as insuficiências das demonstrações positivas propostas à luz dos pressupostos avançados e outros argumentos. Findo este momento do texto, o quarto capítulo segue para suas duas últimas etapas. Primeiramente a apresentação de mais duas críticas às noções de movimento e finitude em Spinoza. Após isso, para encerrar esta etapa, se inclui um diagnóstico, onde se pretende determinar o que ocasionou as dificuldades tratadas. Por fim, em quinto lugar, o texto conclui recapitulando as contribuições deste trabalho e propondo princípios sumários para uma filosofia que abre mão dos pressupostos considerados problemáticos e que, portanto, poderia lidar de outra forma com os temas do movimento e da finitude. Além disso, se apresentam algumas questões que esta direção de pensamento deixa em aberto, apontando para desenvolvimentos posteriores, enfim encerrando este trabalho. / [en] The aim of the present text is to demonstrate the impossibility of the deduction of both finitude and motion in the system of Spinoza s Ethics. The interest behind this objective is to provide reasons that justify the pertinence of updating Spinoza s philosophy. To this end, the method employed will be an immanent reading of this work, trying, whenever possible, to avoid exogenous understandings of its content. Thus, the text is divided into five parts. First, there is an introduction in which the objectives, the method used, and the basic structure of the work are presented. Secondly, there is a presentation of the relevant presuppositions for the intended demonstration, such as the concepts of: substance, attributes, infinite modes, finite modes, the principle of sufficient reason and true knowledge. In the third part the problem is delimited more precisely in three steps. Initially, differentiating it from the accusation of acosmism, made by Hegel against Spinoza. Then, pointing out the epistolary exchange between Spinoza and Tschirnhaus as an instance of the precise position of the problems considered, whose formulations are polished resulting in three questions. After that, the third stage of this third chapter seeks to defend the legitimacy of posing such questions, against the claims of two contemporary commentators. Then the text proceeds to its fourth act, in a series of steps. First, thirteen contemporary attempts to solve the problem are presented and evaluated. They are grouped into three sets, each related primarily to one of the three questions reached in the previous step. From the consideration of these attempts, further criticism arises in the interest of establishing the impossibility of demonstrating motion and finitude in the system of the Ethics. Thereafter, all the results obtained in this stage are consolidated, in an individualized treatment of the three questions cited, each subjected to four stages. Initially, the legitimacy or not of the question is explained. Next, the assumptions relevant to the issue under consideration are shown. After that, what the interpretation advanced by this thesis believes can be demonstrated according to Spinoza is positively demonstrated. Finally, the polemical demonstrations are included, in which the inadequacies of the positive demonstrations proposed in light of the presuppositions advanced and other arguments are presented. At this point in the text, the fourth chapter moves on to its last two stages. First the presentation of two more critiques of the notions of motion and finitude in Spinoza. After this, to close this stage, a diagnosis is included, where it is intended to determine what has caused the difficulties treated. Finally, in fifth place, the text concludes by recapitulating the contributions of this work and proposing in brief principles for a philosophy that gives up the assumptions considered problematic and that, therefore, could deal differently with the themes of movement and finiteness. In addition, some questions that this direction of thought leaves open are presented, pointing to further developments, finally closing this work.

[pt] Segerberg apresentou uma prova geral da completude para lógicas proposicionais. Para tal, um sistema de dedução foi definido de forma que suas regras sejam regras para um operador booleano arbitrário para uma dada lógica proposicional. Cada regra desse sistema corresponde a uma linha na tabela de verdade desse operador. Na primeira parte desse trabalho, mostramos uma extensão da ideia de Segerberg para lógicas proposicionais finito-valoradas e para lógicas não-determinísticas. Mantemos a ideia de definir um sistema de dedução cujas regras correspondam a linhas de tabelas verdade, mas ao invés de termos um tipo de regra para cada valor de verdade da lógica correspondente, usamos uma representação bivalente que usa a técnica de fórmulas separadoras definidas por Carlos Caleiro e João Marcos. O sistema definido possui tantas regras que pode ser difícil trabalhar com elas. Acreditamos que um sistema de cálculo de sequentes definido de forma análoga poderia ser mais intuitivo. Motivados por essa observação, a segunda parte dessa tese é dedicada à definição de uma tradução entre cálculo de sequentes e dedução natural, onde procuramos definir uma bijeção melhor do que as já existentes. / [en] Segerberg presented a general completeness proof for propositional logics. For this purpose, a Natural Deduction system was defined in a way that its rules were rules for an arbitrary boolean operator in a given propositional logic. Each of those rules corresponds to a row on the operator s truth-table. In the first part of this thesis we extend Segerbergs idea to finite-valued propositional logic and to non-deterministic logic. We maintain the idea of defining a deductive system whose rules correspond to rows of truth-tables, but instead of having n types of rules (one for each truth-value), we use a bivalent representation that makes use of the technique of separating formulas as defined by Carlos Caleiro and João Marcos. The system defined has so many rules it might be laborious to work with it. We believe that a sequent calculus system defined in a similar way would be more intuitive. Motivated by this observation, in the second part of this thesis we work out translations between Sequent Calculus and Natural Deduction, searching for a better bijective relationship than those already existing.

[pt] A teoria da prova tradicional da lógica proposicional trata provas cujos tamanhos podem ser demasiado grandes. Estudos teóricos de prova descobriram diferenças exponenciais entre provas normais ou livres de corte e suas respectivas provas não-normais. Assim, o uso de grafos-de-prova, ao invés de árvores ou listas, para representar provas está se tornando mais popular entre teóricos da prova. Os grafos-de-prova servem como uma forma de proporcionar uma melhor simetria para a semântica de provas e uma maneira de estudar a complexidade das provas proposicionais. O objetivo deste trabalho é reduzir o peso/tamanho de deduções. Apresentamos formalismos de grafos de prova que visam capturar a estrutura lógica de uma dedução e uma forma de facilitar a visualização das propriedades. A vantagem destes formalismos é que as fórmulas e sub-deduções em dedução natural, preservadas na estrutura de grafo, podem ser compartilhadas eliminando sub-deduções desnecessárias resultando na prova reduzida. Neste trabalho, damos uma definição precisa de grafos de prova para a lógica puramente implicacional, logo estendemos esse resultado para a lógica proposicional completa e mostramos como reduzir (eliminando fórmulas máximas) essas representações de tal forma que um teorema de normalização pode ser provado através da contagem do número de fórmulas máximas na derivação original. A normalização forte será uma consequência direta desta normalização, uma vez que qualquer redução diminui as medidas correspondentes da complexidade da derivação. Continuando com o nosso objetivo de estudar a complexidade das provas, a abordagem atual também fornece representações de grafo para lógica de primeira ordem, a inferência profunda e lógica bi-intuitionista. / [en] Traditional proof theory of Propositional Logic deals with proofs which size can be huge. Proof theoretical studies discovered exponential gaps between normal or cut free proofs and their respective non-normal proofs. Thus, the use of proof-graphs, instead of trees or lists, for representing proofs is getting popular among proof-theoreticians. Proof-graphs serve as a way to provide a better symmetry to the semantics of proofs and a way to study complexity of propositional proofs and to provide more efficient theorem provers, concerning size of propositional proofs. The aim of this work is to reduce the weight/size of deductions. We present formalisms of proof-graphs that are intended to capture the logical structure of a deduction and a way to facilitate the visualization. The advantage of these formalisms is that formulas and subdeductions in Natural Deduction, preserved in the graph structure, can be shared deleting unnecessary sub-deductions resulting in the reduced proof. In this work, we give a precise definition of proof-graphs for purely implicational logic, then we extend this result to full propositional logic and show how to reduce (eliminating maximal formulas) these representations such that a normalization theorem can be proved by counting the number of maximal formulas in the original derivation. The strong normalization will be a direct consequence of such normalization, since that any reduction decreases the corresponding measures of derivation complexity. Continuing with our aim of studying the complexity of proofs, the current approach also give graph representations for first order logic, deep inference and bi-intuitionistic logic.

[pt] Existem diferentes estilos de cálculos dedutivos, usados para derivar os teoremas de uma lógica. Os mais habituais são os sistemas axiomáticos; mas, do ponto de vista da teoria da prova, os sistemas em dedução natural parecem ser mais interessantes. Essa é a motivação que leva ao desenvolvimento de técnicas que visam a facilitar a transformação de um cálculo dedutivo para o estilo em dedução natural. Esse trabalho se concentra no aspecto de modelar regras para os quantificadores da linguagem considerada e, para isso, faz uso de rótulos. Após uma apresentação intuitiva da técnica desenvolvida, passa-se à exposição de sistemas lógicos tratados pelo método: lógica de ultrafiltros, lógica de filtros, CTL, lógica de Keisler e CTL*. Em cada caso, analisam-se aspectos de teoria da prova. / [en] There are many kinds of deductive calculus. The axiomatic ones are the more usual. However, from the point of view of proof theory, Natural Deduction systems seem to be more interesting. This is the motivation for developping a technique that aims to ease the transformation from deductive calculus to Natural Deduction style. This work concentrates on the aspect of modeling the rules for the quantifiers of the logic considered, and for this purpose labels are used. After an intuitive presentation of the technique developped, some logical systems are treated by the method: ultrafilter logic, filter logic, CTL, Keisler`s logic and CTL*. For each one of them proof-theoretical aspects are analysed.

[pt] Neste trabalho propomos um framework lógico para sistemas de Dedução Natural rotulados. Sua meta-linguagem é baseada numa generalização dos esquemas de regras propostos por Prawitz, e o uso de rótulos permite a definição de lógicas intencionais como lógicas modais e de descrição, bem como a definição uniforme de quantificadores como o para um número não-renumerável de indivíduos vale a propriedade P (lógica de Keisler), ou para quase todos os indivíduos vale P (lógica de ultra-filtros), sem mencionar os quantificadores padrões de lógica de primeira-ordem. Mostramos também a implementação deste framework em um assistente de prova virtual disponível livremente na web, e comparamos a definição de sistemas lógicos nele com o mesmo feito em outros assistentes — Agda, Isabelle, Lean, Metamath. Como subproduto deste experimento comparativo, também contribuímos uma prova formal em Lean do postulado de Zolt em três dimensões usando o sistema Zp proposto por Giovaninni et al. / [en] We propose a Logical Framework for labelled Natural Deduction systems. Its meta-language is based on a generalization of the rule schemas proposed by Prawitz, and the use of labels allows the definition of intentional logics, such as Modal Logic and Description Logic, as well as some quantifiers, such as Keisler s for non-denumerable-many individuals property P, or for almost all individuals P holds, or generally P holds, not to mention standard first-order logic quantifiers, all in a uniform way. We also show an implementation of this framework as a freely-available web-based proof assistant. We then compare the definition of logical systems in our implementation and in other proof assistants — Agda, Isabelle, Lean, Metamath. As a sub-product of this comparison experiment, we contribute a formal proof (in Lean) of De Zolt s postulate for three dimensions, using the Zp system proposed by Giovaninni et al.