The recent discovery of an interpretation of constructive type theory into abstract homotopy theory suggests a new approach to the foundations of mathematics with intrinsic geometric content and a computational implementation. Voevodsky has proposed such a program, including a new axiom with both geometric and logical significance: the Univalence Axiom. It captures the familiar aspect of informal mathematical practice according to which one can identify isomorphic objects. While it is incompatible with conventional foundations, it is a powerful addition to homotopy (...) type theory. It also gives the new system of foundations a distinctly structural character. (shrink)

A comprehensive reference to category theory for students and researchers in mathematics, computer science, logic, cognitive science, linguistics, and philosophy. Useful for self-study and as a course text, the book includes all basic definitions and theorems, as well as numerous examples and exercises.

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)

Despite Kant's belief in a universal causal determinism among phenomena and his rejection of any noumenal agency in brutes, he nevertheless rejected Descartes's hypothesis that brutes are machines. Explaining Kant's response to Descartes forms the basis for this discussion of the nature of consciousness and matter in Kant's system. Kant's numerous remarks on animal psychology-as found in his lecture notes and reflections on metaphysics and anthropology-suggest a theory of consciousness and self-consciousness at odds with that traditionally ascribed to him.

Moral judgments about an agent's behavior are enmeshed with inferences about the agent's mind. Folk psychology—the system that enables such inferences—therefore lies at the heart of moral judgment. We examine three related folk-psychological concepts that together shape people's judgments of blame: intentionality, choice, and free will. We discuss people's understanding and use of these concepts, address recent findings that challenge the autonomous role of these concepts in moral judgment, and conclude that choice is the fundamental concept of the three, defining (...) the core of folk psychology in moral judgment. (shrink)

of type theory has been used successfully to formalize large parts of constructive mathematics, such as the theory of generalized recursive definitions [NPS90, ML79]. Moreover, it is also employed extensively as a framework for the development of high-level programming languages, in virtue of its combination of expressive strength and desirable proof-theoretic properties [NPS90, Str91]. In addition to simple types A, B, . . . and their terms x : A b(x) : B, the theory also has dependent types x : (...) A B(x), which are regarded as indexed families of types. There are simple type forming operations A × B and A → B, as well as operations on dependent types, including in particular the sum x:A B(x) and product x:A B(x) types (see the appendix for details). The Curry-Howard interpretation of the operations A × B and A → B is as propositional conjunction and.. (shrink)

The thesis of this work is that in both modern Japanese philosophy and American pragmatism there has been a paradigm shift from a monological concept of self as an isolated "I" to a dialogical concept of the social self as an "I-Thou relation," including a communication model of self as individual-society interaction. It is also shown for both traditions all aesthetic, moral, and religious values are a function of the social self arising through communicative interaction between the individual and society. (...) However, at the same time this work critically examines major ideological conflicts arising between the social self theories of modern Japanese philosophy and American pragmatism with respect to such problems as individualism versus collectivism, freedom versus determinism, liberalism versus communitarianism, and relativism versus objectivism. (shrink)

In this paper the machinery and results developed in [Awodey et al, 2004] are extended to the study of constructive set theories. Specifically, we introduce two constructive set theories BCST and CST and prove that they are sound and complete with respect to models in categories with certain structure. Specifically, basic categories of classes and categories of classes are axiomatized and shown to provide models of the aforementioned set theories. Finally, models of these theories are constructed in the category of (...) ideals. (shrink)

Extant models of moral judgment assume that an action’s intentionality precedes assignments of blame. Knobe (2003b) challenged this fundamental order and proposed instead that the badness or blameworthiness of an action directs (and thus unduly biases) people’s intentionality judgments. His and other researchers’ studies suggested that blameworthy actions are considered intentional even when the agent lacks skill (e.g., killing somebody with a lucky shot) whereas equivalent neutral actions are not (e.g., luckily hitting a bull’s-eye). The present five studies offer an (...) alternative account of these provocative findings. We suggest that people see the morally significant action examined in previous studies (killing) as accomplished by a basic action (pressing the trigger) for which an unskilled agent still has sufficient skill. Studies 1 through 3 show that when this basic action is performed unskillfully or is absent, people are far less likely to view the killing as intentional, demonstrating that intentionality judgments, even about immoral actions, are guided by skill information. Studies 4 and 5 further show that a neutral action such as hitting the bull’s-eye is more difficult than killing and that difficult actions are less often judged intentional. When difficulty is held constant, people’s intentionality judgments are fully responsive to skill information regardless of moral valence. The present studies thus speak against the hypothesis of a moral evaluation bias in intentionality judgments and instead document people’s sensitivity to subtle features of human action. (shrink)

