This paper develops an account of intersectional feminist theory by critically examining the notion of identity implicitly assumed in major critiques of intersectionality. Critics take intersectionality to fragment women along the lines of identity categories such as race, class, and sexuality. Underlying this interpretation, I argue, is the metaphysical assumption that identity is a fixed entity. This is a misunderstanding of identity that neglects how identity is actually lived. By exploring how Asian American women experience their “Asian” identity in (...) their everyday lives (e.g., the “Asian-as-patriarchal vs. White-as-gender-progressive” stereotype, growing anti-Asian racism amid COVID-19, and Asian-Black feminist solidarities), I demonstrate that Asian identity is not fixed but changing according to how it is related to power. I identify and discuss three characteristic types of the identity-power relationship: manifestation of power-as-oppression through the construction of identity, reproduction of power-as- oppression, and creation of new forms of power, namely resistance and solidarity, through the reconstruction of identity. The lives of multiply-oppressed women (e.g., Asian women) can be understood as the locus at which the identity-power relationship is worked out, that is, the power dynamics of oppression are manifested, reproduced, and resisted through the (re)construction of identity. Building on this analysis and engaging discussions on non-ideal theory in social/political philosophy, I argue that intersectional feminist theory can be best explained as a non-ideal theory in a strong sense: a theory that, by focusing on the lives of the multiply oppressed, presents the intersecting dynamics of oppression as central and theory-guiding. (shrink)

In this paper, we investigate the possibility of translating a fragment of natural deduction system (NDS) for natural language semantics into modern type theory (MTT), originally suggested by Luo (2014). Our main goal will be to examine and translate the basic rules of NDS (namely, meta-rules, structural rules, identity rules, noun rules and rules for intersective and subsective adjectives) to MTT. Additionally, we will also consider some of their general features.

In this paper we present a study of adjectival/adverbial modification using modern type theories, i.e. type theories within the tradition of Martin-Löf. We present an account of various issues concerning adjectival/adverbial modification and argue that MTTs can be used as an adequate language for interpreting NL semantics. MTTs are not only expressive enough to deal with a range of modification phenomena, but are furthermore well-suited to perform reasoning tasks that can be easily implemented given their proof-theoretic nature. In (...) MTT-semantics, common nouns are interpreted as types rather than predicates. Therefore, in order to capture the semantics of adjectives adequately, one needs to meet the challenge of modeling CNs modified by adjectives as types. To explicate that this can be done successfully, we first look at the mainstream classification of adjectives, i.e. intersective, subsective and non-subsective adjectives. There, we show that the rich type structure available in MTTs, along with a suitable subtyping framework, offers an adequate mechanism to model these cases. In particular, this modelling naturally takes care of the characterising inferences associated with each class of adjectives. Then, more advanced issues on adjectival modification are discussed: degree adjectives, comparatives and multidimensional adjectives. There, it is shown that the use of indexed types can be usefully applied in order to deal with these cases. In the same vein, the issue of adverbial modification is discussed. We study two general typings for sentence and VP adverbs respectively. It is shown that the rich type structure in MTTs further provides useful organisational mechanisms in giving formal semantics for adverbs. In particular, we discuss the use of \-types to capture the veridicality/non-veridicality distinction and further discuss cases of intensional adverbs using the type theoretic notion of context. We also look at manner, subject and speech act adverbials and propose solutions using MTTs. Finally, we show that the current proof technology can help mechanically check the associated inferences. A number of our proposals concerning adjectival and adverbial modification have been formalised in the proof assistant Coq and many of the associated inference patterns are checked to be correctly captured. (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.

In this paper, we shall present a generalization of phrase structure grammar, in which all functional categories have type restrictions, that is, their argument types are specific domains. In ordinary phrase structure grammar, there is just one universal domain of individuals. The grammar does not make a distinction between verbs and adjectives in terms of domains of applicability. Consequently, it fails to distinguish between sentences like every line intersects every line, which is well typed, and every line intersects every (...) point, which is ill typed.Our generalization relates to ordinary phrase structure grammar in the same way as the higherlevel constructive type theory of Martin-Löf relates to the simple type theory of Church . Simple type theory has been used in linguistics and related with phrase structure grammar, especially in the tradition based on the work of Montague .Our definition of the grammar will be more formal than Montague's in the sense that we shall use a formal metalanguage, that of constructive type theory, for defining both the object language and its interpretation. The grammar, both syntax and semantics, is thus readily implementable in the type-theoretical proof system ALF . Inside type theory, a distinction can be made between the object language and the model, in other words, between syntactic and semantic types. It will turn out that the object language cannot be defined independently of the model, as in ordinary Tarski semantics. This is a direct consequence of introducing the typing restrictions.The grammar presented here can be seen as a formal linguistic elaboration of the work presented in Ranta 1991 and 1994. The organization of generative grammar as categorial grammar followed by sugaring should now look more familiar to the linguist, as the grammatical formalism on which sugaring operates is no longer full type theory but a set of phrase structure trees. (shrink)

At the intersection of taxonomy and nomenclature lies the scientific practice of typification. This practice occurs in biology with the use of holotypes (type specimens), in geology with the use of stratotypes, and in metrology with the use of measurement prototypes. In this paper I develop the first general definition of a scientific type and outline a new philosophical theory of types inspired by Pierre Duhem. I use this general framework to resolve the necessity-contingency debate about (...) type specimens in philosophy of biology, to advance the debate over the myth of the absolute accuracy of standards in metrology, and to address the definition-correlation debate in geology. I conclude that just as there has been a productive synergy between philosophical accounts of natural kinds and scientific taxonomic practices, so too there is much to be gained from developing a deeper understanding of the practices and philosophy of scientific types. (shrink)

Ethical challenges that arise within healthcare delivery institutions are currently categorized as either clinical or organizational, based on the type of issue. Despite this common binary issue-based methodology, empirical study and increasing academic dialogue indicate that a clear line cannot easily be drawn between organizational and clinical ethics. Disagreement around end-of-life treatments, for example, often spawn value differences amongst parties at both organizational and clinical levels and requires a resolution to address both the case at hand and large-scale underlying (...) system-level confounders. I refer to issues that contain elements of both clinical and organizational issues as hybrids and propose a new taxonomy to characterize hybrid cases. I contend that salient contextual features of an ethical issue, such as where it is identified, who it impacts and where it is ideally resolved in relation to its scope of impact, should inform procedure. Implementation of a Hybrid taxonomy viewing ethical issues as existing on a continuum furthers that end. The primary goals are to 1) systematize thinking about ethical issues that arise within healthcare delivery institutions and 2) allow the content of the ethical challenge to drive the process, rather than continuing to rely on the traditional binary issue-based choice. Failure to capture the complexity of hybrid situations perpetuates incomplete information and ultimately an inchoate resolution that creates more questions than answers. (shrink)

