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. (shrink)

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. (shrink)

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. (shrink)

This paper deals with the recent Swedish proposals of a Intuitionistic notion of Truth, by Dag Prawitz and Per Martin-Löf.

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. (shrink)

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. (shrink)

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. (shrink)

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 introduction and elimination rules are instances of (...) the higher-level schemes can be defined in terms of $\{ \vee, \wedge, \rightarrow, \bot \}$.The aim of the present work is to extend the well-known connections between Proof Theory and Category Theory to higher-level Natural Deduction. To be precise, we will show how an adjointness between cartesian closed categories with finite coproducts can be associated, in a systematic way, with any operator $\phi$ defined by the higher-level schemes. The objects in the categories will be rules instead of formulas. (shrink)

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. (shrink)

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.

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. (shrink)

Veloso-Pereira-Haeusler_On-what-there-must-be.

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.

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.

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. (shrink)

RESUMO Na "Kritik der praktischen Vernunft", os conceitos do factum da razão e do sentimento de respeito pela lei moral geram grandes divergências interpretativas. O presente artigo tem como objetivo apresentar as interpretações de Zeljko Loparic, Guido Antônio de Almeida e Flávia Carvalho Chagas. ABSTRACT In "Kritik der praktischen Vernunft", the concepts of factum of reason and of feeling of respect for the moral law generate great interpretative divergences. This paper aims to present the interpretations of Zeljko Loparic, Guido Antônio (...) de Almeida and Flávia Carvalho Chagas. (shrink)

Baseando-se na premissa de que a pessoa com deficiência se torna vítima das várias violências institucionais, sobretudo as de cunho jurídico e social, quando introduzida no sistema carcerário, o objetivo deste trabalho é assentar uma reflexão acerca da introdução dos deficientes na prisão, especialmente em relação à provisão da acessibilidade, sob a perspectiva das normas do direito nacional. A partir do objetivo traçado, o estudo é demarcado pela pesquisa de cunho bibliográfico, destacando opiniões doutrinárias e dados estatísticos brasileiros em relação (...) ao número de encarcerados nessas condições. Dentre os resultados e conclusões atingidas, cumpre dizer que o Brasil ainda possui atitudes jurídico-administrativas embrionárias em relação à provisão de acessibilidade ao deficiente no ambiente carcerário, incompatível com a dignidade dessas pessoas. (shrink)

We address the impingement of Artificial Intelligence (AI) on logic, by examining the requirements posed on logic by knowledge representation and reasoning issues which A I has addressed. We then outline some of AI's contributions, via Logic Programming, to more dynamic forms of logic, in order to deal with knowledge in flux, namely: incomplete and contradictory information; hypotheses making through abduction; argumentation; diagnosis and debugging; updating; and learning. Along the way we delve into implications for the philosophy of knowledge.

We address the impingement of Artificial Intelligence (AI) on logic, by examining the requirements posed on logic by knowledge representation and reasoning issues which A I has addressed. We then outline some of AI's contributions, via Logic Programming, to more dynamic forms of logic, in order to deal with knowledge in flux, namely: incomplete and contradictory information; hypotheses making through abduction; argumentation; diagnosis and debugging; updating; and learning. Along the way we delve into implications for the philosophy of knowledge.

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.

The objective of this article is to analyze the several concepts existing between the greeks as for archç, and its relations with the construction of the neotestamentary thought. Deal with one approach that visualizes identify interferences of ideas spread in the hellenic world that slowly had affected the way to think and to understand the origin of the things in the christian thought in formation process at the first century. For this reason, when writing yours texts, the neotestamentarys authors presented (...) to their communities and to others readers what they understood be archç, that is, the origin of all the things. (shrink)

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.

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. (shrink)

Trata-se de uma pesquisa de natureza bibliográfica, com abordagem quanti-qualitativa, de caráter descritivo-exploratório que objetiva analisar a produção do conhecimento do Curso de Educação Física da Universidade do Estado do Pará em Altamira, no período de 2011-2018. Os achados apontam uma evolução do modo de produzir conhecimento, pois constatou-se uma redução dos vazios analíticos presentes nas pesquisas analisadas. Conclui que há um aumento no rigor cientifico presente nas produções devido uma maior utilização de técnicas, metodologias e teorias consistentes para a (...) verificação da realidade pesquisada e para a elaboração das respostas (R) dos problemas (P) investigados. (shrink)

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. (shrink)

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. (shrink)

Physiological responses in futsal have not been studied together with temporal information about the players’ stay on the court. The aim of this study was to compare heart rate and blood lactate concentration responses between 1-H and 2-H considering the time of permanency of the players on the court at each substitution in a futsal match. HR was recorded during entire match and [La−] was analyzed after each substitution of seven players. %HRmean and [La−] mean did not differ between 1-H (...) and 2-H. Time in intensity zones of 50–100 %HRmax differed only in 60–70 %HRmax. HR coefficient of variation throughout the match was low and among the four outfield players on the court. Substitutions, time of permanence on the court, ratio between time in- and out-ratio on the court also were similar between 1-H and 2-H. Balancing the number of substitutions, and the In:Outcourt ratio of players in both halves of the match, playing lower time at 1-H, ~8 min for each participation in the match, made it possible to maintain intensity of the match in 2-H similar to the 1H. These results are a good guidance to coaches and for application in future studies. (shrink)