This is a draft of the introduction to a forthcoming volume that brings together all of J. G. Herder's student notes from Immanuel Kant's lectures. It is intended as a volume in Kant's gesammelte Schriften (de Gruyter). These are the earliest notes (1762-64) we have from Kant's lectures (which span from 1755 to 1796) and the only notes before his professorship began in 1770. Included are improved transcriptions of Herder's notes on metaphysics, moral philosophy, logic, physics, and mathematics, and the (...) first transcription of his notes from Kant’s physical geography lectures. (shrink)

We show how to interpret the language of first-order set theory in an elementary topos endowed with, as extra structure, a directed structural system of inclusions (dssi). As our main result, we obtain a complete axiomatization of the intuitionistic set theory validated by all such interpretations. Since every elementary topos is equivalent to one carrying a dssi, we thus obtain a first-order set theory whose associated categories of sets are exactly the elementary toposes. In addition, we show that the full (...) axiom of Separation is validated whenever the dssi is superdirected. This gives a uniform explanation for the known facts that cocomplete and realizability toposes provide models for Intuitionistic Zermelo—Fraenkel set theory (IZF). (shrink)

As McKinsey and Tarski showed, the Stone representation theorem for Boolean algebras extends to algebras with operators to give topological semantics for propositional modal logic, in which the “necessity” operation is modeled by taking the interior of an arbitrary subset of a topological space. In this article, the topological interpretation is extended in a natural way to arbitrary theories of full first-order logic. The resulting system of S4 first-order modal logic is complete with respect to such topological semantics.

We define the notion of a model of higher-order modal logic in an arbitrary elementary topos E. In contrast to the well-known interpretation of higher-order logic, the type of propositions is not interpreted by the subobject classifier ΩE, but rather by a suitable complete Heyting algebra H. The canonical map relating H and ΩE both serves to interpret equality and provides a modal operator on H in the form of a comonad. Examples of such structures arise from surjective geometric morphisms (...) f : F → E, where H = f∗ΩF. The logic differs from non-modal higher-order logic in that the principles of functional and propositional extensionality are not longer valid but may be replaced by modalized versions. The usual Kripke, neighborhood, and sheaf semantics for propositional and first-order modal logic are subsumed by this notion. (shrink)

In this short note we give a glimpse of homotopy type theory, a new field of mathematics at the intersection of algebraic topology and mathematical logic, and we explain Vladimir Voevodsky’s univalent interpretation of it. This interpretation has given rise to the univalent foundations program, which is the topic of the current special year at the Institute for Advanced Study.

This book represents emerging alternative perspectives to the "constructivist" orthodoxy that currently dominates the field of science and technology studies. Various contributions from distinguished Americans and Europeans in the field, provide arguments and evidence that it is not enough simply to say that science is "socially situated." Controversial Science focuses on important political, ethical, and broadly normative considerations that have yet to be given their due, but which point to a more realistic and critical perspective on science policy.

Artistic Detachment in Japan and the West takes up the notion of artistic detachment, or psychic distance, as an intercultural motif for East-West comparative aesthetics. The work begins with an overview of aesthetic theory in the West from the eighteenth-century empiricists to contemporary aesthetics and concludes with a survey of various critiques of psychic distance. Throughout, the author takes a highly innovative approach by juxtaposing Western aesthetic theory against Eastern aesthetic theory. Weaving between cultures and time periods, the author focuses (...) on a remarkably wide range of theories: in the West, the Kantian notion of disinterested contemplation, Heidegger's Gelassenheit, semiotics, and pragmatism; in Japan, Zeami's notion of riken no ken, the Kyoto School's intepretation of nothingness, D. T. Suzuki's analysis of the function of no-mind, and the writings of Kuki Shuzo on Buddhist detachment. "Portrait of the artist" fiction by such writers as Henry James, James Joyce, Mori Ogai, and Natsume Soseki demonstrates how the main theme of detachment is expressed in literary traditions. The role of sympathy or pragmatism in relation to disinterest is examined, suggesting conflicts within or challenges to the notion of detachment. Researchers and students in Eastern and Western areas of study, including philosophers and religionists, as well as literary and cultural critics, will deem this work an invaluable contribution to cross-cultural philosophy and literary studies. (shrink)

