This introduction to the basic ideas of structural proof theory contains a thorough discussion and comparison of various types of formalization of first-order logic. Examples are given of several areas of application, namely: the metamathematics of pure first-order logic (intuitionistic as well as classical); the theory of logic programming; category theory; modal logic; linear logic; first-order arithmetic and second-order logic. In each case the aim is to illustrate the methods in relatively simple situations and then apply them elsewhere in much (...) more complex settings. There are numerous exercises throughout the text. In general, the only prerequisite is a standard course in first-order logic, making the book ideal for graduate students and beginning researchers in mathematical logic, theoretical computer science and artificial intelligence. For the new edition, many sections have been rewritten to improve clarity, new sections have been added on cut elimination, and solutions to selected exercises have been included. (shrink)

Provability, Computability and Reflection.

This paper studies, by way of an example, the intuitionistic propositional connective * defined in the language of second order propositional logic by * ≡ ∃Q. In full topological models * is not generally definable but over Cantor-space and the reals it can be classically shown that *↔ ⅂⅂P; on the other hand, this is false constructively, i.e. a contradiction with Church's thesis is obtained. This is comparable with some well-known results on the completeness of intuitionistic first-order predicate logic. Over (...) [0, 1], the operator * is undefinable. We show how to recast this argument in terms of intuitive intuitionistic validity in some parameter. The undefinability argument essentially uses the connectedness of [0, 1]; most of the work of recasting consists in the choice of a suitable intuitionistically meaningful parameter, so as to imitate the effect of connectedness. Parameters of the required kind can be obtained as so-called projections of lawless sequences. (shrink)

Dans la genese de sa constitution, la philosophie n'a pu faire l'economie d'une confrontation avec la musique qui fournissait aux anciens Grecs les schemes fondamentaux de la culture. De cette confrontation Platon est le temoin. Scindant la musique, il privilegie l'Harmonique, qui en est la partie theorique, sans toutefois lui reconnaitre la titre de science supreme. Correlativement, il condamne comme dysharmonie, tumulte fracassant et perturbateur de l'ordre cosmique, l'harmonie chromaticiste dont il s'emploie, non sans paradoxe, a decrire le detail. Par (...) cette lecture en filigrane des Dialogues de Platon, l'auteur se propose de reconstruire la pensee qui procede de l'harmonie chromaticiste et de montrer son importance dans l'elaboration de la philosophie fondatrice. Au carrefour des disciplines du savoir antique, ce livre s'adresse non seulement aux philosophes, mais aussi a tous ceux qui, musiciens ou stylisticiens, s'interessent a la forme musicale. (shrink)

The paper deals with two versions of the fragment with unit, tensor, linear implication and storage operator of intuitionistic linear logic. The first version, ILL, appears in a paper by Benton, Bierman, Hyland and de Paiva; the second one, ILL+, is described in this paper. ILL has a contraction rule and an introduction rule !I for the exponential; in ILL+, instead of a contraction rule, multiple occurrences of labels for assumptions are permitted under certain conditions; moreover, there is a different (...) introduction rule for the exponential, !I+, which is closer in spirit to the necessitation rule for the normalizable version of S4 discussed by Prawitz in his monograph “Natural Deduction”.It is relatively easy to adapt Prawitz's treatment of natural deduction for intuitionistic logic to ILL+; in particular one can formulate a notion of strong validity permitting a proof of strong normalization.The conversion rules for ILL explicitly mentioned in the paper by Benton et al. do not suffice for normal forms with subformula property, but we can show that this can be remedied by addition of a special permutation conversion plus some “satellite” permutation conversions.Some discussion of the categorical models which might correspond to ILL+ is given. (shrink)

