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)

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)

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)

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)

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 given non-Hamiltonian graphs, (...) since the Hamiltonian graph problem in NPcomplete. Thus, loosely speaking, the proof of NP = coNP can be obtained by HSC-elimination from our proof of NP = PSPACE. (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)

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 for magnitudes. We also formulate and derive an abstract version of Euclid’s Common Notion 5 (“The whole is greater than the part”), and analyze its logical relation to the former proposition. These results prove to be relevant for the clarification of some key conceptual aspects of Hilbert’s proof of De Zolt’s postulate, in his classicalFoundations of Geometry(1899). Furthermore, our abstract treatment of this central proposition provides interesting insights for the development of a well-behaved theory ofcompatiblemagnitudes. (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)

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 from a proof in many-sorted intuitionist logic, (...) where the axioms define the abstract data types, using Natural Deduction as deductive system. It is proved the correctness, as well as the completeness of the method regarding the Heyting arithmetic with ω-rule . A discussion about the use of the finitary induction instead of computational ω-rule concludes the work. (shrink)

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

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.

This historical analysis indicates that it is highly unlikely that the Nobel Prize winning research of Hermann J. Muller was peer-reviewed. The published paper of Muller lacked a research methods section, cited no references, and failed to acknowledge and discuss the work of Gager and Blakeslee that claimed to have induced gene mutation via ionizing radiation six months prior to Muller’s non-data Science paper :84-87, 1927a). Despite being well acclimated into the scientific world of peer-review, Muller choose to avoid (...) the peer-review process on his most significant publication. It appears that Muller’s actions were strongly influenced by his desire to claim primacy for the discovery of gene mutation. The actions of Muller have important ethical lessons and implications today, when self-interest trumps one’s obligations to society and the scientific culture that supports the quest for new knowledge and discovery. (shrink)

Summary Hermann Helmholtz has often been understood to have started research under the influence of Kant, and then to have made a transition to a later mature empiricist phase. Without claiming that in 1847 Helmholtz held the same positions that he later espoused, I suggest that already in his 1847 ‘Über die Erhaltung der Kraft’ one may find important aspects of his later empiricism. I highlight the ways in which, from early on, Helmholtz turned Kant to use in developing (...) an empirical program of inquiry into possible basic natural causes. To that end, I indicate how, throughout his arguments, Helmholtz employed, sometimes explicitly, but often tacitly, an empiricist logic, one that ran contrary to any form of transcendental deduction, and even to all a priori knowledge. Instead of deriving aspects about the ultimate constituents of nature, Helmholtz aimed to define the proper project for physical natural science. The first part of the paper describes the context of discussion in which Helmholtz entered. The bulk of the paper then analyzes Helmholtz's arguments in order to make space between (1) Kantian, and other, deductions of characteristics that must be true of nature and (2) Helmholtz's delineation of empirically determinable characteristics of presumed ultimate elements of nature, ones that he meant to be specified and delimited through future experimental research. The paper highlights that throughout his discussion Helmholtz meant to define the proper project for physical natural science, a project rife with empiricist aspects. (shrink)

Wittgenstein explores learning through practice in the Philosophical Investigations by means of an extended analogy with games. However, does this concern with learning also necessarily extend to education, in our institutional understanding of the word? While Wittgenstein's examples of language learning and use are always shared or social, he does not discuss formal educational institutions as such. He does not wish to found a ‘school of thought’, and is suspicious of philosophy acting as a theory that can be applied to (...) other areas of life. While Wittgenstein's focus on developing independent thinking was neither individualistic nor anti-institutional, it did, however, focus on developing the thinking of his students rather than theorising about how this could be applied on a large scale. An analysis of Hermann Hesse's novel, The Glass Bead Game will help us to pick up where Wittgenstein deliberately left off—thinking about how (or if) one can institutionalise learning methods that encourage thinking for oneself. These differences in the writers’ treatment of education will become evident in the differences between their game analogies. While language-games combat our ‘craving for generality’ in Philosophical Investigations, the Glass Bead Game represents this craving, and how it manifests itself throughout history in disciplines other than logic and philosophy of language. It also represents the potential for institutions to become insular, exclusive communities. (shrink)

