In this paper, I present a two-pronged argument devoted to defending the type-identity theory of mind against the argument presented by Kripke in _Naming and Necessity_. In the first part, the interpersonal case, I show that since it is not possible to establish the metaphysical conditions for phenomenal identity, it is not possible to argue that there can be physical differences between two subjects despite their phenomenal identity. In the second part, the intrapersonal case, I (...) consider the possibility of imagining one and the same individual having the same phenomenal state while counterfactually being in very different physical states. I argue that this case should respect Kripke’s implicit theory of personal identity—but this proves to be a very difficult task to accomplish, thus preventing the argument from getting off the ground. Therefore, I maintain, that the type-identity theory is still the better option to solve the mind–body problem. (shrink)

Functionalists in philosophy of mind traditionally raise two major arguments against the type identity theory: (1) psychological states are _multiply realizable_ so that there are no one-to-one mappings of psychological states onto neural states and (2) the most that evidence could ever establish is the _correlation_ of psychological and neural states, not their identity. We defend a variant on the traditional type identity theory which we call _heuristic identity theory_ (HIT) against both (...) of these objections. Drawing its inspiration from scientific practice, heuristic identity theory construes identity claims as hypotheses that guide subsequent inquiry, not as conclusions of the research. (shrink)

In this essay I shall argue that the crucial assumptions of Kripke's argument, i.e. the collapse of the appearance/reality distinction in the case of phenomenal states and the idea of a qualitatively identical epistemic situation, imply an objective principle of identity for mental-state types. This principle, I shall argue, rather than being at odds with physicalism, is actually compatible with both the type-identity theory of the mind and Kripke's semantics and metaphysics. Finally, I shall sketch a (...) version of the type-identity theory. (shrink)

The type identity theory, according to which types of mental state are identical to types of physical state, fell out of favour for some years but is now being considered with renewed interest. Many philosophers are critically re-examining the arguments which were marshalled against it, finding in the type identity theory both resources to strengthen a comprehensive, physicalistic metaphysics and a useful tool in understanding the relationship between developments in psychology and new results in (...) neuroscience. This volume brings together leading philosophers of mind, whose essays challenge in new ways the standard objections to type identity theory, such as the multiple realizability objection and the modal argument. Other essays show how cognitive science and neuroscience are lending new support to type identity theory and still others provide, extend and improve traditional arguments concerning the theory's explanatory power. (shrink)

It is commonly believed that there is a fundamental incompatibility between multiple realization and type identity in the philosophy of mind. This claim can be challenged, however, since a single neural type may be realized by different microphysical types. In this case, the identity statement would connect the psychological and the neural type, while the neural type, in turn, could be multiply realized by different microphysical types. Such a multiple realization of higher level types (...) occurs quite frequently even within physics and it should be acceptable for physicalism in general. (shrink)

Nonreductive physicalists have a causal exclusion problem. Given certain theses all physicalists accept, including psychophysical supervenience and the causal closure of the physical realm, it is difficult to see how irreducible mental phenomena could make a causal difference to the world. The upshot, according to those who push the problem, is that we must embrace reductive physicalism. Only then is mental causation saved. -/- Grant the argument, at least provisionally. Here our focus is the conditional question: What form should one's (...) reductionism take if it is motivated in part by the exclusion problem? Must one be a type identity theorist, or are alternative reductive views available, as Jaegwon Kim has suggested more than once? (shrink)

I identify a class of arguments against multiple realization (MR): BookofSand arguments. The arguments are in their general form successful under reasonably uncontroversial assumptions, but this, on the other hand, turns the table on identity theory: If arguments from MR can always be refuted by BookofSand arguments, is identity theory falsifiable? In the absence of operational demarcation criteria, it is not. I suggest a parameterized formal demarcation principle for brain state/process types and show how it can (...) be used to identify previously unconsidered contenders for evidence for MR, e.g., binary classification, division, and sorting. For these to be actual instances of MR, the corresponding psychological kinds must be verifiably, relevantly similar. I also briefly discuss possible linguistic, behavioral, and experimental demarcation criteria for psychological kinds. (shrink)

