Type theory is a fast-evolving field at the crossroads of logic, computer science and mathematics. This gentle step-by-step introduction is ideal for graduate students and researchers who need to understand the ins and outs of the mathematical machinery, the role of logical rules therein, the essential contribution of definitions and the decisive nature of well-structured proofs. The authors begin with untyped lambda calculus and proceed to several fundamental type systems culminating in the well-known and powerful Calculus of Constructions. The book (...) also covers the essence of proof checking and proof development, and the use of dependent type theory to formalize mathematics. The only prerequisites are a good knowledge of undergraduate algebra and analysis. Carefully chosen examples illustrate the theory throughout. Each chapter ends with a summary of the content, some historical context, suggestions for further reading and a selection of exercises to help readers familiarize themselves with the material. (shrink)

The paper first formalizes the ramified type theory as (informally) described in the Principia Mathematica [32]. This formalization is close to the ideas of the Principia, but also meets contemporary requirements on formality and accuracy, and therefore is a new supply to the known literature on the Principia (like [25], [19], [6] and [7]).As an alternative, notions from the ramified type theory are expressed in a lambda calculus style. This situates the type system of Russell and Whitehead in a modern (...) setting. Both formalizations are inspired by current developments in research on type theory and typed lambda calculus; see [3]. (shrink)

We provide a syntax and a derivation system fora formal language of mathematics called Weak Type Theory (WTT). We give the metatheory of WTT and a number of illustrative examples.WTT is a refinement of de Bruijn''s Mathematical Vernacular (MV) and hence:– WTT is faithful to the mathematician''s language yet isformal and avoids ambiguities.

Typed λ-calculus uses two abstraction symbols which are usually treated in different ways: λx:*.x has as type the abstraction Πx:*.*, yet Πx:*.* has type □ rather than an abstraction; moreover, C is allowed and β-reduction evaluates it, but C is rarely allowed. Furthermore, there is a general consensus that λ and Π are different abstraction operators. While we agree with this general consensus, we find it nonetheless important to allow Π to act as an abstraction operator. Moreover, experience with AUTOMATH (...) and the recent revivals of Π-reduction as in [11, 14], illustrate the elegance of giving Π-redexes a status similar to λ-redexes. However, Π-reduction in the λ-cube faces serious problems as shown in [11, 14]: it is not safe as regards subject reduction, it does not satisfy type correctness, it loses the property that the type of an expression is well-formed and it fails to make any expression that contains a Π-redex well-formed. In this paper, we propose a solution to all those problems. The solution is to use a concept that is heavily present in most implementations of programming languages and theorem provers: abbreviations or let-expressions. We will show that the λ-cube extended with Π-conversion and abbreviations satisfies all the desirable properties of the cube and does not face any of the serious problems of Π-reduction. We believe that this extension of the λ-cube is very useful: it gives a full formal study of two concepts that are useful for theorem proving and programming languages. (shrink)

In this article, we study the prehistory of type theory up to 1910 and its development between Russell and Whitehead's Principia Mathematica ([71], 1910-1912) and Church's simply typed λ-calculus of 1940. We first argue that the concept of types has always been present in mathematics, though nobody was incorporating them explicitly as such, before the end of the 19th century. Then we proceed by describing how the logical paradoxes entered the formal systems of Frege, Cantor and Peano concentrating on Frege's (...) Grundgesetze der Arithmetik for which Russell applied his famous paradox and this led him to introduce the first theory of types, the Ramified Type Theory (RTT). We present RTT formally using the modern notation for type theory and we discuss how Ramsey, Hilbert and Ackermann removed the orders from RTT leading to the simple theory of types STT. We present STT and Church's own simply typed λ-calculus (λ → C) and we finish by comparing RTT, STT and λ → C. (shrink)