Body part terms (BPTs) are used extensively in Mesoamerican languages to name object parts. The process through which BPTs might be extended to refer to a part of an object and further serve as a relator in describing the relation between objects in space has often been attributed to metaphorical processes. This study proposes an alternative analysis following a Structure–Mapping Theory approach (Gentner, 1983, inter alia), based on data from Diidxazá (Isthmus Zapotec, Otomanguean) obtained through elicitation and experimental tasks. (...) The data show that structure mapping does not depend on a 1:1 match of attributes; frequency of use shed light on principles that constrain the semantic extension of most BPTs; a core set of six BPTs are extended by abstraction of the set of intersecting axes of the body. The detailed nature of this study enables an analysis of the mental representations underlying the semantic extension of BPTs. This in turn elucidates on aspects of the relation between spatial language and spatial cognition. In addition, this study allows us to address questions about the categorial status of BPTs in Diidxazá and their lexicographic representation. (shrink)

Higher-order logic, with its type-theoretic apparatus known as the simple theory of types (STT), has increasingly come to be employed in theorizing about properties, relations, and states of affairs—or ‘intensional entities’ for short. This paper argues against this employment of STT and offers an alternative: ordinal type theory (OTT). Very roughly, STT and OTT can be regarded as complementary simplifications of the ‘ramified theory of types’ outlined in the Introduction to Principia Mathematica (on a realist (...) reading). While STT, understood as a theory of intensional entities, retains the Fregean division of properties and relations into a multiplicity of categories according to their adicities and ‘input types’ and discards the division of intensional entities into different ‘orders’, OTT takes the opposite approach: it retains the hierarchy of orders (though with some modifications) and discards the categorisation of properties and relations according to their adicities and input types. In contrast to STT, this latter approach avoids intensional counterparts of the Epimenides and related paradoxes. Fundamental intensional entities lie at the base of the proposed hierarchy and are also given a prominent part to play in the individuation of non-fundamental intensional entities. (shrink)

