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)

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)

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)

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.

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

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)

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.

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)

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)

The Nature of God explores a perennial problem in the philosophy of religion.

First published in 1903, this volume revolutionized philosophy and forever altered the direction of ethical studies. A philosopher’s philosopher, G. E. Moore was the idol of the Bloomsbury group, and Lytton Strachey declared that Principia Ethica marked the rebirth of the Age of Reason. This work clarifies some of moral philosophy’s most common confusions and redefines the science’s terminology. Six chapters explore: the subject matter of ethics, naturalistic ethics, hedonism, metaphysical ethics, ethics in relation to conduct, and the ideal. Moore's (...) simplicity of style and precise use of everyday language exercised an enormous influence on the development of analytic philosophy, and they contribute to the continuing resonance of his compelling arguments. (shrink)

Originally published in 1962. This book discusses and interprets the main themes of Buddhist thought in India and is divided into three parts: Archaic Buddhism: Tacit assumptions, the problem of "original Buddhism", the three marks and the perverted views, the five cardinal virtues, the cultivation of the social emotions, Dharma and dharmas, Skandhas, sense-fields and elements. The Sthaviras: the eighteen schools, doctrinal disputes, the unconditioned and the process of salvation, some Abhidharma problems. The Mahayana: doctrines common to all Mahayanists, the (...) Madhyamikas, the Yogacarins, Buddhist logic, the Tantras. (shrink)

Eighteenth-century theologian_Jonathan Edwards remains a significant influence on modern religion, and this book constitutes his most important contribution to Christian thought. Edwards_raises timeless questions about desire, choice, good, and evil, contrasting the opposing Calvinist and Arminian views of free will and addressing issues related to God's foreknowledge, determinism, and moral agency.

Any account of “what is special about the human brain” (Passingham 2008) must specify the neural basis of our unique ability to produce speech and delineate how these remarkable motor capabilities could have emerged in our hominin ancestors. Clinical data suggest that the basal ganglia provide a platform for the integration of primate-general mechanisms of acoustic communication with the faculty of articulate speech in humans. Furthermore, neurobiological and paleoanthropological data point at a two-stage model of the phylogenetic evolution of this (...) crucial prerequisite of spoken language: (i) monosynaptic refinement of the projections of motor cortex to the brainstem nuclei that steer laryngeal muscles, presumably, as part of a “phylogenetic trend” associated with increasing brain size during hominin evolution; (ii) subsequent vocal-laryngeal elaboration of cortico-basal ganglia circuitries, driven by human-specificFOXP2mutations.;>This concept implies vocal continuity of spoken language evolution at the motor level, elucidating the deep entrenchment of articulate speech into a “nonverbal matrix” (Ingold 1994), which is not accounted for by gestural-origin theories. Moreover, it provides a solution to the question for the adaptive value of the “first word” (Bickerton 2009) since even the earliest and most simple verbal utterances must have increased the versatility of vocal displays afforded by the preceding elaboration of monosynaptic corticobulbar tracts, giving rise to enhanced social cooperation and prestige. At the ontogenetic level, the proposed model assumes age-dependent interactions between the basal ganglia and their cortical targets, similar to vocal learning in some songbirds. In this view, the emergence of articulate speech builds on the “renaissance” of an ancient organizational principle and, hence, may represent an example of “evolutionary tinkering” (Jacob 1977). (shrink)

Clinical research under the usual regulatory constraints may be difficult or even impossible in a public health emergency. Regulators must seek to strike a good balance in granting as wide therapeutic access to new drugs as possible at the same time as gathering sound evidence of safety and effectiveness. To inform current policy, I reexamine the philosophical rationale for restricting new medicines to clinical trials, at any stage and for any population of patients (which resides in the precautionary principle), to (...) show that its objective to protect public health, now or in the future, could soon be defeated in a pandemic. Providing wider therapeutic access and coordinating observations and natural experiments, including service delivery by cluster (wedged cluster trials), may provide such a balance. However, there are important questions of fairness to resolve before any such research can proceed. (shrink)

What sense could it make to describe your life as ‘unlivable’? What is it not only to be alive but to have a life that you live or lead? I answer by developing a social understanding of the pursuit of meaning in life. True to other uses of ‘meaning,’ I propose, meaning in a life is communicative. If you experience your life as ‘unlivable,’ recovery can lie in this communicative dynamic: you regain the experience of leading your life by letting (...) others remind you of meanings you have communicated to them in leading it. My argument develops an analogy between two dimensions in which you project an investment – a care, concern, love, or the like – when you form an intention or plan. Intrapersonally, you project your investment as communicatively intelligible to your own future self at ‘plan’s end.’ Interpersonally, you project it as communicatively intelligible to others who might come to love this thing that you love simply because you love it, as an expression of love for you. The normativity of meaning in your life puts rational pressure on you not only to abandon investments that you cannot communicate but to experience the meaning in investments that you retain. (shrink)

What is the connection between philosophy as studied in universities and those general views of man and reality which are commonly considered "philosophy"? Through his attempt to rediscover this connection, Craig offers a view of philosophy and its history since the early 17th century. Craig discusses the two contrary visions of man's essential nature that dominated this period--one portraying man as made in the image of God and required to resemble him as closely as possible, the other depicting man as (...) the autonomous creator of his own environment and values--and uses this context to clarify previously opaque textual detail. Illustrating how general concepts embodied by philosophical thought can be embodied in other media--especially literary--the author brings together disparate disciplines; he also reveals striking similarities between Anglo-American and certain 20th-century continental European lines of thought. (shrink)

This book presents a systematic account of the role of the personal spiritual ideal of wu-wei--literally "no doing," but better rendered as "effortless action"--in early Chinese thought. Edward Slingerland's analysis shows that wu-wei represents the most general of a set of conceptual metaphors having to do with a state of effortless ease and unself-consciousness. This concept of effortlessness, he contends, serves as a common ideal for both Daoist and Confucian thinkers. He also argues that this concept contains within itself (...) a conceptual tension that motivates the development of early Chinese thought: the so-called "paradox of wu-wei," or the question of how one can consciously "try not to try." Methodologically, this book represents a preliminary attempt to apply the contemporary theory of conceptual metaphor to the study of early Chinese thought. Although the focus is upon early China, both the subject matter and methodology have wider implications. The subject of wu-wei is relevant to anyone interested in later East Asian religious thought or in the so-called "virtue-ethics" tradition in the West. Moreover, the technique of conceptual metaphor analysis--along with the principle of "embodied realism" upon which it is based--provides an exciting new theoretical framework and methodological tool for the study of comparative thought, comparative religion, intellectual history, and even the humanities in general. Part of the purpose of this work is thus to help introduce scholars in the humanities and social sciences to this methodology, and provide an example of how it may be applied to a particular sub-field. (shrink)

Preface and Postscript Combining a Preface with a Postscript seems a particularly apposite way to introduce (and conclude) a collection of essays on ...