At the very beginning of L’Homme-Machine, La Mettrie claims that Leibnizians with their monads have “rather spiritualized matter than materialized the soul”; a few years later Pierre-Louis Moreau de Maupertuis, President of the Berlin Academy of Sciences and natural philosopher with a strong interest in the modes of transmission of ‘genetic’ information, conceived of living minima which he termed molecules, “endowed with desire, memory and intelligence,” in his Système de la nature ou Essai sur les corps organisés. This text first (...) appeared in Latin in 1751 under the title Dissertatio inauguralis metaphysica de universali naturae systemate, with the pseudonym Dr Baumann; it was translated by Maupertuis in 1754 as Essai sur la formation des corps organisés and was later included in his 1756 Œuvres under the title Système de la nature. Now, it is clear that Maupertuis was a kind of Leibnizian; and that his molecule possessed higher-level, ‘mental’ properties. In that sense he falls under the first category described by La Mettrie. But he was also involved in a debate on this issue with Diderot, who put forth a sustained critique of Maupertuis’ theory of the molecule in the additions to his 1753 Pensées sur l’interprétation de la nature. Where Maupertuis attributes higher-level properties to his living minima, Diderot argues that these properties are ‘organizational’, i.e., they can only be properties of the whole. At issue here is the degree of commitment to a form of materialism. (shrink)

In his Philosophical Inquiry concerning Human Liberty (1717), the English deist Anthony Collins proposed a complete determinist account of the human mind and action, partly inspired by his mentor Locke, but also by elements from Bayle, Leibniz and other Continental sources. It is a determinism which does not neglect the question of the specific status of the mind but rather seeks to provide a causal account of mental activity and volition in particular; it is a ‘volitional determinism’. Some decades later, (...) Diderot articulates a very similar determinism, which seeks to recognize the existence of “causes proper to man” (as he says in the Réfutation d’Helvétius). The difference with Collins is that now biological factors are being taken into account. Obviously both the ‘volitional’ and the ‘biological’ forms of determinism are noteworthy inasmuch as they change our picture of the nature of determinism itself, but my interest here is to compare these two determinist arguments, both of which are broadly Spinozist in nature – and as such belong to what Jonathan Israel called in his recent book “the radical Enlightenment,” i.e. a kind of underground Enlightenment constituted by Spinozism – and to see how Collins’ specifically psychological vision and Diderot’s specifically biological vision correspond to their two separate national contexts: determinism in France in the mid-1750s was a much more medico-biological affair than English determinism, which appears to be on a ‘path’ leading to Mill and associationist psychology. (shrink)

This volume emphasizes the diversity and fruitfulness of early modern mechanism as a program, as a concept, as a model. Mechanistic study of the living body but also of the mind and mental processes are examined in careful historical focus, dealing with figures ranging from the first-rank (Bacon, Descartes, Spinoza, Cudworth, Gassendi, Locke, Leibniz, Kant) to less well-known individuals (Scaliger, Martini) or prominent natural philosophers who have been neglected in recent years (Willis, Steno, etc.). The volume moves from early modern (...) medicine and physiology to late Enlightenment and even early 19th-century psychology, always maintaining a conceptual focus. It is a contribution to a newly active field in the history and philosophy of early modern life science. It is of interest to scholars studying the history of medicine and the development of mechanistic theories. (shrink)

Ce livre étudie, à travers une série d'épisodes allant de la philosophie des Lumières à notre époque, le problème du matérialisme dans l'histoire de la philosophie et l’histoire des sciences. Comment comprendre les spécificités de l’histoire du matérialisme, des Lumières à nos jours, au sein de la grande histoire de la philosophie et de l’histoire des sciences ? Quelle est l’actualité de l’opposition classique entre le corps et l’esprit ? Qu’est-ce que le rire ou le rêve peuvent nous apprendre du (...) matérialisme ? En traversant l’histoire de ce concept jusqu’à l’émergence d’un « nouveau matérialisme » contemporain, l’ouvrage vise à revitaliser le matérialisme et sa lecture. -/- . (shrink)

How do we judge whether an action is morally right or wrong? If an action is wrong, what reason does that give us not to do it? Why should we give such reasons priority over our other concerns and values? In this book, T. M. Scanlon offers new answers to these questions, as they apply to the central part of morality that concerns what we owe to each other. According to his contractualist view, thinking about right and wrong is thinking (...) about what we do in terms that could be justified to others and that they could not reasonably reject. He shows how the special authority of conclusions about right and wrong arises from the value of being related to others in this way, and he shows how familiar moral ideas such as fairness and responsibility can be understood through their role in this process of mutual justification and criticism. Scanlon bases his contractualism on a broader account of reasons, value, and individual well-being that challenges standard views about these crucial notions. He argues that desires do not provide us with reasons, that states of affairs are not the primary bearers of value, and that well-being is not as important for rational decision-making as it is commonly held to be. Scanlon is a pluralist about both moral and non-moral values. He argues that, taking this plurality of values into account, contractualism allows for most of the variability in moral requirements that relativists have claimed, while still accounting for the full force of our judgments of right and wrong. (shrink)