This paper defends a version of Davidson’s demonstrative theory of quotation and against against the Fregean identity theory (IT henceforth) as articulated and defended by Corey Washington (1992). On the Fregean view, when an expression is referred to by means of quotation the quoted material itself is a linguistic referring expression. Quotation-marks are not needed; when they are used, they serve to make clearer the shift in syntactic and semantic properties effected on the quoted material by its (...) occupying that linguistic context: whatever its usual syntactic function, the quoted material functions as a singular term; whatever its usual semantic function, in that linguistic environment the quoted material refers to itself. On DT, in contrast, quotation-marks themselves are the linguistic bearers of reference, functioning like a demonstrative; the quoted material merely plays the role of a demonstratum. In the version I argue for the referent is obtained through some contextually suggested relation; in the default case the relation will be: … instantiates the linguistic type __, but there are other possibilities. In this way, the view can deal with the fact that we do not merely refer with quotations to expression-types, but also to other entities related in some way to the relevant token we use: features exhibited by the token distinct from those constituting its linguistic type, features exhibited by other tokens of the same type but not by the one actually used (as when, by using a graphic token, we refer to its phonetic type), or even other related tokens. (shrink)

IN discussions of the identity theory of mind, there is constant recourse to two related types of argument, from ordinary language usage, to the effect that the theory in question is either false or meaningless. We can refer to the two arguments under discussion as the category argument and the meaninglessness argument. If either one of these arguments were well founded we could decide a priori without waiting for further research in the relevant sciences, whether or not (...) the mind could be identified with processes of the central nervous system. The answer would be in the negative. It is proposed to examine these two arguments here, and to question the persuasive simplicity with which they have been frequently put forward. If they do not bear up well under closer scrutiny we may not, of course, conclude to the truth of the identity theory; we will conclude only that it has not been a priori eliminated, by these arguments, as a contender for the solution of the mind-body problem. (shrink)

IN discussions of the identity theory of mind, there is constant recourse to two related types of argument, from ordinary language usage, to the effect that the theory in question is either false or meaningless. We can refer to the two arguments under discussion as the category argument and the meaninglessness argument. If either one of these arguments were well founded we could decide a priori without waiting for further research in the relevant sciences, whether or not (...) the mind could be identified with processes of the central nervous system. The answer would be in the negative. It is proposed to examine these two arguments here, and to question the persuasive simplicity with which they have been frequently put forward. If they do not bear up well under closer scrutiny we may not, of course, conclude to the truth of the identity theory; we will conclude only that it has not been a priori eliminated, by these arguments, as a contender for the solution of the mind-body problem. (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)

It is often said that there are two varieties of identity theory. Type-identity theorists interpret physicalism as the claim that every property is identical to a physical property, while token-identity theorists interpret it as the claim that every particular is identical to a physical particular. The aim of this paper is to undermine the distinction between the two. Drawing on recent work connecting generalized identity to truth-maker semantics, I demonstrate that these interpretations are logically (...) equivalent. I then argue that each has the resources to resolve problems facing the other. (shrink)

Among the most interesting features of Homotopy Type Theory is the way it treats identity, which has various unusual characteristics. We examine the formal features of “identity types” in HoTT, and how they relate to its other features including intensionality, constructive logic, the interpretation of types as concepts, and the Univalence Axiom. The unusual behaviour of identity types might suggest that they be reinterpreted as representing indiscernibility. We explore this by defining indiscernibility in HoTT and (...) examine its relationship with identity. We argue that identity types are a primitive component of HoTT and cannot be reduced to indiscernibility. (shrink)

