Luiz Carlos Pereira

A common misconception among logicians is to think that intuitionism is necessarily tied-up with single conclusion calculi. Single conclusion calculi can be used to model intuitionism and they are convenient, but by no means are they necessary. This has been shown by such influential textbook authors as Kleene, Takeuti and Dummett, to cite only three. If single conclusions are not necessary, how do we guarantee that only intuitionistic derivations are allowed? Traditionally one insists on restrictions on particular rules: implication right, negation right and universal quantification right are required to be single conclusion rules. In this note we show that instead of a cardinality restriction such as one-conclusion-only, we can use a notion of dependency between formulae to enforce the constructive character of derivations. The system we obtain, called FIL for full intuitionistic logic, satisfies basic properties such as soundness, completeness and cut elimination. We present two motivating applications of FIL and discuss some future work.

Much has been said about intuitionistic and classical logical systems since Gentzen’s seminal work. Recently, Prawitz and others have been discussing how to put together Gentzen’s systems for classical and intuitionistic logic in a single unified system. We call Prawitz’ proposal the Ecumenical System, following the terminology introduced by Pereira and Rodriguez. In this work we present an Ecumenical sequent calculus, as opposed to the original natural deduction version, and state some proof theoretical properties of the system. We reason that sequent calculi are more amenable to extensive investigation using the tools of proof theory, such as cut-elimination and rule invertibility, hence allowing a full analysis of the notion of Ecumenical entailment. We then present some extensions of the Ecumenical sequent system and show that interesting systems arise when restricting such calculi to specific fragments. This approach of a unified system enabling both classical and intuitionistic features sheds some light not only on the logics themselves, but also on their semantical interpretations as well as on the proof theoretical properties that can arise from combining logical systems.

In 2015 Dag Prawitz proposed an Ecumenical system where classical and intuitionistic logic could coexist in peace. The classical logician and the intuitionistic logician would share the universal quantifier, conjunction, negation and the constant for the absurd, but they would each have their own existential quantifier, disjunction and implication, with different meanings. Prawitz’ main idea is that these different meanings are given by a semantical framework that can be accepted by both parties. The aim of the present paper is [1] to prove the normalization theorem for the propositional fragment NEp of Prawitz’ ecumenical system, and [2] to show that NEp is sound and complete with respect to a Kripke-style semantics for the language of NEp.

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 extend Seldin's normalization strategy to Peirce's rule by showing that every derivation Π in the implicational fragment can be transformed into a derivation Π' such that no application of Peirce's rule in Π' occurs above applications of →-introduction and →-elimination. As a corollary of Seldin's normalization strategy we obtain a form of Glivenko's theorem for the classical {→}-fragment.

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 arithmetically formalizable way, concluding that the normalization of GL can be formalized in PA. MSC: 03F05, 03B35, 03B45

Recent works about ecumenical systems, where connectives from classical and intuitionistic logics can co-exist in peace, warmed the discussion on proof systems for combining logics. This discussion has been extended to alethic modalities using Simpson’s meta-logical characterization: necessity is independent of the viewer, while possibility can be either intuitionistic or classical. In this work, we propose a pure, label free calculus for ecumenical modalities, nEK\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {nEK}$$\end{document}, where exactly one logical operator figures in introduction rules and every basic object of the calculus can be read as a formula in the language of the ecumenical modal logic EK\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {EK}$$\end{document}. We prove that nEK\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {nEK}$$\end{document} is sound and complete w.r.t. the ecumenical birelational semantics and discuss fragments and extensions.

This paper proposes a classification of economic models into three types: historical, axiomatic and conditional. Historical or empirical models utilize the historical-deductive method, and are generalizations from the economic regularities and tendencies that we find in the real world. Axiomatic models utilize the hypothetical-deductive method; they are syllogisms whose major premise is an axiom – a self-evident truth; they are appropriate for methodological sciences such as mathematics and econometrics. Conditional economic models are likewise syllogisms, but they are suitable for economics because they make for clearer and more precise economic reasoning. The criterion of truth of the substantive sciences is the conformity with reality, of the methodological science, its internal consistency. When a school of economic thought adopts mainly axiomatic models, as is the case with neoclassical economics, it implicitly falls into contradiction because their best representatives believe in the conformity with reality criterion.

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 includes material on the extension of natural deduction with higher-order rules, as opposed to higher-order connectives, and a paper discussing the application of natural deduction rules to dealing with equality in predicate calculus. The volume continues with a key chapter summarizing work on the extension of the Curry-Howard isomorphism, via methods of category theory that have been successfully applied to linear logic, as well as many other contributions from highly regarded authorities. With an illustrious group of contributors addressing a wealth of topics and applications, this volume is a valuable addition to the libraries of academics in the multiple disciplines whose development has been given added scope by the methodologies supplied by natural deduction. The volume is representative of the rich and varied directions that Prawitz work has inspired in the area of natural deduction.

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. We show that dag-like SEQ*0 has good deterministic proof search strategy. Furthermore, we expose six examples showing that dag-like deducibility in SEQ*0 admits exponential-size proof compression, as compared to familiar proof systems like cutfree sequent calculi, resolution and cutting plane proof systems

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 arithmetically formalizable way, concluding that the normalization of GL can be formalized in PA. MSC: 03F05, 03B35, 03B45.

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 that the acceptance of the ex falso is a sufficient condition for the acceptance of the disjunctive syllogism, but the interesting question is: is the ex falso a necessary condition for the acceptance of the disjunctive syllogism? The aim of the present paper is to discuss some possible ways to define systems that combines the preservation of the disjunctive syllogism with the rejection of the ex falso.

In 1930, Johann von Neumann, together with Rudolf Carnap and Arend Heyting, participated in a conference held in Königsberg, called “Second Seminar on the Epistemology of Exact Sciences”. The idea behind the reunion of these three researchers was to compose a fairly faithful picture of the three main foundational programs of mathematics at the time: formalism, logicism, and intuitionism. The main objective of this paper is to propose an analysis of the text “The Formalist Foundation of Mathematics” presented by von Neumann in this conference. We show how, from von Neumann's perspective, the problem of the consistency of mathematical theories results from the transformation of a genuinely philosophical question into a genuinely logical-mathematical question and how a proof of consistency could be seen as the solution to the foundational problem. In the final part of the text, we present some considerations about Gerhard Gentzen’s consistency proofs and their importance to contemporary proof theory.

In 2015 Dag Prawitz proposed a natural deduction ecumenical system, where classical logic and intuitionistic logic are codified in the same system. In his ecumenical system, Prawitz recovers the harmony of rules, but the rules for the classical operators do not satisfy separability. In fact, the classical rules are not pure, in the sense that negation is used in the definition of the introduction and elimination rules for the classical operators. In this work we propose an ecumenical system adapting, to the natural deduction framework, Girard’s mechanism of stoup. This allows for the definition of a pure harmonic natural deduction system for the propositional fragment of Prawitz’s ecumenical logic. We conclude by presenting an extension proposal to the first-order setting and a different approach to purity based on some ideas proposed by Julien Murzi.