Cartesian closed categories (CCCs) have played and continue to play an important role in the study of the semantics of programming languages. An axiomatization of the isomorphisms which hold in all Cartesian closed categories discovered independently by Soloviev and Bruce, Di Cosmo and Longo leads to seven equalities. We show that the unification problem for this theory is undecidable, thus settling an open question. We also show that an important subcase, namely unification modulo the linear isomorphisms, is NP-complete. Furthermore, the (...) problem of matching in CCCs is NP-complete when the subject term is irreducible. CCC-matching and unification form the basis for an elegant and practical solution to the problem of retrieving functions from a library indexed by types investigated by Rittri. It also has potential applications to the problem of polymorphic type inference and polymorphic higher-order unification, which in turn is relevant to theorem proving and logic programming. (shrink)

In this paper we consider the problem of the existence of a λ-theory T such that:–T is recursive enumerable;–the ω-rule holds in T .We solve affirmatively this problem.Some related questions are also discussed.

Moral dilemmas set a challenge for ethical theory. They are situations where agents seem to be under an obligation both to do, and to refrain from doing, a specific act. Are such situations possible? What is their exact nature? These are the questions that _Moral Dilemmas_ tries to answer. The book argues that moral theories should not allow for the possibility of irresolvable dilemmas, for situations in which no right answer exists. To this end, arguments seeking to prove the existence (...) of irresolvable dilemmas, especially the argument from the incommensurability of values, are discussed at length and refuted. The book shows that though on the normative level dilemmas are resolved, they typically involve a high moral cost for which there is no adequate compensation. This moral cost is the source of the regret and pain suffered by agents in moral dilemmas. Thus, moral dilemmas do not point to any inconsistency in our moral reasoning or theory, but to a problematic aspect of the human condition; at times (probably less often than is usually believed), human beings are justified, and even required, to dirty their hands by behaving in ways that in ordinary situations would be strictly forbidden and condemned. (shrink)

Logic has pride of place in mathematics and its 20th century offshoot, computer science. Modern symbolic logic was developed, in part, as a way to provide a formal framework for mathematics: Frege, Peano, Whitehead and Russell, as well as Hilbert developed systems of logic to formalize mathematics. These systems were meant to serve either as themselves foundational, or at least as formal analogs of mathematical reasoning amenable to mathematical study, e.g., in Hilbert’s consistency program. Similar efforts continue, but have been (...) expanded by the development of sophisticated methods to study the properties of such systems using proof and model theory. In parallel with this evolution of logical formalisms as tools for articulating mathematical theories (broadly speaking), much progress has been made in the quest for a mechanization of logical inference and the investigation of its theoretical limits, culminating recently in the development of new foundational frameworks for mathematics with sophisticated computer-assisted proof systems. In addition, logical formalisms developed by logicians in mathematical and philosophical contexts have proved immensely useful in describing theories and systems of interest to computer scientists, and to some degree, vice versa. Three examples of the influence of logic in computer science are automated reasoning, computer verification, and type systems for programming languages. (shrink)

The last decade or so has witnessed a wave of empirical studies purporting to show that men’s sexual focus on the female body leads to increased hostility and aggression against women. According to what I call “The Objectification Hypothesis”, the explanation for this phenomenon has to do with the fact that, in such circumstances, men “objectify” women, that is, regard them as mere objects or as means only. The paper rejects this hypothesis and offers an alternative explanation for the connection (...) between men’s sexual gaze and their aggression against women. This explanation makes no reference to the notions of seeing-other-as-object or of treating-as-means-only. Instead, it locates the dynamic at hand within the theoretical framework of misogyny along the lines developed by Kate Manne. (shrink)

The central question in contemporary ethics is whether virtue can replace duty as the primary notion in ethical theory. The subject of intense contemporary debate in ethical theory, virtue ethics is currently enjoying an increase in interest. This is the first book to focus directly on the subject. It provides a clear, systematic introduction to the area and houses under one cover a collection of the central articles published on the debate over the past decade. The essays encompass a wide (...) range ofaspects: the difference between virtue ethics and traditional duty ethics; present arguments for and against virtue ethics; the practical implications of virtue ethics and the Aristotelian and Kantian attitudes to virtue ethics. (shrink)

