From ancient times to the present, the discovery and presentation of new proofs of previously established theorems has been a salient feature of mathematical practice. Why? What purposes are served by such endeavors? And how do mathematicians judge whether two proofs of the same theorem are essentially different? Consideration of such questions illuminates the roles that proofs play in the validation and communication of mathematical knowledge and raises issues that have yet to be resolved by mathematical logicians. The Appendix, in (...) which several proofs of the Fundamental Theorem of Arithmetic are compared, provides a miniature case study. (shrink)
Science and technology studies (STS) research challenges the concept of technological determinism by investigating how the end users of a technology influence that technology’s trajectory. STS critiques of determinism are needed in studies of agricultural technology. However, we contend that focusing on the agency of end users may mask the role of political-economic factors which influence technology developments and applications. This paper seeks to mesh STS insights with political-economic perspectives by accounting for relationships between availability of diverse technologies, variations in (...) political-economic structures, and farmer interests and characteristics. We present the results of an analysis on the recent development of three wheat varieties: (a) a wheat variety that was modified genetically to tolerate the herbicide glyphosate, (b) wheat varieties with characteristics selected to serve specific markets, (c) and emerging research and development of perennial wheat varieties. Using data obtained through a survey of wheat growers in Washington State, we analyzed whether farmer interest in these three clusters of wheat varieties was associated with distinct individual characteristics and attitudes and whether those characteristics and attitudes are consistent with political economic structures. Although our analysis did not allow us to assess the degree of direct influence that farmers have on the technological development trajectory for these types of wheat, we were able to document variation in technological alternatives and farmer characteristics related to different political-economic trends. (shrink)
Three decades of concern over consumption of potentially contaminated Great Lakes fish has led government agencies and public health proponents to implement risk assessment and management programs as a means of protecting the health of fishers and their families. While well-meaning in their intent, these programs––and much of the research conducted to support and evaluate them––were not designed to accommodate the understandings and concerns of the fish consumer. Results from a qualitative component of a multi-disciplinary, multi-year research project on frequent (...) (average 108 meals per year) consumers of Great Lakes fish tell the fishers’ side of the story. We present data from 87 tape recorded interviews conducted with Vietnamese, Chinese, and English-speaking participants that underscore the quality of freshly caught Great Lakes fish and the important social and cultural benefits of fish and fishing to the consumer. We also outline the participants’ understandings of risk from eating Great Lakes fish and the way in which fishers and their families manage this risk. The paper concludes with a discussion of these benefits, risks, and risk management strategies as ways that Great Lakes fish consumers “construct” rather than “perceive” risk. We advocate for risk assessment and management protocols that involve those who will be affected the most, such as frequent consumers of Great Lakes fish, from the initial “risk characterization” stage through to any necessary risk communication. (shrink)
Though regarded today as one of the most important results in logic, the compactness theorem was largely ignored until nearly two decades after its discovery. This paper describes the vicissitudes of its evolution and transformation during the period 1930-1970, with special attention to the roles of Kurt Gödel, A. I. Maltsev, Leon Henkin, Abraham Robinson, and Alfred Tarski.
As initially envisioned, Gödel's Collected Works were to include transcriptions of material from his mathematical workbooks. In the end that material, as well as some other manuscript items from Gödel's Nachlass, had to be left out. This note describes some of the unpublished items in the Nachlass that are likely to attract the notice of scholars and surveys the extent of shorthand transcription efforts undertaken hitherto. Some examples of sources outside Gödel's Nachlass that may be of interest to Gödel scholars (...) are also indicated. (shrink)
According to several commentators, Kurt Godel's incompleteness discoveries were assimilated promptly and almost without objection by his contemporaries - - a circumstance remarkable enough to call for explanation. Careful examination reveals, however, that there were doubters and critics, as well as defenders and rival claimants to priority. In particular, the reactions of Carnap, Bernays, Zermelo, Post, Finsler, and Russell, among others, are considered in detail. Documentary sources include unpublished correspondence from Godel's Nachlass.
Objectives To conduct an independent evaluation of the first phase of the Health Foundation’s Safer Patients Initiative (SPI), and to identify the net additional effect of SPI and any differences in changes in participating and non-participating NHS hospitals. Design Mixed method evaluation involving five substudies, before and after design. Setting NHS hospitals in the United Kingdom. Participants Four hospitals (one in each country in the UK) participating in the first phase of the SPI (SPI1); 18 control hospitals. Intervention The SPI1 (...) was a compound (multi-component) organisational intervention delivered over 18 months that focused on improving the reliability of specific frontline care processes in designated clinical specialties and promoting organisational and cultural change. Results Senior staff members were knowledgeable and enthusiastic about SPI1. There was a small (0.08 points on a 5 point scale) but significant (P<0.01) effect in favour of the SPI1 hospitals in one of 11 dimensions of the staff questionnaire (organisational climate). Qualitative evidence showed only modest penetration of SPI1 at medical ward level. Although SPI1 was designed to engage staff from the bottom up, it did not usually feel like this to those working on the wards, and questions about legitimacy of some aspects of SPI1 were raised. Of the five components to identify patients at risk of deterioration—monitoring of vital signs (14 items); routine tests (three items); evidence based standards specific to certain diseases (three items); prescribing errors (multiple items from the British National Formulary); and medical history taking (11 items)—there was little net difference between control and SPI1 hospitals, except in relation to quality of monitoring of acute medical patients, which improved on average over time across all hospitals. Recording of respiratory rate increased to a greater degree in SPI1 than in control hospitals; in the second six hours after admission recording increased from 40% (93) to 69% (165) in control hospitals and from 37% (141) to 78% (296) in SPI1 hospitals (odds ratio for “difference in difference” 2.1, 99% confidence interval 1.0 to 4.3; P=0.008). Use of a formal scoring system for patients with pneumonia also increased over time (from 2% (102) to 23% (111) in control hospitals and from 2% (170) to 9% (189) in SPI1 hospitals), which favoured controls and was not significant (0.3, 0.02 to 3.4; P=0.173). There were no improvements in the proportion of prescription errors and no effects that could be attributed to SPI1 in non-targeted generic areas (such as enhanced safety culture). On some measures, the lack of effect could be because compliance was already high at baseline (such as use of steroids in over 85% of cases where indicated), but even when there was more room for improvement (such as in quality of medical history taking), there was no significant additional net effect of SPI1. There were no changes over time or between control and SPI1 hospitals in errors or rates of adverse events in patients in medical wards. Mortality increased from 11% (27) to 16% (39) among controls and decreased from 17% (63) to 13% (49) among SPI1 hospitals, but the risk adjusted difference was not significant (0.5, 0.2 to 1.4; P=0.085). Poor care was a contributing factor in four of the 178 deaths identified by review of case notes. The survey of patients showed no significant differences apart from an increase in perception of cleanliness in favour of SPI1 hospitals. Conclusions The introduction of SPI1 was associated with improvements in one of the types of clinical process studied (monitoring of vital signs) and one measure of staff perceptions of organisational climate. There was no additional effect of SPI1 on other targeted issues nor on other measures of generic organisational strengthening. (shrink)
The word “euthanasia” is hopelessly overloaded with emotional connotations. It means so many things to many different people. The implications of euthanasia associated with the Second World War have often rendered the term unsuitable for discussions of a rational manner. As far as I am concerned, what happened in Germany under Hitler had nothing to do with the classic meaning of a gentle and easy death but was rather simply a policy of mass murder.
We are printing in its entirety the discussion document which sets out a code of professional conduct for nurses published by the Royal College of Nursing in November 1976 together with commentaries by the Assistant Secretary of the British Medical Association, a professor of nursing studies, student nurses and a lawyer. The image of the nurse is still that of one of Florence Nightingale's young ladies or of a member of a religious order who is wholly dedicated to caring for (...) the sick. Today, as this document and the comments upon it show, 'dedication' is still part of the motive which leads a man or woman to become a nurse but in addition, and this is where the public may be ignorant or choose to be ignorant, nursing offers a career where intellectual achievement and the satisfaction of a demanding job bring their proper financial reward and place in the professional community. We are grateful to the Royal College of Nursing for permission to publish this document. (shrink)
We compare several methods of implementing the display (sequent) calculus RA for relation algebra in the logical frameworks Isabelle and Twelf. We aim for an implementation enabling us to formalise within the logical framework proof-theoretic results such as the cut-elimination theorem for RA and any associated increase in proof length. We discuss issues arising from this requirement.
We use a deep embedding of the display calculus for relation algebras ÆRA in the logical framework Isabelle /HOL to formalise a machine-checked proof of cut-admissibility for ÆRA. Unlike other “implementations”, we explicitly formalise the structural induction in Isabelle /HOL and believe this to be the ﬁrst full formalisation of cutadmissibility in the presence of explicit structural rules.
We re-express our theorem on the strong-normalisation of display calculi as a theorem about the well-foundedness of a certain ordering on first-order terms, thereby allowing us to prove the termination of systems of rewrite rules. We first show how to use our theorem to prove the well-foundedness of the lexicographic ordering, the multiset ordering and the recursive path ordering. Next, we give examples of systems of rewrite rules which cannot be handled by these methods but which can be handled by (...) ours. Finally, we show that our method can also prove the termination of the Knuth-Bendix ordering and of dependency pairs. Keywords: rewriting, termination, well-founded ordering, recursive path ordering.. (shrink)
We describe how we used the interactive theorem prover Isabelle to formalise and check the laws of the Timed Interval Calculus (TIC). We also describe some important corrections to, clarifications of, and flaws in these laws, found as a result of our work.