The Curry-Howard isomorphism states an amazing correspondence between systems of formal logic as encountered in proof theory and computational calculi as found in type theory. For instance, minimal propositional logic corresponds to simply typed lambda-calculus, first-order logic corresponds to dependent types, second-order logic corresponds to polymorphic types, sequent calculus is related to explicit substitution, etc. The isomorphism has many aspects, even at the syntactic level: formulas correspond to types, proofs correspond to terms, provability corresponds to inhabitation, proof normalization corresponds to (...) term reduction, etc. But there is more to the isomorphism than this. For instance, it is an old idea---due to Brouwer, Kolmogorov, and Heyting---that a constructive proof of an implication is a procedure that transforms proofs of the antecedent into proofs of the succedent; the Curry-Howard isomorphism gives syntactic representations of such procedures. The Curry-Howard isomorphism also provides theoretical foundations for many modern proof-assistant systems (e.g. Coq). This book give an introduction to parts of proof theory and related aspects of type theory relevant for the Curry-Howard isomorphism. It can serve as an introduction to any or both of typed lambda-calculus and intuitionistic logic. Key features - The Curry-Howard Isomorphism treated as common theme - Reader-friendly introduction to two complementary subjects: Lambda-calculus and constructive logics - Thorough study of the connection between calculi and logics - Elaborate study of classical logics and control operators - Account of dialogue games for classical and intuitionistic logic - Theoretical foundations of computer-assisted reasoning · The Curry-Howard Isomorphism treated as the common theme. · Reader-friendly introduction to two complementary subjects: lambda-calculus and constructive logics · Thorough study of the connection between calculi and logics. · Elaborate study of classical logics and control operators. · Account of dialogue games for classical and intuitionistic logic. · Theoretical foundations of computer-assisted reasoning. (shrink)

Quillen [17] introduced model categories as an abstract framework for homotopy theory which would apply to a wide range of mathematical settings. By all accounts this program has been a success and—as, e.g., the work of Voevodsky on the homotopy theory of schemes [15] or the work of Joyal [11, 12] and Lurie [13] on quasicategories seem to indicate—it will likely continue to facilitate mathematical advances. In this paper we present a novel connection between model categories and mathematical logic, inspired (...) by the groupoid model of (intensional) Martin–Löf type theory [14] due to Hofmann and Streicher [9]. In particular, we show that a form of Martin–Löf type theory can be soundly modelled in any model category. This result indicates moreover that any model category has an associated “internal language” which is itself a form of Martin-Löf type theory. This suggests applications both to type theory and to homotopy theory. Because Martin–Löf type theory is, in one form or another, the theoretical basis for many of the computer proof assistants currently in use, such as Coq and Agda (cf. [3] and [5]), this promise of applications is of a practical, as well as theoretical, nature. This paper provides a precise indication of this connection between homotopy theory and logic; a more detailed discussion of these and further results will be given in [20]. (shrink)

This full-length study of Plato's dialogue Phaedrus, now in paperback, is written in the belief that such concerted scrutiny of a single dialogue is an important part of the project of understanding Plato so far as possible 'from the inside' - of gaining a feel for the man's philosophy. The focus of this account is on how the resources both of persuasive myth and of formal argument, for all that Plato sets them in strong contrast, nevertheless complement and reinforce each (...) other in his philosophy. Not only is the dialogue in its formal structure a dovetail of myth and argument, but the philosophic life that it praises is also shaped by an acknowledgement of the limitations of argument and the importance of mythical understanding. By means of this correlation of form and content Plato invites his readers, through the very act of reading, to take a first step along the path of the philosophical life. (shrink)

According to the ‘conceivability argument’ [1] it’s conceivable that a conscious human being H may have a perfect physical duplicate H* who isn’t conscious, [2] whatever is conceivable is possible, therefore [3] H* may possibly exist. This paper argues that the conceivability argument can’t help in discussion of the ‘mind–body problem’ even if [2] is allowed to be true. This is not because [1] is false, but because we don’t and can’t know enough about the nature of the physical to (...) know whether or not [1] is true. This follows from ‘the silence of physics’—the fact that physics neither does nor can tell us about the intrinsic non-structural nature of the physical, and the consequences of this fact for any adequate account of the meaning of the word ‘physical’. (shrink)

This is the long-awaited publication of a set of writings by the British philosopher, historian, and archaeologist R.G. Collingwood (1889-1943) on critical, anthropological, and cultural themes only hinted at in his previously available work. At the core are six essays on folktale and magic in which Collingwood applies the principles of his philosophy of history to problems in the long-term evolution of human society and culture. The volume opens with three substantial introductory essays by the editors, authorities in their various (...) fields, who provide their explanatory and contextual notes to guide the reader through the texts. The Philosophy of Enchantment highlights the broad range of Collingwood's intellectual engagements, their integration, and their relevance to current areas of debate in the fields of philosophy, cultural studies, social and literary history, and anthropology. (shrink)

Originally published in 1965. This is a textbook of modern deductive logic, designed for beginners but leading further into the heart of the subject than most other books of the kind. The fields covered are the Propositional Calculus, the more elementary parts of the Predicate Calculus, and Syllogistic Logic treated from a modern point of view. In each of the systems discussed the main emphases are on Decision Procedures and Axiomatisation, and the material is presented with as much formal rigour (...) as is compatible with clarity of exposition. The techniques used are not only described but given a theoretical justification. Proofs of Consistency, Completeness and Independence are set out in detail. The fundamental characteristics of the various systems studies, and their relations to each other are established by meta-logical proofs, which are used freely in all sections of the book. Exercises are appended to most of the chapters, and answers are provided. (shrink)