In this paper, I take a critical look at Sartorio’s book Causation and Free Will (2016). Sartorio offers a rich defence of an actual-sequence view of freedom, which pays close attention to issues in the philosophy of causation and how they relate to freedom. I argue that although this focus on causation is illuminating, Sartorio’s project nevertheless runs into some serious difficulties. Perhaps most worrying amongst them is whether the agent-based reason-sensitivity account, offered by Sartorio, is consistent with Frankfurt-style cases (...) – the very cases which are provided as the sole reason to endorse an actual-sequence view of freedom. I suggest that given that powers and causation are so intimately bound together, the debate is skewed somewhat by thinking of these as rivals. (shrink)

In this note we shall assume acquaintance with [T4] and the parts of [T1] which deal with intuitionistic arithmetic in all finite types. The bibliography just continues the bibliography of [T4].The principal purpose of this note is the discussion of two models for intuitionistic finite type arithmetic with fan functional. The first model is needed to correct an oversight in the proof of Theorem 6 [T4, §5]: the model ECF+as defined there cannot be shown to have the required properties inEL+ (...) QF-AC, the reason being that a change in the definition ofW12alone does not suffice—if one wishes to establish closure under the operations of HAωthe definitions ofW1σfor other σ have to be adopted as well. It is difficult to see how to do this directly in a uniform way — but we succeed via a detour, which is described in §2.For a proper understanding, we should perhaps note already here thaton the assumption of the fan theorem, ECF+as defined in [T4] and the new model of this note coincide ; but inELit is impossible to prove this. (shrink)

_A portion of the revenue from this book’s sales will be donated to Doctors Without Borders to assist the humanitarian work of nurses, doctors, and other health care providers in the fight against COVID-19 and beyond._ _Concepts and Cases in Nursing Ethics_ is an introduction to contemporary ethical issues in health care, designed especially for Canadian audiences. The book is organized around six key concepts: beneficence, autonomy, truth-telling, confidentiality, justice, and integrity. Each of these concepts is explained and discussed with (...) reference to professional and legal norms. The discussion is then supplemented by case studies that exemplify the relevant concepts and show how each applies in health care and nursing practice. This new fourth edition includes an added chapter on end-of-life issues, and it is revised throughout to reflect the latest developments on topics such as global health ethics, cultural competence, social media, and palliative sedation, as well as ethical issues relating to COVID-19. (shrink)

In this paper we discuss a particular example of the passage from the informal, but rigorous description of a concept to the axiomatic formulation of principles holding for the concept; in particular, we look at the principles of continuity and lawlike choice in the theory of lawless sequences. Our discussion also leads to a better understanding of the rôle of the so-called density axiom for lawless sequences.

This paper studies, by way of an example, the intuitionistic propositional connective * defined in the language of second order propositional logic by. In full topological models * is not generally definable, but over Cantor-space and the reals it can be classically shown that; on the other hand, this is false constructively, i.e. a contradiction with Church's thesis is obtained. This is comparable with some well-known results on the completeness of intuitionistic first-order predicate logic.Over [0, 1], the operator * is (...) (constructively and classically) undefinable. We show how to recast this argument in terms of intuitive intuitionistic validity in some parameter. The undefinability argument essentially uses the connectedness of [0, 1]; most of the work of recasting consists in the choice of a suitable intuitionistically meaningful parameter, so as to imitate the effect of connectedness. (shrink)

The meaning of life and man's alienation from himself and his natural environment is examined in brief selections, illustrated with photographs, from the works of Albert Schweitzer.

Pionnière dans la pénalisation du viol en 1980, la France a été en eurocrime qu’aurait entraîné l’unanimité dans l’acceptation de la nouvelle définition proposée par la Commission européenne. L’absence de consentement devient finalement pour tous le critère principal, et de nombreux pays ont aligné récemment leur législation avec la directive européenne. Sur le droit à l’avortement, la convergence est moins sensible, plusieurs pays mettent d’importantes restrictions. La constitutionnalisation de la liberté d’avorter et de sa garantie en France va peut-être conduire (...) à son inscription dans les droits humains. (shrink)

Was passiert, wenn die Bevölkerung die Möglichkeit erhält, sich ungeschminkt und ungefiltert zu bioethischen Problemstellungen zu äußern?