Recent debates in metaphysics have highlighted the significance of type theories, such as Simple Type Theory (STT), for our philosophical analysis. In this chapter, I present the salient features of a constructive type theory in the style of Martin-Löf, termed CTT. My principal aim is to convey the flavour of this rich, flexible and sophisticated theory and compare it with STT. I especially focus on the forms of quantification which are available in CTT. A (...) further aim is to argue that a comparison between a plurality of theories is beneficial to the philosophical analysis. We may, for example, discover helpful features of one theory that we may want to import into another context, thus enriching our repertoire of formal tools. Or, through comparison with a less well-known theory, we may gain a better understanding of the characteristics of the theories we are familiar with. As argued in this chapter, CTT has much to offer in all of these respects. (shrink)

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 postsecular turn within feminist theory refers to a renewed attention to religion within feminist scholarship. However, rather than conceptualizing the postsecular as a new moment within feminist theorizing that breaks with a previous trend of secular feminism, this article stresses that it is important to recognize the long history of coexistence and contestations between religious and secular feminist approaches. In this article, the different reception histories of the story of Sojourner Truth are examined to elucidate and reflect on (...) the complicated relationship of the religious and the secular within feminist scholarship. Three different types of feminist theoretical engagement with the story of Sojourner Truth are examined and contrasted: the implicitly secular use of the story of Sojourner Truth in black feminist scholarship and theorizing of intersectionality, the explicitly religious interpretations found in the work of feminist and womanist theologians, and the deconstructive reading by Donna Haraway. In discussing and comparing these different engagements with the story of Sojourner Truth, it is stressed that the boundaries between the religious and the secular are perhaps less clear-cut than initially imagined, and that a dialogue between secular and religious feminist approaches is very fruitful. The article closes by examining how the complex intersections of gender, religion and race in the story of Sojourner Truth can be connected to the contemporary theorizing on the racialization of religion within critical race scholarship. (shrink)

This volume presents a Type Theory of Law (TTL), claiming that this is a unique theory of law that stems from the philosophical understanding of Jung's psychological types applied to the phenomenon of law. Furthermore, the TTL claims to be a universal, general and descriptive account of law. To prove that, the book first presents the fundamentals of Jungian psychological types, as they had been invented by Jung and consequently developed further by his followers. The next part (...) of the book describes how the typological structure of an individual determines their understanding of law. It then addresses the way in which inclusive legal theory can be understood based on this typology. Finally, the book describes the TTL in general and descriptive terms and puts it into context. All in all, the book shows how the integral or inclusive approach to understanding the nature of law is not only in tune with our time, but also relevant for presenting a more persuasive picture of law than the older exclusivist or dualist approaches of strict natural law and rigid legal positivism did. (shrink)

We address three fundamental questions: What does it mean for an entity to be living? What is the role of inter-organismic collaboration in evolution? What is a biological individual? Our central argument is that life arises when lineage-forming entities collaborate in metabolism. By conceiving of metabolism as a collaborative process performed by functional wholes, which are associations of a variety of lineage-forming entities, we avoid the standard tension between reproduction and metabolism in discussions of life – a tension particularly evident (...) in discussions of whether viruses are alive. Our perspective assumes no sharp distinction between life and non-life, and does not equate life exclusively with cellular or organismal status. We reach this conclusion through an analysis of the capabilities of a spectrum of biological entities, in which we include the pivotal case of viruses as well as prions, plasmids, organelles, intracellular and extracellular symbionts, unicellular and multicellular life-forms. The usual criterion for classifying many of the entities of our continuum as non-living is autonomy. This emphasis on autonomy is problematic, however, because even paradigmatic biological individuals, such as large animals, are dependent on symbiotic associations with many other organisms. These composite individuals constitute the metabolic wholes on which selection acts. Finally, our account treats cooperation and competition not as polar opposites but as points on a continuum of collaboration. We suggest that competitive relations are a transitional state, with multi-lineage metabolic wholes eventually outcompeting selfish competitors, and that this process sometimes leads to the emergence of new types or levels of wholes. Our view of life as a continuum of variably structured collaborative systems leaves open the possibility that a variety of forms of organized matter – from chemical systems to ecosystems – might be usefully understood as living entities. (shrink)

This paper discusses the relation between the minimal positive relevant logic B and intersection and union type theories. There is a marvelous coincidence between these very differently motivated research areas. First, we show a perfect fit between the Intersection Type Discipline ITD and the tweaking BT of B, which saves implication and conjunction but drops disjunction . The filter models of the -calculus (and its intimate partner Combinatory Logic CL) of the first author and her coauthors (...) then become theory models of these calculi. (The logician's "theory" is the algebraist's "filter".) The coincidence extends to a dual interpretation of key particles—the subtype translates to provable , type intersection to conjunction , function space to implication, and whole domain to the (trivially added but trivial) truth T. This satisfying ointment contains a fly. For it is right, proper, and to be expected that type union should correspond to the logical disjunction of B. But the simulation of functional application by a fusion (or modus ponens product) operation on theories leaves the key Bubbling lemma of work on ITD unprovable for the -prime theories now appropriate for the modeling. The focus of the present paper lies in an appeal to Harrop theories which are (a) prime and (b) closed under fusion. A version of the Bubbling lemma is then proved for Harrop theories, which accordingly furnish a model of and CL. (shrink)

This chapter contains sections titled: Introduction: Major Problems with Trait Ascriptions The Logic of Intellectual Trait Ascription and the Generality Problem The Logic of Moral Trait Ascription and the Global Trait Problem The Common Structure of the Two Problems Acknowledgments References.