Principlism aims to provide a framework to help those working in medicine both to identify moral problems and to make decisions about what to do. For it to meet this aim, the principles included within it must express values that all morally serious people share (or ought to share), and there must be no other values that all morally serious people share (or ought to share). This paper challenges the latter of these claims. I will argue that as a descriptive (...) claim about what values morally serious people do in fact share, principlism is inadequate; more principles would be needed to make this claim true. Furthermore, I will argue that while, taken as a claim about what principles we ought to share, principlism could turn out to be correct, it is either unsupported or unable to meet its aims. The only way in which principlists can avoid these problems is to add to the current four principles. (shrink)

Synthetic biologists aim to generate biological organisms according to rational design principles. Their work may have many beneficial applications, but it also raises potentially serious ethical concerns. In this article, we consider what attention the discipline demands from bioethicists. We argue that the most important issue for ethicists to examine is the risk that knowledge from synthetic biology will be misused, for example, in biological terrorism or warfare. To adequately address this concern, bioethics will need to broaden its scope, contemplating (...) not just the means by which scientific knowledge is produced, but also what kinds of knowledge should be sought and disseminated. (shrink)

"A beautiful piece of work on the theory of altered states of consciousness ." "Stanislav Grof, M.D. author of Realms of the Human Unconsciousness".

Abstract I argue that the two primary motivations in the literature for positing seemings as sui generis mental states are insufficient to motivate this view. Because of this, epistemological views which attempt to put seemings to work don’t go far enough. It would be better to do the same work by appealing to what makes seeming talk true rather than simply appealing to seeming talk. Content Type Journal Article Pages 1-12 DOI 10.1007/s11406-012-9363-8 Authors T. Ryan Byerly, Department of Philosophy, Baylor (...) University, Waco, TX, USA Journal Philosophia Online ISSN 1574-9274 Print ISSN 0048-3893. (shrink)

Some philosophers have thought that life could only be meaningful if there is no God. For Sartre and Nagel, for example, a God of the traditional classical theistic sort would constrain our powers of self-creative autonomy in ways that would severely detract from the meaning of our lives, possibly even evacuate our lives of all meaning. Some philosophers, by contrast, have thought that life could only be meaningful if there is a God. God and the Meanings of Life is interested (...) in exploring the truth in both these schools of thought, seeking to discover what God could and couldn't do to make life meaningful (as well as what he would and wouldn't do). Mawson espouses a version of the 'amalgam' or 'pluralism' thesis about the issue of life's meaning – in essence, that there are a number of different legitimate meanings of 'meaning' (and indeed 'life') in the question of life's meaning. According to Mawson, God, were he to exist, would help make life meaningful in some of these senses and hinder in some others. He argues that whilst there could be meaning in a Godless universe, there could be other sorts of meaning in a Godly one and that these would be deeper. (shrink)

This is the text of The Lindley Lecture for 1996, given by T.M. Scanlon, an American philosopher.

The four principles approach to medical ethics plus specification is used in this paper. Specification is defined as a process of reducing the indeterminateness of general norms to give them increased action guiding capacity, while retaining the moral commitments in the original norm. Since questions of method are central to the symposium, the paper begins with four observations about method in moral reasoning and case analysis. Three of the four scenarios are dealt with. It is concluded in the “standard” Jehovah’s (...) Witness case that having autonomously chosen the authority of his religious institution, a Jehovah’s Witness has a reasonable basis on which to refuse a recommended blood transfusion. The author’s view of the child of a Jehovah’s Witness scenario is that it is morally required—not merely permitted—to overrule this parental refusal of treatment. It is argued in the selling kidneys for transplantation scenario that a fair system of regulating and monitoring would be better than the present system which the author believes to be a shameful failure. (shrink)