The logic of identity contains riches not seen through the coarse lens of predicate logic. This is one of several lessons to draw from the subtle treatment of identity in Martin‐Löf type theory, to which the reader will be introduced in this article. After a brief general introduction we shall mainly be concerned with the distinction between identity propositions and identity judgements. These differ from each other both in logical form and in logical strength. (...) Along the way, connections to philosophical debates concerning identity are noted. Some use of logical symbolism is inevitable in any serious discussion of type theory, but the emphasis here is on basic ideas rather than technicalities. (shrink)

This paper analyses and criticizes S. Kripke's celebrated argument against materialist identity?theories. While criticisms of Kripke in the literature attack one or more of his premisses, an attempt is made here to show that Kripke's conclusion is unjustified even if his premisses are accepted. Kripke's premisses have sufficient independent plausibility to make this strategy interesting. Having stated Kripke's argument, it is pointed out that Kripke must assume that the contents of the Cartesian intuitions are clear and of a kind (...) suited for the type of explanation he favours, while his own result concerning contents in epistemic contexts is precisely that this might not be so when objects or events we thought distinct happen to be identical. The point is that only by assuming that the identity?theory is false, can Kripke maintain that the Cartesian intuitions express contents which can be explained in his favoured way. But such an assumption is clearly illegitimate when the aim is to establish that the identity?theory is false. Kripke cannot conclude that the identity?theory is false because no explanation of epistemic possibilities is produced, since by his own standards no such explanation can be produced if the identity?theory is true. (shrink)

It is often said that there are two varieties of identity theory. Type-identity theorists interpret physicalism as the claim that every property is identical to a physical property, while token-identity theorists interpret it as the claim that every particular is identical to a physical particular. The aim of this paper is to undermine the distinction between the two. Drawing on recent work connecting generalized identity to truth-maker semantics, I demonstrate that these interpretations are logically (...) equivalent. I then argue that each has the resources to resolve problems facing the other. (shrink)

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

This paper employs a case study from the history of neuroscience—brain reward function—to scrutinize the inductive argument for the so-called ‘Heuristic Identity Theory’ (HIT). The case fails to support HIT, illustrating why other case studies previously thought to provide empirical support for HIT also fold under scrutiny. After distinguishing two different ways of understanding the types of identity claims presupposed by HIT and considering other conceptual problems, we conclude that HIT is not an alternative to the traditional (...) identity theory so much as a relabeling of previously discussed strategies for mechanistic discovery. (shrink)

On the basis of Martin-Löf’s meaning explanations for his type theory a detailed justification is offered of the rule of identity elimination. Brief discussions are thereafter offered of how the univalence axiom fares with respect to these meaning explanations and of some recent work on identity in type theory by Ladyman and Presnell.

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)

This paper focuses on three theories of personal identity that incorporate the idea that personal identity is the result of a person’s adopting certain attitudes towards certain mental states and actions. I call these theories subjective theories of personal identity. I argue that it is not clear what the proponents of these theories mean by “personal identity”. On standard theories, such as animalism or psychological theories, the term “personal identity” refers to the numerical identity (...) of persons and its analysis provides the persistence conditions for persons. I argue that if the subjective theories purport to provide a criterion of numerical personal identity, they fail. A different interpretation may suggest that they purport to provide a non-numerical type of identity for the purpose of providing plausible analyses of certain identity-related practical concerns. I argue that the criteria the subjective theories provide fail to capture several of the identity-related concerns. As a result, this interpretation must be rejected as well. (shrink)

Although it seems plausible to say that the same story can be retold in different media, it is difficult to say exactly what this would entail. The primary difficulty is in coming up with an acceptable theory of story identity. In this article I present several theories of story identity and explore their weaknesses. I argue that in the end we are left with two unattractive options: a strict theory that implies that the same story can (...) almost never be retold and a lenient theory that has trouble differentiating between a general story type and the same story. (shrink)