The intersection between virtue and care ethics is underexplored in contemporary moral philosophy. This thesis approaches care ethics from a neo-Aristotelian virtue ethical perspective, comparing the two frameworks and drawing on recent work on care to develop a theory thereof. It is split into seven substantive chapters serving three major argumentative purposes, namely the establishment of significant intertheoretical agreement, the compilation and analysis of extant and new distinctions between the two theories, and the synthesis of care ethical insights (...) with neo-Aristotelianism to generate a virtue ethical theory of care. In the first two chapters, I outline virtue ethics and care ethics, and argue for considerable agreement over central premises. Chapter 2 summarises the foundational commitments of care ethics, focusing particularly on their relational ontology and its links to the other ethical claims care ethicists universally ascribe to, namely particularism, partialism, the moral salience of emotions, and the rejection of hard public/private distinctions. Chapter 3 lays out the central concepts in neo-Aristotelian virtue ethics, including eudaimonism, virtue, and character traits, and drawing a number of comparisons between virtue and care ethics specifically with regard to relational ontology and the meta-ethical commitments it underpins. In addition to doing the necessary expository work for the remainder of the thesis, Chapters 2 and 3 also argue that care ethics and virtue ethics have much more in common than is typically acknowledged – the first major contribution of this thesis to the literature. Chapters 2 and 3 to provide at least a prima facie justification for pursuit of the questions I confront in the remainder of the thesis. In Chapter 4, I ask what differentiates these two ethical theories. I survey some of the differences which philosophers in either camp have identified and offer some of my own. I suggest that several of those differences either rest on misunderstandings of one ethic or the other, or that in erecting a divide between virtue and care ethics they also disunify ethics of care. I do, however, identify two differences which seem defensible. Specifically, they are that virtue ethics seems to lack an account of care, which I define minimally as a response or responsiveness to need, and that virtue and care ethics organise their meta-ethical and normative concepts differently. This chapter thus presents a second contribution to the literature: a study of the differences between virtue ethics and care ethics. It also serves to set the trajectory for the remaining chapters, where I respond to the claim that virtue ethics lack an account of care. I spend the remainder of the thesis constructing what I take to be a satisfying foundation for a virtue ethical theory of care. In Chapter 5, I offer three initially viable means of incorporating care into virtue ethics, all of which treat care as a virtue. These are the analogical approach, according to which care is analogous to an existing virtue; the additive approach, according to which care is a novel virtue; and the bundling approach, according to which care is a bundle of virtues. I also offer and evaluate reasons to reject the claim that care is a virtue, concluding that the claim is indeed a viable one so long as the concept of care is sufficiently thick, and I contend that analogical approaches, and particularly analogies with charity, outperform the others. Chapter 5 therefore serves two ends. First, it proffers a novel meta-analysis of concepts of care as a virtue, and thus makes a third contribution to the literature. In doing so, it makes an inroad into the second: the development of a neo-Aristotelian theory of care. Chapter 6 continues this project. I attempt to show how care can be construed as an act-type and a practice. I argue in this chapter that practices are a subcategory of actions, and that care qualifies as an Anscombean act-type which aims at the meeting of needs relating to the care-recipient’s flourishing. I go on to consider the implications of this account for ethics which deploy care as a moral concept, maintaining that it not only offers a better account of consequences than theories of care which include success criteria, but also that it affords us interesting insights into the distinction between ‘caring about’ and ‘caring for’ which allow us to make sense of certain tenets of neo-Aristotelianism. This represents a contribution to both discourses, since neither care nor virtue ethicists working at the intersection of their respective normative theories have delved very deeply into the philosophy of action. Chapter 7 discusses caring relations, suggesting that a virtue ethical theory of caring relations can lean on the work care ethicists have done, and adding some necessary refinements, such as a distinction between ideal and non-ideal caring relations, and a theory of caring relations as reasons for action. This final chapter also draws these three concepts of care together by arguing that virtuous caregivers who are invested in the flourishing of those for whom they care are also sensitive to the relations those care-recipients bear to their institutional environment. I argue that because they are caring participants in caring relations, virtuous agents are characteristically motivated by states of need and dependency to engage in certain sorts of conventionally political practices. In other words, the virtue or virtues of caring characteristically manifest in certain sorts of political or social practices, relating specifically to those areas of moral life. This allows us to build upon recent work in feminist virtue ethics of the sort offered by Tessman and Friedman. I also offer a novel analysis of migration, suggesting that the account of care presenting here is analytically useful both when it comes to historical cases of migration such as the underground railroads and escapes from Nazi-occupied Europe, but also for contemporary issues such as the migrations occurring in the Southern United States and in much of Europe. I thus conclude not only that virtue ethicists ought to incorporate care into their normative framework, and that the theory of care presented here is a coherent one, but that this leads us naturally into applied topics such as virtue politics. I conclude the thesis by considering some its implications and by identifying some further avenues for research. (shrink)

