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)
This is the report on the XVI BRAZILIAN LOGIC CONFERENCE (EBL 2011) held in Petrópolis, Rio de Janeiro, Brazil between May 9–13, 2011 published in The Bulletin of Symbolic Logic Volume 18, Number 1, March 2012. -/- The 16th Brazilian Logic Conference (EBL 2011) was held in Petro ́polis, from May 9th to 13th, 2011, at the Laboratório Nacional de Computação o Científica (LNCC). It was the sixteenth in a series of conferences that started in 1977 with the aim of (...) congregating logicians from Brazil and abroad, furthering interest in logic and its applications, stimulating cooperation, and contributing to the development of this branch of science. EBL 2011 included more than one-hundred and fifty participants, all of them belonging to prominent research institutes from Brazil and abroad, especially Latin America. The conference was sponsored by the Academia Brasileira de Ciências (ABC), the As- sociation for Symbolic Logic (ASL), Universidade Estadual de Campinas (UNICAMP), Centre for Logic, Epistemology and the History of Sciences (CLE), Laboratório Nacional de Computação o Científica (LNCC), Pontif ́ıcia Universidade Cato ́lica do Rio de Janeiro (PUC- Rio), Sociedade Brasileira de Lógica (SBL), and Universidade Federal Fluminense (UFF). Funding was provided by Conselho Nacional de Desenvolvimento Cient ́ıfico e Tecnolo ́ gico (CNPq), Fundac ̧a ̃o de Amparo `a Pesquisa do Estado de São Paulo (FAPESP), Fundação Euclides da Cunha (FEC), and Universidade Federal Fluminense (UFF). The members of the Scientific Committee were: Mário Folhadela Benevides (COPPE- UFRJ), Fa ́bio Bertato (CLE-IFCH-UNICAMP), Jean-Yves Béziau (UFRJ), Ricardo Bianconi (USP), Juliana Bueno-Soler (UFABC), Xavier Caicedo (Universidad de Los An- des), Walter Carnielli (CLE-IFCH-UNICAMP), Oswaldo Chateaubriand Filho (PUC-Rio), Marcelo Esteban Coniglio (CLE-IFCH-UNICAMP), Newton da Costa (UFSC, President), Antonio Carlos da Rocha Costa (UFRG), Alexandre Costa-Leite (UnB), I ́tala M. Loffredo D’Ottaviano (CLE-IFCH-UNICAMP), Marcelo Finger (USP), Edward HermannHaeusler (PUC-Rio), Décio Krause (UFSC), João Marcos (UFRN), Ana Teresa de Castro Martins (UFC), Maria da Paz Nunes de Medeiros (UFRN), Francisco Miraglia (USP), Luiz Car- los Pereira (PUC-Rio and UFRJ), Elaine Pimentel (UFMG), and Samuel Gomes da Silva (UFBA). The members of the Organizing Committee were: Anderson de Araujo (UNICAMP), Walter Carnielli (CLE-IFCH-UNICAMP), Oswaldo Chateaubriand Filho (PUC-Rio, Co- chair), Marcelo Correa (UFF), Renata de Freitas (UFF), Edward HermannHaeusler (PUC- RJ), Hugo Nobrega (COPPE-UFRJ), Luiz Carlos Pereira (PUC-Rio e IFCS/UFRJ), Leandro Suguitani (UNICAMP), Rafael Testa (UNICAMP), Leonardo Bruno Vana (UFF), and Petrucio Viana (UFF, Co-chair). (shrink)
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)
Ludwig von Mühlenfels as Advocatus Schleiermacheri. An addendum. The editorial copy of the “Allgemeine Zeitung” has survived in the Cotta-Archive with the names of the contributors. This has made it possible to identify belatedly the author of the apologia “Another word about Schleiermacher” in the “Außerordentliche Beilage der Allgemeinen Zeitung” of April 2, 1834. It was Ludwig Friedrich von Mühlenfels. Mühlenfels, who led a rather varied life, was related to Schleiermacher’s wife Henriette, and thus belonged to Schleiermacher’s extended family. Member (...) of Lützow’s Freicorps. On Schleiermacher’s suggestion, Mühlenfels participated in the war of liberation against Napoleon as a volunteer with the “Black Hunters”, in the end in the so-called Battle of the Nations at Leipzig. He finished the study of law in 1816 and, on probation, joined the prosecutor’s office in Cologne where the French legal code was still in force. Incarcerated as a demagogue under the investigating judge E. T. A. Hoffmann. Mühlenfels became one of the formative figures in the early history of German fraternities and participated in the Wartburg Festival in October 1817. He was arrested in July 1819 by the authorities in Berlin, charged with activities as a demagogue and incarcerated in Berlin on September 17. Mühlenfels contested the jurisdiction of the authorities in Berlin and refused to testify. The investigative judge was the writer and composer E. T. A. Hoffmann who wanted to have Mühlenfels released, and who later used him as a literary figure in a satirical novel. Flight from Berlin – Exile in Sweden. On May 5, 1821, Mühlenfels succeeded in fleeing to Sweden where he made a meagerly living as a private tutor. Professor for German and Scandinavian Literature in London – Return to Prussia. In October 1827, Mühlenfels reached London. Supported by some German scholars, he obtained the Chair for German and Scandinavian at the newly founded University College. He taught there until 1831 and publishedseveral textbooks. When he was acquitted by a court ruling in 1830, he returned to the Prussian public service in August 1831 and gradually built a solid career. The defender of Schleiermacher. His apologia of Schleiermacher written in opposition to the obituary by Gutzkow is a masterpiece of literary and legal writing. – First publication: Six letters between Mühlenfels, Henriette and Friedrich Schleiermacher, and Georg Andreas Reimer. (shrink)
Resumo: Franz Brentano não foi uma figura solitária que propôs sua filosofia isolada de outros filósofos contemporâneos na Alemanha, tal como alguns neo-brentanianos reivindicaram nos últimos anos. O objetivo deste artigo é corrigir tais concepções equivocadas estabelecendo que Brentano desenvolveu sua psicologia filosófica engajado ativamente no rico contexto histórico-intelectual e acadêmico de seu tempo - em particular, sob a influência de Hermann Lotze. Especificamente, Brentano: (i) adota de Lotze a ideia de que juízo não é apenas uma associação de (...) ideias, mas uma asserção do conteúdo; (ii) também adota a ideia de Lotze de que o conteúdo da percepção é algo dado; (iii) a noção brentaniana de intencionalidade também foi herdada de Lotze, (iv) bem como o método da psicologia descritiva; (v) finalmente, Lozte e Brentano concordaram ao admitir que percepção e conhecimento estão intrinsicamente conectados às emoções. Ao mesmo tempo, há ao menos dois pontos nos quais Brentano discorda de Lotze: (i) ele critica a teoria da percepção do signo local, bem como o atomismo de Lotze. Estas eram claramente teorias construtivistas inspiradas por Kant. (ii) Brentano também critica o princípio do teleomecanismo de Lotze, influenciado pelos idealistas alemães. (shrink)
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 corresponds to a noncommutative bi-endofunctor into a category, which encloses all categories of (...) such hierarchical structure. A soundness theorem for LSC is shown with respect to this semantical framework. (shrink)
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 theoretic approach. Recall that in [3] we considered any valid ρ in question that had a “short” tree-like proof π in the Hudelmaier-style cutfree sequent calculus for minimal logic. The “shortness” means that the height of π and the total weight of different formulas occurring in it are both polynomial in the weight of ρ. However, the size, and hence also the weight, of π could be exponential in that of ρ. To overcome this trouble we embedded π into Prawitz’s proof system of natural deductions containing single formulas, instead of sequents. As in π, the height and the total weight of different formulas of the resulting tree-like natural deduction ∂1 were polynomial, although the size of ∂1 still could be exponential, in the weight of ρ. In our next, crucial move, ∂1 was deterministically compressed into a “small”, although multipremise, dag-like deduction ∂ whose horizontal levels contained only mutually different formulas, which made the whole weight polynomial in that of ρ. However, ∂ required a more complicated verification of the underlying provability of ρ. In this paper we present a nondeterministic compression of ∂ into a desired standard dag-like deduction ∂0 that deterministically proves ρ in time and space polynomial in the weight of ρ.2 Together with [3] this completes the proof of NP = PSPACE.Natural deductions are essential for our proof. Tree-to-dag horizontal compression of π merging equal sequents, instead of formulas, is not sufficient, since the total number of different sequents in π might be exponential in the weight of ρ – even assuming that all formulas occurring in sequents are subformulas of ρ. On the other hand, we need Hudelmaier’s cutfree sequent calculus in order to control both the height and total weight of different formulas of the initial tree-like proof π, since standard Prawitz’s normalization although providing natural deductions with the subformula property does not preserve polynomial heights. It is not clear yet if we can omit references to π even in the proof of the weaker result NP = coNP. (shrink)
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 total number of distinct formulas, ϕ(∂), of a given tree-like deduction ∂ of a minimal (...) tautology ρ are both polynomial in the length of ρ, |ρ|, then the size of the horizontal dag-like compression ∂ᶜ is at most h(∂)×ϕ(∂), and hence polynomial in |ρ|. That minimal tautologies ρ are provable by tree-like natural deductions ∂ with |ρ|-polynomial h(∂) and ϕ(∂) follows via embedding from Hudelmaier’s result that there are analogous sequent calculus deductions of sequent ⇒ρ. The notion of dag-like provability involved is more sophisticated than Prawitz’s tree-like one and its complexity is not clear yet. Our approach nevertheless provides a convergent sequence of NP lower approximations of PSPACE-complete validity of minimal logic. (shrink)
Hermann Cohen afirma, em uma conferência, que a aversão à religião se deve à desconfiança da filosofia, uma vez que esta oferece à religião seu fundamento crítico e autoconsciência. Ele formula três postulados religiosos. O primeiro é a ideia da unicidade de Deus, como fundamento da moralidade do homem. O segundo postulado é o messianismo, como fundamento da ideia de humanidade universal. O terceiro postulado é a promoção do estudo da Wissenschaft des Judentums. Este texto enfoca três temas: a (...) relação entre a tradição monoteísta judaica e a tradição filosófica grega; a questão do humanismo; a diferença entre monoteísmo e religiões. (shrink)
“The Messiah [...] is the source of all religious art.” This statement, which we find in Cohen’s Über den ästhetischen Wert unserer religiösen Bildung, seems to be not fully consistent with the whole of Cohen’s aesthetics and with Cohen’s thought about the possibility of art having religious themes. In order to explain this statement and Cohen’s perspective about Messianism in art, in §§ 1-3 I examine Cohen’s reflections about this topic in his main works about art and religion; in § (...) 4 I maintain that the goal of this statement is to underline a difference between Jewish and Christian religious art. Finally, in § 5, I offer a short examination of some 20th or 21th century artworks that can be compared to Cohen’s views about Messianism in art: namely, Marc Chagall’s crucifixions, Gustav Mahler’s 4th symphony, and Michelangelo Pistoletto’s Terzo Paradiso. (shrink)
Economic growth and development remain embedded in the very core of our current international economic system and the so called “material economy”. However, depleting natural resources and environmental degradation, which now threaten the well-being of future generations, has challenged this premise, and placed sustainable development as a necessary objective of business activity and expansion. Environmental impact assessments (EIAs) have emerged as a key tool for governments, businesses, and NGOs to manage the negative impact of their activities on the environment. Businesses (...) in particular play a key role in averting or mitigating current environmental trends given that the economic growth they have stimulated has serious consequences for both the environment and social well-being. However, research on the use of EIAs has been conducted mostly from a governmental perspective producing a clear gap between research development and business (corporate) practice. To bridge this gap in knowledge, we develop a new EIA process tailored to real world business constraints and provide a range of propositions which we hope will stimulate future research efforts toward understanding and guiding how businesses integrate environmental issues into their decision-making processes. (shrink)
O artigo discute como a lacuna deixada pela crítica a uma ética racionalizada, que sustentou o projeto pedagógico moderno, pode encontrar nova justificação. Isso implica na necessidade. De desencadear um processo refletido sobre as formas de relação entre ética e estética, de modo a explicitar os problemas e perspectivas que se apresentam à ética na educação, diante da emergência dos processos de estetização do mundo da vida.
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.
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. (shrink)
