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)

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)

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

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.

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)

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)

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 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)

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)

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)

One of the core problems with engineering ethics education is perceptual. Although ethics is meant to be a central component of today’s engineering curriculum, it is often perceived as a marginal requirement that must be fulfilled. In addition, there is a mismatch between faculty and student perceptions of ethics. While faculty aim to communicate the nuances and complexity of engineering ethics, students perceive ethics as laws, rules, and codes that must be memorized. This paper provides some historical context to better (...) understand these perceptual differences, and suggests that curriculum constraints are important contributing factors. Drawing on the growing scholarship of student engagement approaches to pedagogy, the paper explores how students can be empowered to effect change in the broader engineering curriculum through engineering ethics. The paper describes a student engagement approach to pedagogy that includes students as active participants in curriculum design—a role that enables them to critically reflect about why ethics is a requirement. Including students in the process of curriculum design leads students to reframe ethics as an integrative tool with the capacity to bring together different engineering departments and build bridges to non-engineering fields. This paper argues that students can and should play an active and important role in relocating ethics from the periphery to the core of the engineering curriculum. (shrink)

We have identified a sample of 53 societies outside of the classical Himalayan and Marquesean area that permit polyandrous unions. Our goal is to broadly describe the demographic, social, marital, and economic characteristics of these societies and to evaluate some hypotheses of the causes of polyandry. We demonstrate that although polyandry is rare it is not as rare as commonly believed, is found worldwide, and is most common in egalitarian societies. We also argue that polyandry likely existed during early human (...) history and should be examined from an evolutionary perspective. Our analysis reveals that it may be a predictable response to a high operational sex ratio favoring males and may also be a response to high rates of male mortality and, possibly, male absenteeism. Other factors may contribute, but our within-polyandry sample limits analysis. (shrink)

Big Ideas for Little Kids includes everything a teacher, a parent, or a college student needs to teach philosophy to elementary school children from picture books. Written in a clear and accessible style, the book explains why it is important to allow young children access to philosophy during primary-school education. Wartenberg also gives advice on how to construct a "learner-centered" classroom, in which children discuss philosophical issues with one another as they respond to open-ended questions by saying whether they agree (...) or disagree with what others have said. (shrink)

The aim of this study is to explore how nurses perceive patient participations of patients over 75 years old undergoing hemodialysis treatment in dialysis units, and of their next of kin. Ten nurses told stories about what happened in the dialysis units. These stories were analyzed with critical discourse analysis. Three discursive practices are found: (1) the nurses’ power and control; (2) sharing power with the patient; and (3) transferring power to the next of kin. The first and the predominant (...) discursive practice can be explained with an ideology of paternalism, in which the nurses used biomedical explanations and the ethical principle of benefice to justify their actions. The second can be explained with an ideology of participation, in which the nurses used ethical narratives as a way to let the patients participate in the treatment. The third seemed to involve autonomous decision-making and the ethical principle of autonomy for the next of kin in the difficult end-of-life decisions. (shrink)

В статье философия характеризуется на основе дискурсной парадигмы анализа: как текст, интеллектуальная деятельность и коммуникация. Характеризуются два равнозначных аспекта философского дискурса - когнитивный и коммуникативный. Обсуждается феномен философских контроверз, специфика философского спора, выразительные (знаковые) средства философского дискурса, роль мировоззренческого дискурса в современной общественно-политической ситуации в стране.

Background: Despite an increase in health research conducted in Africa, there are still inadequate human resources with research ethics training and lack of local long-term training opportunities in research ethics. A research ethics training program named United States-Mali Research Ethics Training Program (US-Mali RETP) was established through a partnership between the George Washington University Milken Institute School of Public Health (GWSPH), USA and University of Sciences, Techniques & Technologies of Bamako (USTTB), to address the critical need for improved bioethics training, (...) leadership, and policy in Mali. Methods: The aims of the capacity building programme are achieved by leveraging US and Africa-based expertise to strengthen research ethics education and capacity through: (1) intensive faculty development to design ethics training curricula; (2) development of a research ethics specialization within the existing Masters of Public Health program (MPH); and (3) establishing professional development courses through short-term training workshops and webinars to address research and professional needs in ethics. Results: The program will strengthen USTTB’s capacity of research ethics by training at least 15 MPH students over 5 years to prepare the next generation of ethics researchers. During the first two years of the program, a new ethics training curricula was developed, two cohorts of Master’s students were enrolled, and a series of webinars and workshops were conducted with participation of Malian and international researchers. Conclusions: US-Mali RETP will promote a sustainable bioethics enterprise at USTTB, and enable dissemination of research ethics training to increase health research capacity in Mali. (shrink)