Selection type theories solve adaptation problems. Natural selection, clonal selection for antibody production, and selective theories of higher brain function are examples. An abstract characterization of typical selection processes is generated by analyzing and extending previous work on the nature of natural selection. Once constructed, this abstraction provides a useful tool for analyzing the nature of other selection theories and may be of use in new instances of theory construction. This suggests the potential fruitfulness of research to find (...) other theory types and construct their abstractions. (shrink)

Standard Type Theory, STT, tells us that b^n(a^m) is well-formed iff n=m+1. However, Linnebo and Rayo have advocated the use of Cumulative Type Theory, CTT, has more relaxed type-restrictions: according to CTT, b^β(a^α) is well-formed iff β > α. In this paper, we set ourselves against CTT. We begin our case by arguing against Linnebo and Rayo’s claim that CTT sheds new philosophical light on set theory. We then argue that, while CTT ’s (...) class='Hi'>type-restrictions are unjustifiable, the type-restrictions imposed by STT are justified by a Fregean semantics. What is more, this Fregean semantics provides us with a principled way to resist Linnebo and Rayo’s Semantic Argument for CTT. We end by examining an alternative approach to cumulative types due to Florio and Jones; we argue that their theory is best seen as a misleadingly formulated version of STT. (shrink)

The theory I present and defend in this paper—what I term the art type theory— holds that something is a work of art iff it belongs to an established art type. Something is an established art type, in turn, either because its paradigmatic instances standardly satisfy eight art-making conditions, or because the art world has seen fit to enfranchise it as such. It follows that the art status of certain objects is independent of what any (...) individual or culture might say about it, while the art status of others fundamentally depends on the judgment of the art world. Because of the theory's quasi-institutional component, I conclude by defending it against four objections that have been raised against institutional definitions. (shrink)

We study the intersection type assignment system as defined by Barendregt, Coppo and Dezani. For the four essential variants of the system (with and without a universal type and with and without subtyping) we show that the emptiness (inhabitation) problem is recursively unsolvable. That is, there is no effective algorithm to decide if there is a closed term of a given type. It follows that provability in the logic of "strong conjunction" of Mints and Lopez-Escobar is (...) also undecidable. (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)

This E-Special issue brings together a range of articles from the Theory, Culture, & Society archive that directly explore the relations between fiction and social theory. Each article develops a different perspective on these relations, yet they all share a common interest in probing at the different ways in which fiction might enrich and provoke our conceptual imaginations. These articles ask how theory might be used to understand or illuminate fiction, whilst also considering how theory might (...) be extended, challenged or informed by fictional resources. In general terms, the articles take three types of overlapping approach. First, there are those that use fiction to extend the imagination of social theory. Second are the articles that use fiction as a documentary resource and platform for theorizing. And, finally, there are those articles that use theory to reanimate and re-examine fictional forms. In exploring these three intersecting branches the pieces illustrate the different ways in which fiction and social theory might interweave in our thinking. The articles gathered here provide frameworks, ideas and resources through which the reader might continue to think imaginatively and creatively about the social world. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:HINDUISM AND MIMETIC THEORY: A RESPONSE Julia W. Shinnick Austin, Texas i: Introduction "would like to thankProfessor Clooney for his thorough presentation.ofthe enormously complex and layeredtreatment ofviolence within Hindu religious traditions. In his paper I found many aspects of Hinduism that directly engage the mimetic theory, and I hope that I can articulate some of these in such a way as to initiate discussion during the next (...) hour or so this afternoon. As one of the so-called "Girardians," my first impression in response to Professor Clooney's paper is that the complexity of Hindu attitudes toward violence and sacrifice seem to indicate an awareness of the ritualization and control of violence, as developed over a very long period of time. I. Language of Avoidance/Denial: The Horse I would like to start with a small detail, but one which seems to me key to many larger issues in light of the mimetic theory: the ritual directions and prayers [1.1] in which the words "to kill" and "to die" are carefully avoided through the substitutions of such words as "he takes hold of and "he makes consent." I might add here also, that the avoidance ofusing "real" words for what is "really" being doneDkilling the animalDreminds me to some extent of the use of language by contemporary torturers as analyzed in the book The Body in Pain: The Making and Unmaking ofthe World by Elaine Scarry. Scarry argues that the language used by torturers avoids any acknowledg- Julia W. Shinnick141 ment of the real actions they are committing, as well as any acknowledgment of the very real pain they are causing their victims; furthermore, it is a dehumanizing language, referring to the victims as, for example, submarines, in one particular type of torture. This discrepancy between language and actual action is intriguing in both cases. Granted, the sacrificers in the Rg Veda do not deny that they are sacrificing the horse, and the "apology" (the words to the horseD"Do not let the axe linger in yourbody...") is not part ofan act oftorture, but the words have in common with Scarry's report a certain denial or avoidance of the reality of both the actions ofkilling and/orharming and the result ofthese actions, pain and/or death. Furthermore, the avoidance of the words "to kill" and "to die" would fit in with the mimetic theory's idea ofprohibiting the ritual from bringing actual facts of the founding murder to consciousness. II.Sacrificial Instructions The words addressed to the horse in the Rg Veda [I.l]and the instructions for the treatment of animals to be sacrificedO'The axe penetrates the thirty-four ribs of the swift horse...so that the limbs may be unperforated, and recapitulating, joint by joint "Dseem to me to intersect with the mimetic theory in terms of ritual sacrifice as a reenactment of the founding conflict. As I understand it, in the mimetic theory, one reason for careful, detailed ritual instructions and the sense ofgreatdangerin sacrifice (the sense that if the ritual is not carried out exactly and correctly, something horrible might happen) has to do with a non-conscious fear of unleashing the mimetic crisis all over again. I see aspects of this in the minutely detailed instructions to the priest such as the importance of leading the horse but not holding on to it, and the desire to pacify the animal to be sacrificed. These kinds of details are of course also present in other sacrifice rituals. For example, in Perpetua's Passion: The Death and Memory of a Young Roman Woman, Joyce Salisbury speaks of the simultaneous sacrifice of hundreds of children in ancient Carthage during the Punic Wars. The children had to be (appear) "willing" to be sacrificed. Ifthey cried out, the sacrifice was considered invalid. The parents also had to be (appear) "willing;" ifthe mother shed a tear, the sacrifice was invalid. Thus, immediately before the fatal knife thrust, the sacrificing parents would caress their children and tickle them to make them laugh. III.Violence and Kings According to James Williams in his introduction to chapter 6 of The 142Hinduism and Mimetic Theory: A Response Girard Reader, one of... (shrink)

