-
7On an Ecumenical Natural Deduction with Stoup. Part I: The Propositional CaseIn Antonio Piccolomini D'Aragona (ed.), Perspectives on Deduction: Contemporary Studies in the Philosophy, History and Formal Theories of Deduction, Springer Verlag. pp. 139-169. 2024.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 adap…Read more
-
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
-
60An ecumenical notion of entailmentSynthese 198 (S22): 5391-5413. 2019.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 th…Read more
-
27A Pure View of Ecumenical ModalitiesIn Alexandra Silva, Renata Wassermann & Ruy de Queiroz (eds.), Logic, Language, Information, and Computation: 27th International Workshop, Wollic 2021, Virtual Event, October 5–8, 2021, Proceedings, Springer Verlag. pp. 388-407. 2021.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} \…Read more
-
60Michael Detlefsen (ed.), Proof, Logic and Formalization. Michael Detlefsen (ed.), Proof and Knowledge in Mathematics (review)Erkenntnis 47 (2): 245-254. 1997.
-
43Validades Existenciais e Enigmas RelacionadosDois Pontos 6 (2). 2009.Logic does not have purely existential theorems: the only existential sentences that are valid are those with valid universal analogues. Here, we show indeed this is so, when properly interpreted: every existential validity has a simple universal analogue, which is also valid. We also characterize existential and universal validities in terms of tautologies
-
10Caminhos da razão. Estudos em homenagem a Guido Antônio de Almeida e Raul Ferreira Landim Filho (edited book)Nau Editora. 2010.Coletânea de artigos em homenagem a Guido Antonio de Almeida e Raul Ferreira Landim Filho.
-
Metafísica, lógica e outras coisas mais (edited book)Nau Editora. 2011.Livro em homenagem ao filósofo brasileiro Luiz Henrique Lopes, um dos maiores expoentes da filosofia analítica. Neste livro grandes nomes da filosofia brasileira discorrem sobre a filosofia analítica e vários assuntos da filosofia contemporânea.
-
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
-
5A propósito del formalismo de Johann von NeumannMetatheoria – Revista de Filosofía E Historia de la Ciencia 10 (2): 51--59. 2020.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 Mathemati…Read more
-
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.
-
20Michael Detlefsen (ed.), Proof, Logic and Formalization. Michael Detlefsen (ed.), Proof and Knowledge in Mathematics (review)Erkenntnis 47 (2): 245-254. 1997.
-
18Propositional 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
-
49Normalization, Soundness and Completeness for the Propositional Fragment of Prawitz’ Ecumenical SystemRevista Portuguesa de Filosofia 73 (3-4): 1153-1168. 2017.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…Read more
-
26Historical models and economic syllogismsJournal of Economic Methodology 25 (1): 68-82. 2018.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 econ…Read more
-
11A 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
-
The rules-as-types interpretation of schroder-heister's extension of natural deductionManuscrito 22 (2): 149. 1999.
-
5Logic, sets and information: proceedings of the tenth Brazilian Conference on Mathematical Logic (edited book)Centro de Lógica, Epistemologia e História da Ciência, UNICAMP. 1995.Proceedings of the Tenth Brazilian Conference on Mathematical Logic. Coleção CLE, volume 14, 1995. Centro De Lógica, Epistemologia e História da Ciência, Unicamp, Campinas, SP, Brazil.
-
21The semantics of falsity and negationManuscrito 27 (1): 183-191. 2004.In Logical Forms Chateaubriand offers a realist semantics for false elementary propositions and for true negative propositions that appeals to negative facts. Although he does not refer to Wittgenstein, he rules out “possibilist” solutions such as that of the Tractatus. In this paper I will critically discuss Chateaubriand’s solution and compare it with the semantics of the Tractatus
-
101A short note on intuitionistic propositional logic with multiple conclusionsManuscrito 28 (2): 317-329. 2005.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 restri…Read more
-
48A 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
-
360Considerações sobre a Noção Construtiva de VerdadeO Que Nos Faz Pensar 17 107-123. 2003.This paper deals with the recent Swedish proposals of a Intuitionistic notion of Truth, by Dag Prawitz and Per Martin-Löf.
-
249th Workshop on Logic, Language, Information and ComputationLogic Journal of the IGPL 10 (6): 679-688. 2002.
-
Alguns resultados sobre fragmentos com negação da lógica clássicaO Que Nos Faz Pensar 105-111. 2008.
-
A Categorical Approach To Higher-level Introduction And Elimination RulesReports on Mathematical Logic 3-19. 1994.A natural extension of Natural Deduction was defined by Schroder-Heister where not only formulas but also rules could be used as hypotheses and hence discharged. It was shown that this extension allows the definition of higher-level introduction and elimination schemes and that the set $\{ \vee, \wedge, \rightarrow, \bot \}$ of intuitionist sentential operators forms a {\it complete} set of operators modulo the higher level introduction and elimination schemes, i.e., that any operator whose intr…Read more