Families of types are fundamental objects in Martin-Löf type theory. When extending the notion of setoid (type with an equivalence relation) to families of setoids, a choice between proof-relevant or proof-irrelevant indexing appears. It is shown that a family of types may be canonically extended to a proof-relevant family of setoids via the identity types, but that such a family is in general proof-irrelevant if, and only if, the proof-objects of identity types are unique. A (...) similar result is shown for fibre representations of families. The ubiquitous role of proof-irrelevant families is discussed. (shrink)

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

This book examines the conception of the person at work in John Rawls's writings from Theory of Justice to Justice as Fairness: A Restatement. The book aims to show that objections to Rawls's political conception of the person fail and that a Rawlsian conception of political identity is defensible. The book shows that the debate between liberals and communitarians is relevant to the current debate regarding perfectionism and neutrality in politics, and clarifies the debate between Rawls and communitarians (...) in a way that will promote fruitful discussion on the issue of political identity. It does this by providing a clearer account of a conception of personal identity according to which persons are socially constituted, including the intuitions and assumptions underlying the communitarians' conception of persons as "socially constituted." It examines the communitarian objections to liberal political theory and to the liberal conception of persons, the "unencumbered self." The book differentiates between two types of objection to the liberal conception of persons: the metaphysical and normative. It explains Rawls's political conception of persons, and the metaphysical and normative commitments Rawls incurs-and does not incur-in virtue of that conception. It shows that both kind of objection to Rawls's political conception of the person fail. Finally, modifying Rawls's political conception of the person, a Rawlsian conception of political identity is explained and defended. (shrink)

One of the greatest challenges of consciousness research is to understand the relationship between consciousness and its implementing substrate. Current research into the neural correlates of consciousness regards the biological brain as being this substrate, but largely fails to clarify the nature of the brain-consciousness connection. A popular approach within this research is to construe brain-consciousness correlations in causal terms: the neural correlates of consciousness are the causes of states of consciousness. After introducing the notion of the neural correlate of (...) consciousness, we argue (in section 2) that this causal strategy is misguided. It implicitly involves an undesirable dualism of matter and mind and should thus be avoided. A non-causal account of the brain-mind correlations is to be preferred. We favor the theory of the identity of mind and brain, according to which states of phenomenal consciousness are identical with their neural correlates. Research into the neural correlates of consciousness and the theory of identity (in the philosophy of mind) are two major research paradigms that hitherto have had very little mutual contact. We aim to demonstrate that they can enrich each other. This is the task of the third part of the paper in which we show that the identity theory must work with a suitably defined concept of type. Surprisingly, neither philosophers nor neuroscientists have taken much care in defining this central concept; more often than not, the term is used only implicitly and vaguely. We attempt to open a debate on this subject and remedy this unhappy state of affairs, proposing a tentative hierarchical classification of phenomenal and neurophysiological types, spanning multiple levels of varying degrees of generality. The fourth part of the paper compares the theory of identity with other prominent conceptions of the mind-body connection. We conclude by stressing that scientists working on consciousness should engage more with metaphysical issues concerning the relation of brain processes and states of consciousness. Without this, the ultimate goals of consciousness research can hardly be fulfilled. (shrink)

In this paper I will develop a lambda-term calculus, lambda-2Int, for a bi-intuitionistic logic and discuss its implications for the notions of sense and denotation of derivations in a bilateralist setting. Thus, I will use the Curry-Howard correspondence, which has been well-established between the simply typed lambda-calculus and natural deduction systems for intuitionistic logic, and apply it to a bilateralist proof system displaying two derivability relations, one for proving and one for refuting. The basis will be the natural deduction system (...) of Wansing's bi-intuitionistic logic 2Int, which I will turn into a term-annotated form. Therefore, we need a type theory that extends to a two-sorted typed lambda-calculus. I will present such a term-annotated proof system for 2Int and prove a Dualization Theorem relating proofs and refutations in this system. On the basis of these formal results I will argue that this gives us interesting insights into questions about sense and denotation as well as synonymy and identity of proofs from a bilateralist point of view. (shrink)