We introduce a predicative version of topos based on the notion of small maps in algebraic set theory, developed by Joyal and one of the authors. Examples of stratified pseudotoposes can be constructed in Martin-Löf type theory, which is a predicative theory. A stratified pseudotopos admits construction of the internal category of sheaves, which is again a stratified pseudotopos. We also show how to build models of Aczel-Myhill constructive set theory using this categorical structure.

I argue that there is an affective injustice in gendered and racialized oppression. To account for this, we must deny the opposition of affect and intentionality often assumed in the philosophy of emotion and the affective turn: while affect and intentionality are not opposed in principle, affective intentionality may be refused uptake in oppressive practices. In section 1, I read Merleau‐Ponty’s theory of the body schema as a theory of affect that accommodates my account of affective injustice and (...) aligns with accounts of affect transmission and circulation in feminist philosophies of the affective turn. This is crucial for understanding Fanon’s contribution to the theory of the body schema, in which it is susceptible to historical‐racial “affective disorders.” In sections 2–4, I distinguish three types of affective injustice: affective marginalization, exploitation, and violence. In section 2 I develop an intersectional feminist account of this distinction drawing on Lorde and Lugones and raise questions about the limits of framing the issue of affective injustice in terms of intentionality as opposed to a more psychoanalytic conceptual vocabulary that accommodates the displacement of affective force. In sections 3 and 4, I explore these affective injustices through an analysis of Fanonian concepts, showing how the theory of the body schema can accommodate not only affective intentionality but also the oppressive disjunction of affect and intentionality, as well as forms of affective injustice that exceed the oppressive disabling of sense‐making and involve the exploitative and violent displacement of affective force. (shrink)

Many philosophers believe in things, propositions, which are the things that we believe, assert etc., and which are the contents of sentences. The act-type theory of propositions is an attempt to say what propositions are, to explain how we stand in relations to them, and to explain why they are true or false. The core idea of the act-type theory is that propositions are types of acts of predication. The theory is developed in various ways (...) to offer explanations of the important properties of propositions. I present the core idea of the theory, and some developments of it. I discuss the relationship between the theory and the content–force distinction. I also present an important type of objection that has been raised to the explanations offered by the act-type theory. (shrink)

The first system of intersection types, Coppo and Dezani [3], extended simple types to include intersections and added intersection introduction and elimination rules (( $\wedge$ I) and ( $\wedge$ E)) to the type assignment system. The major advantage of these new types was that they were invariant under β-equality, later work by Barendregt, Coppo and Dezani [1], extended this to include an (η) rule which gave types invariant under βη-reduction. Urzyczyn proved in [6] that for both these (...) systems it is undecidable whether a given intersection type is empty. Kurata and Takahashi however have shown in [5] that this emptiness problem is decidable for the sytem including (η), but without ( $\wedge$ I). The aim of this paper is to classify intersection type systems lacking some of ( $\wedge$ I), ( $\wedge$ E) and (η), into equivalence classes according to their strength in typing λ-terms and also according to their strength in possessing inhabitants. This classification is used in a later paper to extend the above (un)decidability results to two of the five inhabitation-equivalence classes. This later paper also shows that the systems in two more of these classes have decidable inhabitation problems and develops algorithms to find such inhabitants. (shrink)