We consider three problems concerning alpha conversion of closed terms (combinators). (1) Given a combinator M find the an alpha convert of M with a smallest number of distinct variables. (2) Given two alpha convertible combinators M and N find a shortest alpha conversion of M to N. (3) Given two alpha convertible combinators M and N find an alpha conversion of M to N which uses the smallest number of variables possible along the way. We obtain the following results. (...) (1) There is a polynomial time algorithm for solving problem (1). It is reducible to vertex coloring of chordal graphs. (2) Problem (2) is co-NP complete (in recognition form). The general feedback vertex set problem for digraphs is reducible to problem (2). (3) At most one variable besides those occurring in both M and N is necessary. This appears to be the folklore but the proof is not familiar. A polynomial time algorithm for the alpha conversion of M to N using at most one extra variable is given. There is a tradeoff between solutions to problem (2) and problem (3) which we do not fully understand. (shrink)

This study reconstructs the relationship between philosophy and politics in the way in which Heidegger's failure as a politician influenced the redevelopment of philosophy in the 1930s. The author also explains how Heidegger's failure influenced the content and direction of his later work.

The topic of standing to blame has recently received a lot of attention. Until now, however, it has focused mainly on the blamer's perspective, investigating what it means to say of blamers that they lose standing to blame and why it is that they lose this standing under specified conditions. The present paper focuses on the perspective of the blamees and tries to explain why they are allowed to disregard standingless, more specifically hypocritical, blame. According to the solution proposed by (...) the paper, while hypocritical blamers present themselves as caring about justice or about the moral or material good of the blamees—and they themselves half‐believe this presentation—their real motivation in blaming is less respectable. It is this problematic motivation that explains why blamees are permitted to disregard hypocritical blame. Ill‐motivated blame is often unreliable, and readiness to even consider it often involves a compromise on the self‐respect of the blamees. (shrink)

The paper discusses a neglected condition for justified self-defense, namely, 'The Success Condition [SC].' According to SC, otherwise immoral acts can be justified under the right to self-defense only if they actually achieve the intended defense from the perceived threat. If they don't, they are almost always excused, but not morally justified. I show that SC leads to a troubling puzzle because victims who estimate they cannot prevent the attack against them would be morally required to surrender. I try to (...) solve the puzzle by relying on what I call 'The Honor Solution.' Even if defensive acts fail to protect the victim's body, property, or life, they are successful in protecting her honor, thus they do ultimately meet the success condition. (shrink)

Some luck, in a decision of Gauguin's kind, is extrinsic to his project, some intrinsic; both are necessary for success, and hence for actual justification, but only the latter relates to un- justification. If we now broaden the range of cases slightly, ...

Studies the politics of Heidegger in terms of "thrownness" or "existential contingency". Attempts to think through Heidegger's philosophy in a manner that parallels his own dialogue with other key western thinkers.

The Curry-Howard isomorphism is a proof-theoretic result that establishes a connection between derivations in natural deduction and terms in typed lambda calculus. It is an important proof-theoretic result, but also underlies the development of type systems for programming languages. This fact suggests a potential importance of the result for a philosophy of code.

Pascal’s wager faces serious criticisms and is generally considered unconvincing. We argue that it can make a comeback powered by an unlikely ally: postmodernism. If one denies the existence of objective facts (e.g. about God or His relation to the world), then various non-theological considerations should come to the fore when considering the rationality of religious commitment and the choice of education for one’s children. In fact, we shall argue that, if one genuinely cares about one’s children, then – in (...) many Western countries – one cannot consistently be both secular and post-modernist. (shrink)

Proponents of corporate environmental responsibility argue that corporations shortchange shareholders by investing too little in environmental responsibility. They claim that corporations can improve their financial performance by increasing their investment in environmental responsibility. Opponents of corporate social responsibility argue that corporations shortchange shareholders by investing too much in environmental responsibility. They claim that corporations can improve their financial performance by reducing their investment in environmental responsibility. Yet, others claim that corporations serve their shareholders well by investing just enough in social (...) responsibility, not too little and not too much. If so, corporations increase their investment in environmental responsibility when an increase improves financial performance and reduce their investment in environmental responsibility when a decrease improves financial performance. Our evidence is consistent with this last claim. We find that the behavior of corporations is consistent with the claim that they act in the interest of shareholders, increasing or decreasing their investment in environmental responsibility as necessary to improve their financial performance. (shrink)

The proof theory of many-valued systems has not been investigated to an extent comparable to the work done on axiomatizatbility of many-valued logics. Proof theory requires appropriate formalisms, such as sequent calculus, natural deduction, and tableaux for classical (and intuitionistic) logic. One particular method for systematically obtaining calculi for all finite-valued logics was invented independently by several researchers, with slight variations in design and presentation. The main aim of this report is to develop the proof theory of finite-valued first order (...) logics in a general way, and to present some of the more important results in this area. In Systems covered are the resolution calculus, sequent calculus, tableaux, and natural deduction. This report is actually a template, from which all results can be specialized to particular logics. (shrink)