The paper sets out a new strategy for theory reduction by means of functional sub-types. This strategy is intended to get around the multiple realization objection. We use Kim's argument for token identity (ontological reductionism) based on the causal exclusion problem as starting point. We then extend ontological reductionism to epistemological reductionism (theory reduction). We show how one can distinguish within any functional type between functional sub-types. Each of these sub-types is coextensive with one type (...) of realizer. By this means, a conservative theory reduction is in principle possible, despite multiple realization. We link this account with Nagelian reduction, as well as with Kim's functional reduction. (shrink)

Alfred Schutz’s theory of the social world, often neglected in philosophy, has the potential to capture the interplay of identity and difference which shapes our action, interaction, and experience in everyday life. Compared to still dominant identity-based models such as that of Jürgen Habermas, who assumes a coordination of meaning built on the idealisation of stable rules, Schutz’s theory is an important step forward. However, his central notion of a “type” runs into a difficulty which (...) requires constructive criticism. Against the background of Schutz’s theory of meaning inspired by Bergson and Husserl, his idea of types “taken for granted until further notice” is shown to express a primacy of identity which, in the final analysis, leads into the implausible scenario of ‘ubiquitous tunnel vision’. This makes it necessary to go beyond Schutz and assume an inherently motivated tendency towards difference in meaning termed ‘spontaneity’. Where spontaneity and the opposed tendency towards identity of meaning work together in the application of types, they enable embodied subjects to interact with the world and with each other in the routine yet flexible and sometimes innovative ways which we all know. (shrink)

Modern analytical metaphysics contains many theories and approaches regarding the problem of personal identity. This diversity inevitably leads to the emergence of various classifications, the authors of which are trying to develop a compact way of typologizing existing views. Most of the classifications involve a significant simplification of the theories and approaches under consideration, and some of them are not taken into account at all. As such global classifications, one can single out an approach based on the identity (...) criterion used in the theory (psychological, biological, narrative views). However, numerous local classifications allow one to point out potential differences in theories, even if formally they use a common criterion of identity. Other possible classifications are the division into endurantism and perdurantism, as well as simple (non-reductionist) and complex (reductionist) theories of identity. Special attention is paid to M. Shechtman‘s approach, which offers a local classification of narrative theories. Its main classification is the presentation of the views of researchers in the form of a possible spectrum. The place of a particular philosopher on this spectrum characterizes his views in relation to other supporters of the narrative approach. The purpose of this article is, based on the classification of narrative theories proposed by Shechtman, to propose a classification option for all theories and approaches to the problem of personal identity, which would be sensitive to conceptual details and differences that are important to them. (shrink)

This paper is part of a broader project whose aim is to present a coherent unified approach to natural language dialogue semantics using tools from type theory. Here we explore aspects of our approach which relate to situation theory and situation semantics. We first point out a relationship between type theory and the Austinian notion of truth. We then consider how records in type theory might be used to represent situations and how dependent (...) record types can be used to model constraints on situations. We then sketch treatments of attitude phenomena for which Barwise and Perry proposed situation semantic analyses (perception complements, belief, the Pierre puzzle) as well as two other intensional phenomena (intensional verbs and intentional identity). Finally we give a characterisation of the type theory used and a small illustrative fragment of English. (shrink)

When philosophers address personal identity, they usually explore numerical identity: what are the criteria for a person's continuing existence? When non-philosophers address personal identity, they often have in mind narrative identity: Which characteristics of a particular person are salient to her self-conception? This book develops accounts of both senses of identity, arguing that both are normatively important, and is unique in its exploration of a range of issues in bioethics through the lens of identity. (...) Defending a biological view of our numerical identity and a framework for understanding narrative identity, DeGrazia investigates various issues for which considerations of identity prove critical: the definition of death; the authority of advance directives in cases of severe dementia; the use of enhancement technologies; prenatal genetic interventions; and certain types of reproductive choices. He demonstrates the power of personal identity theory to illuminate issues in bioethics as they bring philosophical theory to life. (shrink)