This paper assesses possible reasons why Hermann J. Muller avoided peer-review of data that became the basis of his Nobel Prize award for producing gene mutations in male Drosophila by X-rays. Extensive correspondence between Muller and close associates and other materials were obtained from preserved papers to compliment extensive publications by and about Muller in the open literature. These were evaluated for potential historical insights that clarify why he avoided peer-review of his Nobel Prize findings. This paper clarifies the (...) basis of Muller’s (Muller HJ, Sci 66 84-87, 1927c) belief that he produced X-ray induced “gene” mutations in Drosophila. It then shows his belief was contemporaneously challenged by his longtime friend/confidant and Drosophila geneticist, Edgar Altenburg. Altenburg insisted that Muller may have simply poked large holes in chromosomes with massive doses of X-rays, and needed to provide proof of gene “point” mutations. Given the daunting and uncertain task to experimentally address this criticism, especially within the context of trying to become first to produce gene mutations, it is proposed that Muller purposely avoided peer-review while rushing to publish his paper in Science to claim discovery primacy without showing any data. The present paper also explores ethical issues surrounding these actions, including those of the editor of Science, James McKeen Catell and Altenburg, and their subsequent impact on the scientific and regulatory communities. This historical analysis suggests that Muller deliberately avoided peer-review on his most significant findings because he was extremely troubled by the insightful and serious criticism of Altenburg, which suggested he had not produced gene mutations as he claimed. Nonetheless, Muller manipulated this situation (i.e., publishing a discussion within Science with no data, publishing a poorly written non-peer reviewed conference proceedings with no methods and materials, and no references) due to both the widespread euphoria over his claim of gene mutation and confidence that Altenburg would not publically challenge him. This situation permitted Muller to achieve his goal to be the first to produce gene mutations while buying him time to later try to experimentally address Altenburg’s criticisms, and a possible way to avoid discovery of his questionable actions. (shrink)

This paper describes an episode in the life of the prominent plant radiation geneticist, Lewis J. Stadler during which he became a target of the Federal Bureau of Investigation concerning loyalty to the United States due to possible associations with the communist party. The research is based on considerable private correspondence of Dr. Stadler, the FBI interrogatory questions and Dr. Stadler’s answers and letters of support for Dr. Stadler by leading scientists such as, Hermann J. Muller.