Homotopy Type Theory is a proposed new language and foundation for mathematics, combining algebraic topology with logic. An important rule for the treatment of identity in HoTT is path induction, which is commonly explained by appeal to the homotopy interpretation of the theory's types, tokens, and identities as spaces, points, and paths. However, if HoTT is to be an autonomous foundation then such an interpretation cannot play a fundamental role. In this paper we give a derivation of (...) path induction, motivated from pre-mathematical considerations, without recourse to homotopy theory. (shrink)

This paper introduces a multi-modal polymorphic type theory to model epistemic processes characterized by trust, defined as a second-order relation affecting the communication process between sources and a receiver. In this language, a set of senders is expressed by a modal prioritized context, whereas the receiver is formulated in terms of a contextually derived modal judgement. Introduction and elimination rules for modalities are based on the polymorphism of terms in the language. This leads to a multi-modal non-homogeneous version (...) of a type theory, in which we show the embedding of the modal operators into standard group knowledge operators. (shrink)

This book develops an intersectional feminist approach to moral responsibility. It accomplisheses four main goals. First, it outlines a concise list of the main principles of intersectional feminism. Second, it uses these principles to critique prevailing philosophical theories of moral responsibility. Third, it offers an account of moral responsibility that is compatible with the ethos of intersectional feminism. And fourth, it uses intersectional feminist principles to critique culturally normative responsibility practices. -/- This is the first book to provide an explicitly (...) intersectional feminist approach to moral responsibility. After identifying the five principles central to intersectional feminism, the author demonstrates how influential theories of responsibility are incompatible with these principles. She argues that a normatively adequate theory of blame should not be preoccupied with the agency or traits of wrongdoers; it should instead underscore, and seek to ameliorate, oppression and adversity as experienced by the marginalized. Apt blame and praise, according to her intersectional feminist account, is both communicative and functionalist. The book concludes with an extensive discussion of culturally embedded responsibility practices, including asymmetrically structured conversations and gender- and racially biased social spaces. -/- An Intersectional Feminist Approach to Moral Responsibility presents a sophisticated and original philosophical account of moral responsibility. It will be of interest to philosophers working at the crossroads of moral responsibility, feminist philosophy, critical race theory, queer theory, critical disability studies, and intersectionality theory. (shrink)

Neil Tennant’s core logic is a type of bilateralist natural deduction system based on proofs and refutations. We present a proof system for propositional core logic, explain its connections to bilateralism, and explore the possibility of using it as a type theory, in the same kind of way intuitionistic logic is often used as a type theory. Our proof system is not Tennant’s own, but it is very closely related, and determines the same consequence relation. (...) The difference, however, matters for our purposes, and we discuss this. We then turn to the question of strong normalization, showing that although Tennant’s proof system for core logic is not strongly normalizing, our modified system is. (shrink)

I explore the possibility of a structuralist interpretation of homotopy type theory (HoTT) as a foundation for mathematics. There are two main aspects to HoTT's structuralist credentials. First, it builds on categorical set theory (CST), of which the best-known variant is Lawvere's ETCS. I argue that CST has merit as a structuralist foundation, in that it ascribes only structural properties to typical mathematical objects. However, I also argue that this success depends on the adoption of a strict (...) typing system which undermines the metaphysical seriousness of this structuralism. Homotopy type theory adds to CST a distinctive theory of identity between sets, which arguably allows its objects to be seen as ante rem structures. I examine the prospects for such a view, and address many other interpretive problems as they arise. (shrink)

Contextual type theories are largely explored in their applications to programming languages, but less investigated for knowledge representation purposes. The combination of a constructive language with a modal extension of contexts appears crucial to explore the attractive idea of a type-theoretical calculus of provability from refutable assumptions for non-monotonic reasoning. This paper introduces such a language: the modal operators are meant to internalize two different modes of correctness, respectively with necessity as the standard notion of constructive verification and (...) possibility as provability up to refutation of contextual conditions. (shrink)

In this paper I propose a fundamental modification of standard type theory, produce a new kind of type theoretic language, and couch in this language a comprehensive theory of abstract individuals and abstract properties and relations of every type. I then suggest how to employ the theory to solve the four following philosophical problems: the identification and ontological status of Frege's Senses; the deviant behavior of terms in propositional attitude contexts; the non-identity of necessarily (...) equivalent propositions, and the paradox of analysis. We can roughly describe these solutions as follows: the senses of English names and descriptions which denote individuals will be modelled as abstract individuals; the senses of English relation denoting expressions of a given type will be modelled as abstract relations of that type. Inside de dicto attitude contexts, these English expressions denote their senses. Relations and propositions will not be identified with their extensions, nor with functions or sets of any kind. They will be taken as primitive, and precise being and identity conditions will be proposed consistent with the view that necessarily equivalent relations and propositions may be distinct. With the modelling described in, the expressions being a brother and being a male sibling may both denote the same property, though their senses may differ. Just as Frege predicts, being a brother just is being a male sibling is an informative identity statement because the terms flanking the identity sign have the same denotation, though distinct senses. (shrink)