This work is a step toward the development of a logic for types and computation that includes not only the usual spaces of mathematics and constructions, but also spaces from logic and domain theory. Using realizability, we investigate a configuration of three toposes that we regard as describing a notion of relative computability. Attention is focussed on a certain local map of toposes, which we first study axiomatically, and then by deriving a modal calculus as its internal logic. The resulting (...) framework is intended as a setting for the logical and categorical study of relative computability. (shrink)

This paper is the first in a two-part series in which we discuss several notions of completeness for systems of mathematical axioms, with special focus on their interrelations and historical origins in the development of the axiomatic method. We argue that, both from historical and logical points of view, higher-order logic is an appropriate framework for considering such notions, and we consider some open questions in higher-order axiomatics. In addition, we indicate how one can fruitfully extend the usual set-theoretic semantics (...) so as to shed new light on the relevant strengths and limits of higher-order logic. (shrink)

This paper presents completeness and conservative extension results for the boolean extensions of the relevant logic T of Ticket Entailment, and for the contractionless relevant logics TW and RW. Some surprising results are shown for adding the sentential constant t to these boolean relevant logics; specifically, the boolean extensions with t are conservative of the boolean extensions without t, but not of the original logics with t. The special treatment required for the semantic normality of T is also shown along (...) the way. (shrink)

Abbreviations Works by Alfred North Whitehead 1) Adventures of Ideas. New York: Macmillan Co., 1967 AI 2) Concept of Nature. Cambridge: Cambridge University Press, 1971 CN 3) Modes of Thought. New York: Macmillan Co., 1968 MT 4) Process ..

This book introduces the history of third way ideology, surveys its various contrasting forms and locates it within the context of a recurrent crisis of modern European ideologies.

This paper constructs models of intuitionistic set theory in suitable categories. First, a Basic Intuitionistic Set Theory (BIST) is stated, and the categorical semantics are given. Second, we give a notion of an ideal over a category, using which one can build a model of BIST in which a given topos occurs as the sets. And third, a sheaf model is given of a Basic Intuitionistic Class Theory conservatively extending BIST. The paper extends the results in [2] by introducing a (...) new and perhaps more natural notion of ideal, and in the class theory of part three. (shrink)

This paper is a study of four subscripted Gentzen systems G u R +, G u T +, G u RW + and G u TW +. [16] shows that the first three are equivalent to the semilattice relevant logics u R +, u T + and u RW + and conjectures that G u TW + is, equivalent to u TW +. Here we prove Cut Theorems for these systems, and then show that modus ponens is admissible — which (...) is not so trivial as one normally expects. Finally, we give decision procedures for the contractionless systems, G u TW + and G u RW +. (shrink)

Image factorizations in regular categories are stable under pullbacks, so they model a natural modal operator in dependent type theory. This unary type constructor [A] has turned up previously in a syntactic form as a way of erasing computational content, and formalizing a notion of proof irrelevance. Indeed, semantically, the notion of a support is sometimes used as surrogate proposition asserting inhabitation of an indexed family. We give rules for bracket types in dependent type theory and provide complete semantics using (...) regular categories. We show that dependent type theory with the unit type, strong extensional equality types, strong dependent sums, and bracket types is the internal type theory of regular categories, in the same way that the usual dependent type theory with dependent sums and products is the internal type theory of locally Cartesian closed categories. We also show how to interpret first-order logic in type theory with brackets, and we make use of the translation to compare type theory with logic. Specifically, we show that the propositions-as-types interpretation is complete with respect to a certain fragment of intuitionistic first-order logic, in the sense that a formula from the fragment is derivable in intuitionistic first-order logic if, and only if, its interpretation in dependent type theory is inhabited. As a consequence, a modified double-negation translation into type theory (without bracket types) is complete, in the same sense, for all of classical first-order logic. (shrink)