This classic, provocative introduction to classical metaphysical questions focuses on appreciating the problems, rather than attempting to proffer answers.

Christopher New recently argued for the seemingly paradoxical idea that there is no moral reason not to punish someone before she commits her crime (‘prepunishment’), provided that we can be sure that she will, in fact, commit the crime in the future. I argue that the air of paradox dissolves if we understand the possibility of prepunishment as relying on an anti‐moral‐luck position. However, New does not draw the full conclusions from such a position, which would allow prepunishment even prior (...) to the formation of a wrongful intention, on the basis of the idea that bad character is enough to entail blameworthiness. I conclude by examining a legal system which seems to use the idea of prepunishment, i.e. the Talmudic idea that we might punish a child who has not yet sinned in order to save him from sinning in the future. (shrink)

That an intimate connection exists between the notion of human dignity and the notion of humiliation seems to be a commonplace among philosophers, who tend to assume that humiliation should be explained in terms of (violation of) human dignity. I believe, however, that this assumption leads to an understanding of humiliation that is too "philosophical" and too detached from psychological reality. The purpose of the paper is to modify the above connection and to offer a more "down to earth" account (...) of humiliation that does not depend on metaphysical or axiological questions concerning the unique dignity enjoyed by all human beings qua human beings. The paper argues for a subjective-psychological notion of self-respect in the explication of humiliation, instead of an objective-normative one. To be humiliated means to suffer an actual threat to or fall in one's self-respect. (shrink)

Despite their differences in origin, the three influential schools of twentieth-century continental cultural criticism--the Frankfurt School, existentialism, and poststructuralism--have long been treated as an ensemble and with critical hesitancy. Examining these schools as responses to the apparent collapse of Western civilization in the twentieth-century and as formidable intellectual challenges to the cultural legacies of the Enlightenment, this book provides a productive base for criticism and broadens our understanding of their histories and reception.

Yitzhak Benbaji and Daniel Statman present a new theory on the ethics of war which shows that wars can be morally justified at both the ad bellum level and the in bello level.

Having visited Ireland regularly during the 1930s, Ludwig Wittgenstein resigned his Cambridge philosophy professorship in 1947 and moved there, living in a fishing village on the Atlantic coast and hotels in Dublin and the Wicklow Mountains. Although Wittgenstein spent some time out of the country, Ireland was effectively his base for three very productive years during which he worked on what would become one of his key books, the posthumously published Philosophical Investigations. Wittgenstein in Ireland represents the first sustained account (...) of Wittgenstein's time in Ireland, placing it in its historical context. Wall pays a good deal of attention to the representation of the Irish landscape in which the Austrian philosopher found himself able to work; a large part of his writings were produced in the bleak landscapes of Ireland and Norway. (shrink)

Methods available for the axiomatization of arbitrary finite-valued logics can be applied to obtain sound and complete intelim rules for all truth-functional connectives of classical logic including the Sheffer stroke and Peirce’s arrow. The restriction to a single conclusion in standard systems of natural deduction requires the introduction of additional rules to make the resulting systems complete; these rules are nevertheless still simple and correspond straightforwardly to the classical absurdity rule. Omitting these rules results in systems for intuitionistic versions of (...) the connectives in question. (shrink)

The paper discusses a neglected condition for justified self-defense, namely, 'The Success Condition [SC].' According to SC, otherwise immoral acts can be justified under the right to self-defense only if they actually achieve the intended defense from the perceived threat. If they don't, they are almost always excused, but not morally justified. I show that SC leads to a troubling puzzle because victims who estimate they cannot prevent the attack against them would be morally required to surrender. I try to (...) solve the puzzle by relying on what I call 'The Honor Solution.' Even if defensive acts fail to protect the victim's body, property, or life, they are successful in protecting her honor, thus they do ultimately meet the success condition. (shrink)

Hypocrites are generally regarded as morally-corrupt, cynical egoists who consciously and deliberately deceive others in order to further their own interests. The purpose of my essay is to present a different view. I argue that hypocrisy typically involves or leads to self-deception and, therefore, that real hypocrites are hard to find. One reason for this merging of hypocrisy into self-deception is that a consistent and conscious deception of society is self-defeating from the point of view of egoistical hypocrites. The best (...) way for them to achieve their ends would be to believe in the deception, thereby not only deceiving others but also themselves. If my thesis is sound, we ought to be more cautious in ascribing hypocrisy to people, and less harsh in our attitude toward hypocrites. (shrink)