Coletânea de artigos em homenagem a Guido Antonio de Almeida e Raul Ferreira Landim Filho.

Esta obra traz ao leitor ensaios publicados ao longo de algumas décadas, alinhados a tradição brasileira de 'pensamento social'. Entre os vários intelectuais e pensadores analisados por Castro Santos, a obra de Gilberto Freyre, um dos maiores nomes de nosso tempo, mereceu atenção especial. Além do escritor pernambucano, todos os demais autores tratados neste livro revelam uma preocupação com o Brasil, uma intenção de 'reinventar' um país, gerar uma nação, criar metáforas de transformação social, converter idiomas e, regionalismos a uma (...) 'língua geral' de brasilidade. Nomes ilustres e obras hoje clássicas na tradição do pensamento social no Brasil passam pelo crivo do autor, sociólogo pertencente a geração que se voltou para grandes temas e cenários, sempre a cautelosa distância da excessiva especialização profissional dos dias atuais. Apesar da diversidade de perspectivas ou pontos de vista, os autores discutidos neste livro estão sempre a 'conjugar o futuro': a exemplo dos positivistas progressistas, como Pereira Barreto, ou dos agitadores das reformas na educação e saúde, como Azevedo Sodré, Arthur Neiva e Belisário Pena - esses últimos, figuras de destaque da Primeira República; por outro lado, em que pese a diversidade ainda maior de ideais e projetos, em autores como Gilberto Freyre e Sérgio Buarque de Holanda, ou na contribuição destacada de Antonio Candido, há sempre a preocupação de reinventarmo-nos (como já se disse deles), em um sentido que se poderia chamar totalizador. Isto é, trata-se de entender o país, retratá-lo, discutir projetos e novos caminhos. Na agenda intelectual da atualidade, aquela intenção não deveria jamais ser perdida. Essa intenção em 'pensar o país' remete sempre as preocupações do autor, ao relançar, pela EdUERJ, o presente livro. (shrink)

El presente artículo busca enfocar la correlación entre el uso de la energía, el espacio, el territorio y el desarrollo local, teniendo en cuenta la utilización del gas natural en las cerámicas de Mato Grosso del Sur/Brasil. La importancia de los hechos geográficos es pautada por muchos parámetros, como el paso del tiempo, los nuevos descubrimientos tecnológicos, las necesidades de materias primas, los objetivos nacionales e internacionales y la ética de las relaciones internacionales. El gas natural no es utilizado aún (...) como fuente alternativa de energía en gran escala en el Estado. Puede ser considerado como uno de los resultados de la valorización de la política socio económica, de la cultura local y del medio ambiente preservado como parte de la identidad local del ser humano al mejorar su calidad de vida. (shrink)

A cosmological principle, because it was the first to be created, Exu presents itself as the creative protomatter, whose expansive and unfinished character makes possible the appearanceof all other creations. He is the animating principle of existence and in everything there isExu. The crossroads is its space-time and this fact would explain why “black culture is acrossroads culture”. But, incarnated in Afro-diasporic practices in the Atlantic bands, Exunot only vigorously maintains his multifaceted power, showing that colonial redemption didnot obtain the (...) expected result, but also shows that its everyday meanings in the African BlackDiaspora here in the Americas they are the result of battles, negotiations, authoritarianism,power regimes, violence, transgressions, silencing and alliances experienced in the colonialdynamic, as Luiz Rufno reminds us in his book Pedagogia das Encruzilhadas (2019). (shrink)

In §1 I explain that my rejection of possible states of affairs as a basis for an account of falsity is not part of a general rejection of modal notions but is a rejection of possible and impossible entities of any sort. I then show that my account of senses and of propositions is indeed a modal account. In §2 I examine some of Wittgenstein’s ideas about falsity, as presented by Luiz Carlos, in relation to my account of falsity (...) and negation. In §3 I discuss the modal aspects of identification for propositions. (shrink)

This book is about power and freedoms in our technological world and has two main objectives. The first is to demonstrate that a theoretical exploration of the algorithmic governmentality hypothesis combined with the capability approach is useful for a better understanding of power and freedoms in Ambient Intelligence, a world where information and communication technologies are invisible, interconnected, context aware, personalized, adaptive to humans and act autonomously. The second is to argue that these theories are useful for a better comprehension (...) of privacy and data protection concepts and the evolution of their regulation. Having these objectives in mind, the book outlines a number of theses based on two threads: first, the elimination of the social effects of uncertainty and the risks to freedoms and, second, the vindication of rights. Inspired by and building on the outcomes of different philosophical and legal approaches, this book embodies an effort to better understand the challenges posed by Ambient Intelligence technologies, opening paths for more effective realization of rights and rooting legal norms in the preservation of the potentiality of human capabilities. (shrink)