Ethics of Psychiatry addresses the key ethical and legal issues in mental health care. With selections by Paul S. Applebaum, Christopher Boorse, Kerry Brace, Peter R. Breggin, Paula J. Caplan, Glen O. Gabbard, Donald H.J. Hermann, Lawrie Reznek, Thomas Szasz, Jerome Wakefield, Bruce J. Winick, and Robert M. Veatch, among others, this sourcebook offers the latest research in psychiatry, psychology, advocacy, mental health law, social services, and medical ethics relevant to the rational autonomy of psychiatric patients.

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 Hermann Haeusler (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 Hermann Haeusler (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)

The paper addresses Thiodolf Rein’s (1838–1919) view of empiricist philosophies, which arrived in Finland in the second half of the nineteenth century. Rein was the key figure of Finnish philosophy towards the end of the nineteenth century. His philosophy was strongly influenced by Hermann Lotze (1817–1881), probably the most distinguished German philosopher of the time. In his main work, "Försök till en framställning af psykologin eller vetenskapen om själen" (Attempt at a presentation of psychology, or the science of the (...) soul, 1876–1891), Rein attempts to reconcile modern natural science and its empirical methodology with idealist metaphysics. His chief concern is to refute the claim that the results of natural science corroborate materialism. Whereas Lotze had only shortly commented on Charles Darwin’s theory of evolution, Rein attempts to integrate Darwin’s theory into his idealist metaphysics. Besides philosophy, Rein’s arguments had also implications for broader political and cultural issues of the time. (shrink)

This is a book grounded in the real ethical challenges of modern business practice, with a world-religious perspective so necessary in an era of globalization.

The Stanford Encyclopedia of Philosophy is an open access, dynamic reference work designed to organize professional philosophers so that they can write, edit, and maintain a reference work in philosophy that is responsive to new research. From its inception, the SEP was designed so that each entry is maintained and kept up to date by an expert or group of experts in the field. All entries and substantive updates are refereed by the members of a distinguished Editorial Board before they (...) are made public. (shrink)

Bd. 1. Die Gegenwart.--Bd. 2. T.1. Der Leib. T.2. Der Leib im Spiegel der Kunst.--Bd. 3. Der Raum. T.1. Der liebliche Raum. T.2. Der Gefühlsraum. T.3. Der Rechtsraum. Praktische Philosophie. T.4. Das Göttliche und der Raum. T.5. Die Wahrnehmung.--Bd. 4. Die Person.--Bd. 5. Die Aufhebung der Gegenwart.

National Book Award Finalist. How did humanity originate and why does a species like ours exist on this planet? Do we have a special place, even a destiny in the universe? Where are we going, and perhaps, the most difficult question of all, "Why?" In The Meaning of Human Existence, his most philosophical work to date, Pulitzer Prize–winning biologist Edward O. Wilson grapples with these and other existential questions, examining what makes human beings supremely different from all other species. (...) Searching for meaning in what Nietzsche once called "the rainbow colors" around the outer edges of knowledge and imagination, Wilson takes his readers on a journey, in the process bridging science and philosophy to create a twenty-first-century treatise on human existence—from our earliest inception to a provocative look at what the future of mankind portends. Continuing his groundbreaking examination of our "Anthropocene Epoch," which he began with The Social Conquest of Earth, described by the New York Times as "a sweeping account of the human rise to domination of the biosphere," here Wilson posits that we, as a species, now know enough about the universe and ourselves that we can begin to approach questions about our place in the cosmos and the meaning of intelligent life in a systematic, indeed, in a testable way. Once criticized for a purely mechanistic view of human life and an overreliance on genetic predetermination, Wilson presents in The Meaning of Human Existence his most expansive and advanced theories on the sovereignty of human life, recognizing that, even though the human and the spider evolved similarly, the poet's sonnet is wholly different from the spider's web. Whether attempting to explicate "The Riddle of the Human Species," "Free Will," or "Religion"; warning of "The Collapse of Biodiversity"; or even creating a plausible "Portrait of E.T.," Wilson does indeed believe that humanity holds a special position in the known universe. The human epoch that began in biological evolution and passed into pre-, then recorded, history is now more than ever before in our hands. Yet alarmed that we are about to abandon natural selection by redesigning biology and human nature as we wish them, Wilson soberly concludes that advances in science and technology bring us our greatest moral dilemma since God stayed the hand of Abraham. (shrink)

Science provides us with representations of atoms, elementary particles, polymers, populations, genetic trees, economies, rational decisions, aeroplanes, earthquakes, forest fires, irrigation systems, and the world’s climate. It's through these representations that we learn about the world. This entry explores various different accounts of scientific representation, with a particular focus on how scientific models represent their target systems. As philosophers of science are increasingly acknowledging the importance, if not the primacy, of scientific models as representational units of science, it's important to (...) stress that how they represent plays a fundamental role in how we are to answer other questions in the philosophy of science (e.g. the scientific realism debate). This entry begins by disentangling ‘the’ problem of scientific representation, before critically evaluating the current options available in the literature. (shrink)

The so-called ergodic hierarchy (EH) is a central part of ergodic theory. It is a hierarchy of properties that dynamical systems can possess. Its five levels are egrodicity, weak mixing, strong mixing, Kolomogorov, and Bernoulli. Although EH is a mathematical theory, its concepts have been widely used in the foundations of statistical physics, accounts of randomness, and discussions about the nature of chaos. We introduce EH and discuss its applications in these fields.