In his target paper, John Welwood tells us that we have to beware of 'spiritual bypassing -- using spiritual ideas and practices to sidestep personal, emotional -- unfinished business--, to shore up a shaky sense of self, or to belittle basic needs, feelings, and develop-mental tasks, all in the name of enlightenment'. It's arguable that there is an equal danger of 'narrative bypassing' -- using the idea of one's life as a narrative to 'sidestep personal, emotional --unfinished business--, to shore (...) up a shaky sense of self -- all in the name of' a good life. (shrink)

Taking a set of central issues from ancient Greek medicine and biology, this book studies firstly, the interaction between scientific theorising and folklore or popular assumptions; secondly, the ideological character of scientific inquiry. Topics of interest in the philosphy and sociology of science illuminated here include the relationship between primitive thought and early science, the roles of the consensus on the scientific community, tradition and the authority of the written text, in the development of science.

This chapter contains section titled: Introduction.

This book is a study of the origins and development of Greek science, focusing especially on the interactions of scientific and traditional patterns of thought from the sixth to the fourth centuries BC. The starting point is an examination of how certain Greek authors deployed the category of 'magic' and attacked magical beliefs and practices, and these attacks are related to their complex background in Greek medicine and speculative thought. In his second chapter Dr Lloyd outlines the development, and assesses (...) the significance, of the theory and practice of argument in early Greek science, and he follows this with a study of the development of empirical research. Finally the author confronts the question of why the Greeks invented science: what precisely was their contribution to science, and what social, economic, ideological and political factors had a bearing on the growth of science in Greece. (shrink)

First published in 2000, this translation of one of the great works of Western political thought is based on the assumption that when Plato chose the dialogue form for his writing, he intended these dialogues to sound like conversations - although conversations of a philosophical sort. In addition to a vivid, dignified and accurate rendition of Plato's text, the student and general reader will find many aids to comprehension in this volume: an introduction that assesses the cultural background to the (...) Republic, its place within political philosophy, and its general argument; succinct notes in the body of the text; an analytical summary of the work's content; a full glossary of proper names; a chronology of important events; and a guide to further reading. The result is an accomplished and accessible edition of this seminal work, suitable for philosophers and classicists as well as historians of political thought at all levels. (shrink)

Research examining firm and industry effects on performance has primarily focused on the financial aspects of firm performance. Corporate social performance is a major aspect of firm performance that has been under-examined empirically in the literature to date. Adding to the fundamental debate regarding firm versus industry effects on performance, this study uses data drawn from the Kinder, Lydenberg and Domini Co. database to examine the degree to which CSP is related to firm, industry, and temporal factors. The results of (...) these analyses suggest that CSP tends to change in a linear manner over time; however, the slope of this line varies across firms and industries. These findings are supported by several robustness checks accounting for autocorrelation, alternative measures of industry, different samples commonly used when using KLD data to measure CSP, and alternative measures of CSP when using the KLD database. The authors also directly compare firm, industry, and temporal effects between CSP and financial performance. (shrink)

David Hitchcock, in his recent “Informal Logic and the Concept of Argument”, defends a recursive definition of ‘argument.’ I present and discuss several problems that arise for his definition. I argue that refining Hitchcock’s definition in order to resolve these problems reveals a crucial, but minimally explicated, relation that was, at best, playing an obscured role in the original definition or, at worst, completely absent from the original definition.

2011 Reprint of 1943 Edition. Full facsimile of the original edition, not reproduced with Optical Recognition Software. "St. Thomas Aquinas" is enriched by the author's unique ability to see the world through the saint's eyes, a fresh and animated view that shows us Aquinas as no other biography has. Acclaimed as the best book ever written on Aquinas by such outstanding Thomists as Jacques Maritain, Etienne Gilson, and Anton Pegis, this brilliant biography will completely capture the reader and leave him (...) desirous of reading Aquinas' own monumental work. (shrink)

An engaging argument about what experimental music can tell us about being human. -/- In Experimenting the Human, G Douglas Barrett argues that experimental music speaks to the contemporary posthuman, a condition in which science and technology decenter human agency amid the uneven temporality of postwar global capitalism. Time moves forward for some during this period, while it seems to stand still or even move backward for others. Some say we’re already posthuman, while others endure the extended consequences of never (...) having been considered fully human in the first place. Experimental music reflects on this state, Barrett contends, through its interdisciplinary involvements in postwar science, technology, and art movements. -/- Rather than pursuing the human’s beyond, experimental music addresses the social and technological conditions that support such a pursuit. Barrett locates this tendency of experimentalism throughout its historical entanglements with cybernetics, and in his intimate analysis of Alvin Lucier’s neurofeedback music, Pamela Z’s BodySynth performances, Nam June Paik’s musical robotics, Pauline Oliveros’s experiments with radio astronomy, and work by Laetitia Sonami, Yasunao Tone, and Jerry Hunt. Through a unique meeting of music studies, media theory, and art history, Experimenting the Human provides fresh insights into what it means to be human. (shrink)

The empirical investigations over the past fifteen years of evolutionary biologists and cognitive scientists have demonstrated the accessibility and power of the human brain. Whatever moral concepts used to acknowledge the normative appraisals of human conduct are now explained through neurological hardwiring. This essay outlines some of the main views of proponents, but especially Marc Hauser, and I argue that it does not render the end of morals. It does provide an opportunity to view the facts of how the brain (...) functions but this essay finds a large domain of valuing unable to be justified by these new scientific challenges. (shrink)