Concepts and Cases in Nursing Ethics maps the ethical landscape of contemporary nursing. The book is the product of a collaboration between philosopher-ethicist Michael Yeo, nurse-ethicist Anne Moorhouse, and six representatives of various areas of professional nursing. It thus combines philosophical and ethical analysis with nursing knowledge and experience in a manner that is both understandable and relevant. The book is organized around six main concepts in nursing ethics: beneficence, autonomy, confidentiality, truth-telling, justice, and integrity. A chapter is devoted (...) to the elucidation of each of these concepts. In each chapter, historical background and conceptual analysis are supplemented by case studies that exemplify issues and show how the concept applies in nursing practice. In this new edition, the materials in each chapter have been updated to reflect recent developments in nursing and more generally in health care. In addition, a totally new chapter on ethical theory has been added. Complete with bibliographies and study questions for further analysis of cases, this book is ideally suited for textbook use. It will help both practitioners and students to deal better with the clinical problems and issues that are encountered in the field. However, it's simple prose and clear exposition of complex issues will make Concepts and Cases in Nursing Ethics attractive to anyone concerned about health care. (shrink)

This long-awaited two-volume set constitutes the definitive presentation of the system of classifying moral judgment built up by Lawrence Kohlberg and his associates over a period of twenty years. Researchers in child development and education around the world, many of whom have worked with interim versions of the system, indeed, all those seriously interested in understanding the problem of moral judgment, will find it an indispensable resource. Volume I reviews Kohlberg's stage theory, and the by-now large body of research on (...) the significance and utility of his moral stages. Issues of reliability and validity are addressed. The volume ends with detailed instructions for using the forms in Volume 2. Volume 2, in a specially-designed, user-friendly format, includes three alternative functionally-equivalent forms of the scoring system. (shrink)

The paper discusses the transition from informal concepts to mathematically precise notions; examples are given, and in some detail the case of lawless sequences, a concept of intuitionistic mathematics, is discussed. A final section comments on philosophical discussions concerning intuitionistic logic in connection with a ‘theory of meaning’.

Several studies have observed an inverse relationship between attention deficit hyperactivity disorder -related behavior of children, as reported by parents or teachers, and the amount of green space in their residential environment. Research using other, more objective measures to determine ADHD prevalence is scarce and could strengthen the evidence base considerably. In this study, it is investigated whether a similar beneficial association will be observed if the use of ADHD-related medication is selected as an outcome measure. More specifically, registry data (...) from a health insurance company on the reimbursement of ADHD-related medication in 2011 were available for 248,270 children between 5 and 12 years of age. Amounts of green space within 250 and 500 m of the home address were calculated. Multilevel logistic regression analyses for the prevalence of use were conducted, including the following covariates: sex, age, urbanity of the neighborhood, neighborhood socioeconomic status, and percentage of people with a non-Western migration background in the neighborhood population. Results showed that the amount of green space was inversely related to the prevalence of use of ADHD medication. Moreover, the relationship was strongest among children living in the least wealthy neighborhoods and absent among those living in the wealthiest neighborhoods. Results also show that in less wealthy neighborhoods, there is, on average, less green space available nearby: children who are likely to benefit most from nearby green space tend to have the least of it. (shrink)

This book is an intercultural exploration of the full scope of evil. The problems of evil have beset humanity throughout the ages and continue to trouble us. The studies here examine evil in Asian thought, in Western theory, in the cosmic order, in human psychology, and in social practice. Insights are added to the philosophical discussions from religion, culture, history, law, technology, and literature.

The paper discusses the relationship between normal natural deductions and cutfree proofs in Gentzen (sequent) calculi in the absence of term labeling. For Gentzen calculi this is the usual version; for natural deduction this is the version under the complete discharge convention, where open assumptions are always discharged as soon as possible. The paper supplements work by Mints, Pinto, Dyckhoff, and Schwichtenberg on the labeled calculi.