Many writers in various fields--philosophy, religion, literature, and psychology--believe that the question of the meaning of life is one of the most significant problems that an individual faces. In The Meaning of Life, Second Edition, E.D. Klemke collects some of the best writings on this topic, primarily works by philosophers but also selections from literary figures and religious thinkers. The twenty-seven cogent, readable essays are organized around three different perspectives on the meaning of life. In Part I, the readings assert (...) and defend the theistic view that without the existence of God--or faith in God--life has no significance or purpose. In Part II the selections deny this thesis, defending instead the humanistic alternative--that life has or can have meaning and worth without any theistic beliefs or commitment. In the final group of readings, contributors ask if the question of the meaning of life is in itself legitimate and significant. The volume also includes an introduction by the editor and a selected bibliography. This new edition adds essays by A. J. Ayer, Hazel Barnes, William Lane Craig, Owen Flanagan, Antony Flew, Thomas Nagel, Kai Nielsen, Philip L. Quinn, Arthur Schopenhauer, and Walter T. Stace. The only anthology of its kind, The Meaning of Life, Second Edition, is ideal for courses in introduction to philosophy and human nature. It also provides an accessible and stimulating introduction to the subject for general readers. (shrink)

This work has been selected by scholars as being culturally important, and is part of the knowledge base of civilization as we know it. This work was reproduced from the original artifact, and remains as true to the original work as possible. Therefore, you will see the original copyright references, library stamps (as most of these works have been housed in our most important libraries around the world), and other notations in the work. This work is in the public domain (...) in the United States of America, and possibly other nations. Within the United States, you may freely copy and distribute this work, as no entity (individual or corporate) has a copyright on the body of the work. As a reproduction of a historical artifact, this work may contain missing or blurred pages, poor pictures, errant marks, etc. Scholars believe, and we concur, that this work is important enough to be preserved, reproduced, and made generally available to the public. We appreciate your support of the preservation process, and thank you for being an important part of keeping this knowledge alive and relevant. (shrink)

Because factory-farmed meat production inflicts gratuitous suffering upon animals and wreaks havoc on the environment, there are morally compelling reasons to become vegetarian. Yet industrial plant agriculture causes the death of many field animals, and this leads some to question whether consumers ought to get some of their protein from certain kinds of non factory-farmed meat. Donald Bruckner, for instance, boldly argues that the harm principle implies an obligation to collect and consume roadkill and that strict vegetarianism is thus immoral. (...) But this argument works only if the following claims are true: all humans have access to roadkill, roadkill would go to waste if those who happen upon it don’t themselves consume it, it’s impossible to harvest vegetables without killing animals, the animals who are killed in plant production are all-things-considered harmed by crop farming, and the best arguments for vegetarianism all endorse the harm principle. As I will argue in this paper, each claim is deeply problematic. Consequently, in most cases, humans ought to strictly eat plants and save the roadkill for cats. (shrink)

This chapter introduces and defends a pragmatist model of aesthetic disagreement that avoids many of the philosophical puzzles generated by the traditional, semantic, approach. Mainstream philosophical inquiry into aesthetic disagreement begins with a rather innocuous assumption: to understand what’s going on we must first explain what disputants are saying, which involves identifying the meaning of the relevant expressions or determining how aesthetic claims could be true. However, this task brings with it a new host of semantic and epistemic puzzles and (...) fails to vindicate the central role aesthetic disagreements occupy in our aesthetic lives more generally. Further, it isn’t clear how settling the meaning of aesthetic expressions bears on everyday aesthetic disagreements. Paying attention to what we do in an aesthetic disagreement will give us a better chance at identifying what matters for determining what we say. (shrink)

Introduction , Sophie Gibb 1. Mental Causation , John Heil 2. Physical Realization without Preemption , Sydney Shoemaker 3. Mental Causation in the Physical World , Peter Menzies 4. Mental Causation: Ontology and Patterns of Variation , Paul Noordhof 5. Causation is Macroscopic but not Irreducible , David Papineau 6. Substance Causation, Powers, and Human Agency , E. J. Lowe 7. Agent Causation in a Neo-Aristotelian Metaphysics , Jonathan D. Jacobs and Timothy O’Connor 8. Mental Causation and Double Prevention , (...) Sophie Gibb 9. The Identity Theory as a Solution to the Exclusion Problem , David Robb 10. Continuant Causation, Fundamentality, and Freedom , Peter Simons 11. There is no Exclusion Problem , Steinvor Tholl Arnadottir and Tim Crane. (shrink)