Three different styles of foundations of mathematics are now commonplace: set theory, type theory, and category theory. How do they relate, and how do they differ? What advantages and disadvantages does each one have over the others? We pursue these questions by considering interpretations of each system into the others and examining the preservation and loss of mathematical content thereby. In order to stay focused on the “big picture”, we merely sketch the overall form of each construction, referring to the (...) literature for details. Each of the three steps considered below is based on more recent logical research than the preceding one. The first step from sets to types is essentially the familiar idea of set theoretic semantics for a syntactic system, i.e. giving a model; we take a brief glance at this step from the current point of view, mainly just to fix ideas and notation. The second step from types to categories is known to categorical logicians as the construction of a “syntactic category”; we give some specifics for the benefit of the reader who is not familiar with it. The third step from categories to sets is based on quite recent work, but captures in a precise way an intuition from the early days of foundational studies. With these pieces in place, we can then draw some conclusions regarding the differences between the three schemes, and their relative merits. In particular, it is possible to state more precisely why the methods of category theory are more appropriate to philosophical structuralism. (shrink)

La religión y la violencia parecen ir unidas la una a la otra inevitablemente. La cuestión surge acerca de si la violencia es inherente al islam, y para contestarla, el artículo examina periodos sucesivos de la historia musulmana, desde este punto de vista. La investigación muestra que no existe una relación intrínseca y que el islam contemporáneo tiende mayoritariamente a separar la religión de la violencia.

Abstract:Watsuji Tetsurō's model of human existence (ningen sonzai) and his ethical principle of selfless solicitude (kokorozukai) imply not only a broadly permissive position on reproductive rights but a clearer vision of pregnancy and the fetus, and also a deeper moral critique of the anti-abortion movement.

Comics writer and artist Frank Miller reinvented Batman, bringing greater emotional, moral, and political depth to the character. This chapter considers Batman’s ethics and politics, examining his rejection of utilitarianism, his embrace of the will to power, his Kantian dilemma when dealing with the Joker, and the distinction to be drawn between Miller’s own libertarianism and Bruce Wayne’s Bat-Libertarianism.

Wonder Woman has evolved considerably since the Golden Age. (Thank Hera!) Different writers in different eras have tinkered with her back story and her resulting character. Yet throughout her many retellings people can point to two consistent trends: she is a warrior, and she protects the abused. As a warrior, her honor code isn't so different from bushido, the code of the samurai. She is selfless, fearless, relentless, and she even has a magic lasso to enforce the samurai virtue of (...) honesty. In the hands of her best writers, Wonder Woman is not a generic do‐gooder, nor is she a milquetoast rule follower. Though her moral motivations may shift from one author to the next, what is consistent throughout her many incarnations is that Wonder Woman is uniquely placed to be the samurai feminist, the only one who can reconcile bushido and care ethics. (shrink)

Hard determinism is hardly a new position, but the most common arguments are not widely convincing. Theological arguments rest on the oversight or control of a supernatural entity, and so are not convincing to any who do not share the metaphysical assumptions latent in the argument. Psychological arguments reston putatively scientific claims that, if examined more closely, seem not to be scientific at all. A doxastic argument avoids these pitfalls. According to this doxastic argument, beliefs are not freely chosen, for (...) to believe X is to be convinced of X, and it is not up to the agent to find something convincing or unconvincing. If an agent's allegedly free actions are based on beliefs, and if those beliefs cannot freely be chosen by the agent, then that agent's actions are not ultimately free. (shrink)

Les veloppement de la philosophie d'Averrotre mieux dvisions qu'Averrome de ses ouvrages que par l'ordre traditionnel de ses commentaires ; ces res par Averrotapes initiales sont infiuenctations d'Alexandre d'Aphrodise et par Thtapes finales de son loigne de ces auteurs et se rapproche de la pense par la lecture par Averrobut du Livre VIII de la Physique: ls est d'accord avec Aristote dans la premitape de son parcours et s're, puisqu'il croit par la suite que le dessein d'Aristote dans cette partie (...) du livre ternitleste. En ce qui concerne la lecture diffcution qu'Averroes et d'autres philosophes subirent en 1197. II n'affirme plus que la philosophie est la voie pour parvenir à la perfection humaine mais veut settlement exposer clairement la philosophie d'Aristote. (shrink)

The [lambda]-calculus can be represented topologically by assigning certain spaces to the types and certain continuous maps to the terms. Using a recent result from category theory, the usual calculus of [lambda]-conversion is shown to be deductively complete with respect to such topological semantics. It is also shown to be functionally complete, in the sense that there is always a ‘minimal’ topological model in which every continuous function is [lambda]-definable. These results subsume earlier ones using cartesian closed categories, as well (...) as those employing so-called Henkin and Kripke [lambda]-models. (shrink)