Este artigo canta uma canção — uma canção criada ao unir o trabalho de quatro grandes nomes na história da lógica: Hans Reichenbach, Arthur Prior, Richard Montague, e Leon Henkin. Embora a obra dos primeiros três desses autores tenha sido previamente combinada, acrescentar as ideias de Leon Henkin é o acréscimo requerido para fazer com que essa combinação funcione no nível lógico. Mas o presente trabalho não se concentra nas tecnicalidades subjacentes (que podem ser encontradas em Areces, Blackburn, Huertas, e (...) Manzano [no prelo]), e sim nos instrumentos subjacentes e no modo como trabalham em conjunto. Esperamos que o leitor fique tentado a cantar junto. DOI:10.5007/1808-1711.2011v15n2p225. (shrink)

Prolegomena It is fitting to begin this book on intuitionistic type theory by putting the subject matter into perspective. The purpose of this chapter is to ...

The Univalence axiom, due to Vladimir Voevodsky, is often taken to be one of the most important discoveries arising from the Homotopy Type Theory research programme. It is said by Steve Awodey that Univalence embodies mathematical structuralism, and that Univalence may be regarded as ‘expanding the notion of identity to that of equivalence’. This article explores the conceptual, foundational and philosophical status of Univalence in Homotopy Type Theory. It extends our Types-as-Concepts interpretation of HoTT to Universes, (...) and offers an account of the Univalence axiom in such terms. We consider Awodey’s informal argument that Univalence is motivated by the principle that reasoning should be invariant under isomorphism, and we examine whether an autonomous and rigorous justification along these lines can be given. We consider two problems facing such a justification. First, there is a difference between equivalence and isomorphism and Univalence must be formulated in terms of the former. Second, the argument as presented cannot establish Univalence itself but only a weaker version of it, and must be supplemented by an additional principle. The article argues that the prospects for an autonomous justification of Univalence are promising. (shrink)

Philosophy Compass, Volume 17, Issue 2, February 2022.

In the formal semantics based on modern type theories, common nouns are interpreted as types, rather than as predicates of entities as in Montague’s semantics. This brings about important advantages in linguistic interpretations but also leads to a limitation of expressive power because there are fewer operations on types as compared with those on predicates. The theory of coercive subtyping adequately extends the modern type theories and, as shown in this paper, plays a very useful role in (...) making type theories more expressive for formal semantics. It not only gives a satisfactory solution to the basic problem of ‘multiple categorisation’ caused by interpreting common nouns as types, but provides a powerful formal framework to model interesting linguistic phenomena such as copredication, whose formal treatment has been found difficult in a Montagovian setting. In particular, we show how to formally introduce dot-types in a type theory with coercive subtyping and study some type-theoretic constructs that provide useful representational tools for reference transfers and multiple word meanings in formal lexical semantics. (shrink)

A version of intuitionistic type theory is presented here in which all logical symbols are defined in terms of equality. This language is used to construct the so-called free topos with natural number object. It is argued that the free topos may be regarded as the universe of mathematics from an intuitionist's point of view.

The article deals with an approach to the analysis of propositional attitudes based on the type-theoretical semantics proposed by A. Ranta and originating from the type theory of P. Martin-Löf. Type-theoretical semantics contains the notion of context and tools of extracting information from it in an explicit form. This allows us to correctly formalize the dependence on contexts typical of propositional attitudes. In the article the context is presented as a dependent sum type (Record (...) class='Hi'>type in the proof assistant Coq). Ranta’s approach is refined and applied to the analysis of Quine’s phrase “Ralph believes that someone is a spy”. Three variants of formalization for this phrase are described which differ in the content of contextual knowledge and the way the truth values of the phrase are derived. Contexts are connected through the function of conversion, making it possible to relate truth values. As a result, it is shown that the instruments for working with contexts provided by type-theoretical semantics allow us to avoid the problem of opacity described by Quine. Provided formalization along with proofs is coded in Coq and made freely available. (shrink)

In light of the close connection between the ontological hierarchy of set theory and the ideological hierarchy of type theory, Øystein Linnebo and Agustín Rayo have recently offered an argument in favour of the view that the set-theoretic universe is open-ended. In this paper, we argue that, since the connection between the two hierarchies is indeed tight, any philosophical conclusions cut both ways. One should either hold that both the ontological hierarchy and the ideological hierarchy are open-ended, (...) or that neither is. If there is reason to accept the view that the set-theoretic universe is open-ended, that will be because such a view is the most compelling one to adopt on the purely ontological front. (shrink)

Mathematicians often consider Zermelo-Fraenkel Set Theory with Choice (ZFC) as the only foundation of Mathematics, and frequently don’t actually want to think much about foundations. We argue here that modern Type Theory, i.e. Homotopy Type Theory (HoTT), is a preferable and should be considered as an alternative.