This paper discusses some of the ways in which Martin-Löf type theory differs from set theory. The discussion concentrates on conceptual, rather than technical, differences. It revolves around four topics: sets versus types; syntax; functions; and identity. The difference between sets and types is spelt out as the difference between unified pluralities and kinds, or sorts. A detailed comparison is then offered of the syntax of the two languages. Emphasis is placed on the distinction between proposition (...) and judgement, drawn by type theory, but not by set theory. Unlike set theory, type theory treats the notion of function as primitive. It is shown that certain inconveniences pertaining to function application that afflicts the set- theoretical account of functions are thus avoided. Finally, the distinction, drawn in type theory, between judgemental and propositional identity is discussed. It is argued that the criterion of identity for a domain cannot be formulated in terms of propositional identity. It follows that the axiom of extensionality cannot be taken as a statement of the criterion of identity for sets. (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)

The problems of referential opacity in psychological contexts require a solution, of which three types are indicated, that contains a profound theory of predication, identity, and individuation. a radical theory, not in the spirit of the current fashions, is outlined. it is called the guise-consubstantiation, conflation, and consociation theory. this theory was first expounded in "thinking and the structure of the world," "philosophia" (1974) and "critica" (1972). the present paper is an introduction to this essay, (...) motivated by two criticisms of romane clark in "not every object of thought has being," "nous" (1978). it is shown that clark's arguments rest on equivocations, one involving the data and the theory, and the other within the theory itself. thus, a discussion of philosophical method turns out to be crucial, and an analysis of expression 'true of' is offered. (shrink)

This essay explores how the social location of white traitorous identities might be understood. I begin by examining some of the problematic implications of Sandra Harding's standpoint framework description of race traitors as 'becoming marginal.' I argue that the location of white traitors might be better understood in terms of their 'decentering the center.' I distinguish between 'privilege-cognizant' and 'privilege-evasive' white scripts. Drawing on the work of Marilyn Frye and Anne Braden, I offer an account of the contrasting perceptions and (...) behaviors of white who animate one type of script and those who struggle to forge the other type. I use Maria Lugones account of identity and notions of 'world travel' and 'loving perception' and Aristotle's virtue theory to explicate the ways whites, and white feminists in particular, might cultivate a traitorous character conducive to an antiracist politics. (shrink)

This is a brief report on results reported at length in our paper [2], made for the purpose of a presentation at the workshop to be held in November 2011 in Cambridge on the Principia Mathematica of Russell and Whitehead ([?], hereinafter referred to briefly as PM ). That paper grew out of a reading of the paper [3] of Kamareddine, Nederpelt, and Laan. We refereed this paper and found it useful for checking their examples to write our own independent (...) computer type-checker for the type system of PM ([1]), which led us to think carefully about formalization of the language and the type system of PM A modern mathematical logician reading PM finds that it is not completely formalized in a modern sense. The type theory in particular is inarguably not formalized, as no notation for types is given at all! In PM itself, the only type annotations which appear are occasional numerical indices indicating order; the type notation we use here extends one introduced later by Ramsey. The authors of PM regard the absence of explicit indications of type as a virtue of their system: they call it “systematic ambiguity”; modern computer scientists refer to this as “polymorphism”. The language of PM is also not completely formalized, and it is typographically inconvenient for computer software to which ASCII input is to be given. The notation of PM for abstractions (propositional functions) does not use head binders; the order of the arguments of a complex expression is determined by the alphabetical order of the bound variables. For example ˆa < ˆb is the “less than” relation while ˆb < ˆa is the “greater than” relation (this is indicated by the alphabetical order of the variables). In PM , the fact that a variable is bound in a propositional function is indicated by circumflexing it. Variables bound by quantifiers are not circumflexed. A feature of the notation of [3], carried over into ours, is that no circumflexes are used: notations for propositions and the corresponding propositional functions are identical.. (shrink)