-
7Disjunctive Syllogism without Ex falsoIn Thomas Piecha & Kai F. Wehmeier (eds.), Peter Schroeder-Heister on Proof-Theoretic Semantics, Springer. pp. 193-209. 2024.The relation between ex falso and disjunctive syllogism, or even the justification of ex falso based on disjunctive syllogism, is an old topic in the history of logic. This old topic reappears in contemporary logic since the introduction of minimal logic by Johansson. The disjunctive syllogism seems to be part of our general non-problematic inferential practices and superficially it does not seem to be related to or to depend on our acceptance of the frequently disputable ex falso rule. We know …Read more
-
19Propositional proof compressions and DNF logicLogic Journal of the IGPL 19 (1): 62-86. 2011.This paper is a continuation of dag-like proof compression research initiated in [9]. We investigate proof compression phenomenon in a particular, most transparent case of propositional DNF Logic. We define and analyze a very efficient semi-analytic sequent calculus SEQ*0 for propositional DNF. The efficiency is achieved by adding two special rules CQ and CS; the latter rule is a variant of the weakened substitution rule WS from [9], while the former one being specially designed for DNF sequents…Read more
-
34Validades Existenciais e Enigmas RelacionadosDois Pontos 6 (2). 2009.A lógica não contém teoremas puramente existenciais: as únicas sentenças existenciaisválidas são aquelas com análogas universais válidas. Aqui, mostramos que istorealmente é assim quando corretamente interpretado: toda validade ex- istencial possuiuma análoga universal simples, que também é válida. Também caracterizamos validadesuniversais e existenciais em termos de tautologias.
-
8Proof Compression and NP Versus PSPACE II: AddendumBulletin of the Section of Logic 51 (2): 197-205. 2022.In our previous work we proved the conjecture NP = PSPACE by advanced proof theoretic methods that combined Hudelmaier’s cut-free sequent calculus for minimal logic with the horizontal compressing in the corresponding minimal Prawitz-style natural deduction. In this Addendum we show how to prove a weaker result NP = coNP without referring to HSC. The underlying idea is to omit full minimal logic and compress only “naive” normal tree-like ND refutations of the existence of Hamiltonian cycles in g…Read more
-
50De Zolt’s Postulate: An Abstract ApproachReview of Symbolic Logic 15 (1): 197-224. 2022.A theory of magnitudes involves criteria for their equivalence, comparison and addition. In this article we examine these aspects from an abstract viewpoint, by focusing on the so-called De Zolt’s postulate in the theory of equivalence of plane polygons (“If a polygon is divided into polygonal parts in any given way, then the union of all but one of these parts is not equivalent to the given polygon”). We formulate an abstract version of this postulate and derive it from some selected principles…Read more
-
18Advances in Natural Deduction: A Celebration of Dag Prawitz's Work (edited book)Springer. 2012.This collection of papers, celebrating the contributions of Swedish logician Dag Prawitz to Proof Theory, has been assembled from those presented at the Natural Deduction conference organized in Rio de Janeiro to honour his seminal research. Dag Prawitz’s work forms the basis of intuitionistic type theory and his inversion principle constitutes the foundation of most modern accounts of proof-theoretic semantics in Logic, Linguistics and Theoretical Computer Science. The range of contributions in…Read more
-
27Proof Compression and NP Versus PSPACE IIBulletin of the Section of Logic 49 (3): 213-230. 2020.We upgrade [3] to a complete proof of the conjecture NP = PSPACE that is known as one of the fundamental open problems in the mathematical theory of computational complexity; this proof is based on [2]. Since minimal propositional logic is known to be PSPACE complete, while PSPACE to include NP, it suffices to show that every valid purely implicational formula ρ has a proof whose weight and time complexity of the provability involved are both polynomial in the weight of ρ. As is [3], we use proof …Read more
-
56Proof Compression and NP Versus PSPACEStudia Logica 107 (1): 53-83. 2019.We show that arbitrary tautologies of Johansson’s minimal propositional logic are provable by “small” polynomial-size dag-like natural deductions in Prawitz’s system for minimal propositional logic. These “small” deductions arise from standard “large” tree-like inputs by horizontal dag-like compression that is obtained by merging distinct nodes labeled with identical formulas occurring in horizontal sections of deductions involved. The underlying geometric idea: if the height, h(∂), and the tota…Read more
-
8A Concrete Categorical Model For The Lambek Syntactic CalculuMathematical Logic Quarterly 43 (1): 49-59. 1997.We present a categorical/denotational semantics for the Lambek Syntactic Calculus, indeed for a λlD-typed version Curry-Howard isomorphic to it. The main novelty of our approach is an abstract noncommutative construction with right and left adjoints, called sequential product. It is defined through a hierarchical structure of categories reflecting the implicit permission to sequence expressions and the inductive construction of compound expressions. We claim that Lambek's noncommutative product …Read more
-
249th Workshop on Logic, Language, Information and ComputationLogic Journal of the IGPL 10 (6): 679-688. 2002.
-
43A New Normalization Strategy for the Implicational Fragment of Classical Propositional LogicStudia Logica 96 (1): 95-108. 2010.The introduction and elimination rules for material implication in natural deduction are not complete with respect to the implicational fragment of classical logic. A natural way to complete the system is through the addition of a new natural deduction rule corresponding to Peirce's formula → A) → A). E. Zimmermann [6] has shown how to extend Prawitz' normalization strategy to Peirce's rule: applications of Peirce's rule can be restricted to atomic conclusions. The aim of the present paper is to…Read more
-
On the relationship between well-orderings in intuitionistic type theory and data types inductively definedO Que Nos Faz Pensar 61-79. 1991.
-
25A Concrete Categorical Model for the Lambek Syntactic CalculusMathematical Logic Quarterly 43 (1): 49-59. 1997.We present a categorical/denotational semantics for the Lambek Syntactic Calculus , indeed for a λlD-typed version Curry-Howard isomorphic to it. The main novelty of our approach is an abstract noncommutative construction with right and left adjoints, called sequential product. It is defined through a hierarchical structure of categories reflecting the implicit permission to sequence expressions and the inductive construction of compound expressions. We claim that Lambek's noncommutative product…Read more
-
32Completeness of an Action Logic for Timed Transition SystemsBulletin of the Section of Logic 29 (4): 151-160. 2000.
-
25Some Models of Heterogeneous and Distributed Specifications based on Universal ConstructionsIn Jean-Yves Béziau & Alexandre Costa-Leite (eds.), Perspectives on Universal Logic, Polimetrica. 2007.
-
19Exploring Computational Contents of Intuitionist ProofsLogic Journal of the IGPL 13 (1): 69-93. 2005.One of the main problems in computer science is to ensure 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 …Read more
-
11Fibred and Indexed Categories for Abstract Model TheoryLogic Journal of the IGPL 15 (5-6): 707-739. 2007.Indexed and Fibred category theory have a long tradition in computer science as a language to formalize different presentations of the notion of a logic, as for instance, in the theory of institutions and general logics, and as unifying models of logic and type theory as well. Here we introduce the notions of indexed and fibred frames and construct a rich mathematical workspace where many relevant and useful concepts of logics can be elegantly modelled. To demonstrate the applicability of these …Read more
-
19Finitely many-valued logics and natural deductionLogic Journal of the IGPL 22 (2): 333-354. 2014.
-
5Using the Internal Logic of a Topos to Model Search Spaces for ProblemsLogic Journal of the IGPL 15 (5-6): 457-474. 2007.We present a structural model for heuristic search strategies for solving computational problems. The model is defined through the use of topos-theoretical tools and techniques, which provide an appropriate internal logic where objects of interest can be represented
-
24NUL-natural deduction for ultrafilter logicBulletin of the Section of Logic 32 (4): 191-199. 2003.
-
The rules-as-types interpretation of schroder-heister's extension of natural deductionManuscrito 22 (2): 149. 1999.
-
4Síntese Construtiva de Programas Utilizando Lógica Institucionista e Dedução NaturalPrincípios 8 (10): 25-61. 2001.Indisponível
-
50A formalization of Sambins's normalization for GLMathematical Logic Quarterly 39 (1): 133-142. 1993.Sambin [6] proved the normalization theorem for GL, the modal logic of provability, in a sequent calculus version called by him GLS. His proof does not take into account the concept of reduction, commonly used in normalization proofs. Bellini [1], on the other hand, gave a normalization proof for GL using reductions. Indeed, Sambin's proof is a decision procedure which builds cut-free proofs. In this work we formalize this procedure as a recursive function and prove its recursiveness in an arith…Read more
-
106On What There Must Be: Existence in Logic and Some Related RiddlesDisputatio 4 (34): 889-910. 2012.Veloso-Pereira-Haeusler_On-what-there-must-be.
-
1Why is this a Proof? Festschrift for Luiz Carlos Pereira (edited book)College Publications. 2015.
Areas of Interest
Philosophy of Law |
Logic and Philosophy of Logic |