There is a long tradition comparing moral knowledge to mathematical knowledge. In this paper, I discuss apparent similarities and differences between knowledge in the two areas, realistically conceived. I argue that many of these are only apparent, while others are less philosophically significant than might be thought. The picture that emerges is surprising. There are definitely differences between epistemological arguments in the two areas. However, these differences, if anything, increase the plausibility of moral realism as compared to mathematical realism. It (...) is hard to see how one might argue, on epistemological grounds, for moral antirealism while maintaining commitment to mathematical realism. But it may be possible to do the opposite. (shrink)

L'informatique se définissant comme le traitement rationnel de l'information par machine automatique et l'intelligence se caractérisant par une même capacité de traitement rationnel, il était inévitable que l'on songe à associer l'intelligence au traitement automatique de l'information. C'est ce qu'a fait John McCarthy en forgeant le terme d'intelligence artificielle. Par «intelligence artificielle» on peut vouloir exprimer l'ambition de1. Recréer, transformer ou développer l'intelligence artificiellement2. Simuler l'intelligence en la reconstituant dans des modéles imitant certains aspects de notre intelligence dite naturelle.

The ecological approach to perception-action is unlike the standard approach in several respects. It takes the animal-in-its-environment as the proper scale for the theory and analysis of perception-action, it eschews symbol based accounts of perception-action, it promotes self-organization as the theory-constitutive metaphor for perception-action, and it employs self-referring, non-predicative definitions in explaining perception-action. The present article details the complexity issues confronted by the ecological approach in terms suggested by Rosen and introduces non-well-founded set theory as a potentially useful tool for (...) expressing them. The issues and the tool are brought to focus in the concept of affordance that is the basis for explanation of prospective control of action in the ecological approach. (shrink)

I consider the well-known criticism of Quine's characterization of first-order logical truth that it expands the class of logical truths beyond what is sanctioned by the model-theoretic account. Briefly, I argue that at best the criticism is shallow and can be answered with slight alterations in Quine's account. At worse the criticism is defective because, in part, it is based on a misrepresentation of Quine. This serves not only to clarify Quine's position, but also to crystallize what is and what (...) is not at issue in choosing the model-theoretic account of first-order logical truth over one in terms of substitutions. I conclude by highlighting the need for justifying the belief that the definition of first-order logical truth in terms of models is superior to its definition in terms of substitutions. (shrink)

It is well known that the circumflex notation used by Russell and Whitehead to form complex function names in Principia Mathematica played a role in inspiring Alonzo Church's “lambda calculus” for functional logic developed in the 1920s and 1930s. Interestingly, earlier unpublished manuscripts written by Russell between 1903–1905—surely unknown to Church—contain a more extensive anticipation of the essential details of the lambda calculus. Russell also anticipated Schönfinkel's combinatory logic approach of treating multiargument functions as functions having other functions as value. (...) Russell’s work in this regard seems to have been largely inspired by Frege’s theory of functions and “value-ranges”. This system was discarded by Russell due to his abandonment of propositional functions as genuine entities as part of a new tack for solving Russell’s paradox. In this article, I explore the genesis and demise of Russell’s early anticipation of the lambda calculus. (shrink)

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

This open access book is a superb collection of some fifteen chapters inspired by Schroeder-Heister's groundbreaking work, written by leading experts in the field, plus an extensive autobiography and comments on the various contributions by Schroeder-Heister himself. For several decades, Peter Schroeder-Heister has been a central figure in proof-theoretic semantics, a field of study situated at the interface of logic, theoretical computer science, natural-language semantics, and the philosophy of language. -/- The chapters of which this book is composed discuss the (...) subject from a rich variety of angles, including the history of logic, the proper interpretation of logical validity, natural deduction rules, the notions of harmony and of synonymy, the structure of proofs, the logical status of equality, intentional phenomena, and the proof theory of second-order arithmetic. All chapters relate directly to questions that have driven Schroeder-Heister's own research agenda and to which he has made seminal contributions. The extensive autobiographical chapter not only provides a fascinating overview of Schroeder-Heister's career and the evolution of his academic interests but also constitutes a contribution to the recent history of logic in its own right, painting an intriguing picture of the philosophical, logical, and mathematical institutional landscape in Germany and elsewhere since the early 1970s. The papers collected in this book are illuminatingly put into a unified perspective by Schroeder-Heister's comments at the end of the book. Both graduate students and established researchers in the field will find this book an excellent resource for future work in proof-theoretic semantics and related areas. (shrink)

The motivating question of this paper is: ‘How are our beliefs in the theorems of mathematics justified?’ This is distinguished from the question ‘How are our mathematical beliefs reliably true?’ We examine an influential answer, outlined by Russell, championed by Gödel, and developed by those searching for new axioms to settle undecidables, that our mathematical beliefs are justified by ‘intuitions’, as our scientific beliefs are justified by observations. On this view, axioms are analogous to laws of nature. They are postulated (...) to best systematize the data to be explained. We argue that there is a decisive difference between the cases. There is agreement on the data to be systematized in the scientific case that has no analog in the mathematical one. There is virtual consensus over observations, but conspicuous dispute over intuitions. In this respect, mathematics more closely resembles stereotypical philosophy. We conclude by distinguishing two ideas that have long been associated -- realism (the idea that there is an independent reality) and objectivity (the idea that in a disagreement, only one of us can be right). We argue that, while realism is true of mathematics and philosophy, these domains fail to be objective. One upshot of the discussion is that even questions of fundamental physics may fail to be objective in roughly the sense that the question, ‘Is the Parallel Postulate is true?’, understood as one of pure mathematics, fails to be. Another is a kind of pragmatism. Factual questions in mathematics, modality, logic, and evaluative areas go proxy for non-factual practical ones. -/- . (shrink)

Although Benjamin Schnieder’s theory of the “ordinary conception” of properties successfully handles paradoxical properties—particularly, the property of non-self-instantiation—it fails to account for ordinary, non-pathological cases. The theory allows the inference of ‘a has the property of being F’ only given F(a) and the prior assertibility of ‘the property of being F can exist’. While this allows us to block an inference to a contradiction, it also blocks all of the non-pathological instances of the inference from ‘a is F’ to ‘a (...) has the property of being F’. It thereby fails both as a theory of the ordinary conception and as a replacement of the ordinary notion, assuming the latter is defective. (shrink)

It’s generally taken to be established that no local hidden-variable theory is possible. That conclusion applies if our world is a _thread_, where a thread is a world where particles follow trajectories, as in Pilot-Wave theory. But if our world is taken to be a _set_ of threads locality can be recovered. Our world can be described by a _many-threads_ theory, as defined by Jeffrey Barrett in the opening quote. Particles don’t follow trajectories because a particle in our world is (...) a set of _elemental_ particles following different trajectories, each in a thread. The “elements” of a superposition are construed as subsets in such a way that a particle in our world only has definite position if all its set-theoretic elements are at corresponding positions in each thread. Wavefunction becomes a 3D density distribution of particles’ subset measures, the stuff of an electron’s “probability cloud”. Current Pilot-Wave theory provides a non-relativistic dynamics for the elemental particles (approximated by Many Interacting Worlds theory). EPR-Bell nonlocality doesn’t apply because the relevant measurement outcomes in the absolute elsewhere of an observer are always in superposition. (shrink)

This book discusses the problem of mathematical knowledge, and its broader philosophical ramifications. It argues that the problem of explaining the (defeasible) justification of our mathematical beliefs (‘the justificatory challenge’), arises insofar as disagreement over axioms bottoms out in disagreement over intuitions. And it argues that the problem of explaining their reliability (‘the reliability challenge’), arises to the extent that we could have easily had different beliefs. The book shows that mathematical facts are not, in general, empirically accessible, contra Quine, (...) and that they cannot be dispensed with, contra Field. However, it argues that they might be so plentiful that our knowledge of them is intelligible. The book concludes with a complementary ‘pluralism’ about modality, logic and normative theory, highlighting its revisionary implications. Metaphysically, pluralism engenders a kind of perspectivalism and indeterminacy. Methodologically, it vindicates Carnap’s pragmatism, transposed to the key of realism. (shrink)

In his “Epistemology Naturalized,” Quine embraces a form of Humeanism. In this paper, I try to work out the significance of this Humeanism. In particular, I argue that it represents an anti-metaphysical position that Quine shares with Carnap. Crucial to my account is that contrary to much contemporary thinking on metaphysics, Carnap, and Quine following him, recognize both an ontological and an epistemological sense of metaphysics. As commentators have frequently acknowledged, Carnap and Quine disagree over rejecting metaphysics in the ontological (...) sense. I will argue, though, that they agree in rejecting metaphysics in their shared epistemological sense of the term. (shrink)

According to act theories, propositions are structured cognitive act‐types. Act theories appear to make propositions inherently representational and truth‐evaluable, and to provide solutions to familiar problems with alternative theories, including Frege’s and Russell’s problems, and the third‐realm and unity problems. Act theories have critical problems of their own, though: acts as opposed to their objects are not truth evaluable, not structured in the right way, not expressed by sentences, and not the objects of propositional attitudes. I show how identifying propositions (...) with other cognitive event‐types, namely thoughts, has the perceived virtues of act theories without the defects. (shrink)

We consider the argument that Tarski's classic definitions permit an intelligence---whether human or mechanistic---to admit finitary evidence-based definitions of the satisfaction and truth of the atomic formulas of the first-order Peano Arithmetic PA over the domain N of the natural numbers in two, hitherto unsuspected and essentially different, ways: (1) in terms of classical algorithmic verifiabilty; and (2) in terms of finitary algorithmic computability. We then show that the two definitions correspond to two distinctly different assignments of satisfaction and truth (...) to the compound formulas of PA over N---I_PA(N; SV ) and I_PA(N; SC). We further show that the PA axioms are true over N, and that the PA rules of inference preserve truth over N, under both I_PA(N; SV ) and I_PA(N; SC). We then show: (a) that if we assume the satisfaction and truth of the compound formulas of PA are always non-finitarily decidable under I_PA(N; SV ), then this assignment corresponds to the classical non-finitary putative standard interpretation I_PA(N; S) of PA over the domain N; and (b) that the satisfaction and truth of the compound formulas of PA are always finitarily decidable under the assignment I_PA(N; SC), from which we may finitarily conclude that PA is consistent. We further conclude that the appropriate inference to be drawn from Goedel's 1931 paper on undecidable arithmetical propositions is that we can define PA formulas which---under interpretation---are algorithmically verifiable as always true over N, but not algorithmically computable as always true over N. We conclude from this that Lucas' Goedelian argument is validated if the assignment I_PA(N; SV ) can be treated as circumscribing the ambit of human reasoning about `true' arithmetical propositions, and the assignment I_PA(N; SC) as circumscribing the ambit of mechanistic reasoning about `true' arithmetical propositions. (shrink)

During the past few decades, a radical shift has occurred in how philosophers conceive of the relation between science and philosophy. A great number of analytic philosophers have adopted what is commonly called a ‘naturalistic’ approach, arguing that their inquiries ought to be in some sense continuous with science. Where early analytic philosophers often relied on a sharp distinction between science and philosophy—the former an empirical discipline concerned with fact, the latter an a priori discipline concerned with meaning—philosophers today largely (...) follow Willard Van Orman Quine (1908-2000) in his seminal rejection of this distinction. -/- This book offers a comprehensive study of Quine’s naturalism. Building on Quine’s published corpus as well as thousands of unpublished letters, notes, lectures, papers, proposals, and annotations from the Quine archives, this book aims to reconstruct both the nature (chapters 2-4) and the development (chapter 5-7) of his naturalism. As such, this book aims to contribute to the rapidly developing historiography of analytic philosophy, and to provide a better, historically informed, understanding of what is philosophically at stake in the contemporary naturalistic turn. (shrink)

The mereological predicate ‘is part of’ can be used to define the predicate ‘is identical with’. I argue that this entails that mereological theories can be ideologically simpler than nihilistic theories that do not use the notion of parthood—contrary to what has been argued by Ted Sider. Moreover, if one accepts an extensional mereology, there are good philosophical reasons apart from ideological simplicity to give a mereological definition of identity.

This article surveys recent literature by Parsons, McGee, Shapiro and others on the significance of categoricity arguments in the philosophy of mathematics. After discussing whether categoricity arguments are sufficient to secure reference to mathematical structures up to isomorphism, we assess what exactly is achieved by recent ‘internal’ renditions of the famous categoricity arguments for arithmetic and set theory.

Transfinite recursion is an essential component of set theory. In this paper, we seek intrinsically justified reasons for believing in recursion and the notions of higher computation that surround it. In doing this, we consider several kinds of recursion principles and prove results concerning their relation to one another. We then consider philosophical motivations for these formal principles coming from the idea that computational notions lie at the core of our conception of set. This is significant because, while the iterative (...) conception of set has been widely recognized as insufficient to establish replacement and recursion, its supplementation by considerations pertaining to algorithms suggests a new and philosophically well-motivated reason to believe in such principles. (shrink)

La relation d'identité est-elle univoque, ou est-elle au contraire relative au concept sous lequel le jugement est énoncé? Depuis quelques années, parmi les philosophes anglo-américains, partisans et adversaires de la thèse que l'on a appelée « la relativité de l'identité », se sont affrontés sur ce point.

Unaware of Frege's 1879 Begriffsschrift, Russell's 1903 The Principles of Mathematics set out a calculus for logic whose foundation was the doctrine that any such calculus must adopt only one style of variables–entity (individual) variables. The idea was that logic is a universal and all-encompassing science, applying alike to whatever there is–propositions, universals, classes, concrete particulars. Unfortunately, Russell's early calculus has appeared archaic if not completely obscure. This paper is an attempt to recover the formal system, showing its philosophical background (...) and its semantic completeness with respect to the tautologies of a modern sentential calculus. (shrink)

The Institute Vienna Circle held a conference in Vienna in 2003, Cambridge and Vienna a?

For the modern set theorist the empty set Ø, the singleton {a}, and the ordered pair 〈x, y〉 are at the beginning of the systematic, axiomatic development of set theory, both as a field of mathematics and as a unifying framework for ongoing mathematics. These notions are the simplest building locks in the abstract, generative conception of sets advanced by the initial axiomatization of Ernst Zermelo [1908a] and are quickly assimilated long before the complexities of Power Set, Replacement, and Choice (...) are broached in the formal elaboration of the ‘set of’f {} operation. So it is surprising that, while these notions are unproblematic today, they were once sources of considerable concern and confusion among leading pioneers of mathematical logic like Frege, Russell, Dedekind, and Peano. In the development of modern mathematical logic out of the turbulence of 19th century logic, the emergence of the empty set, the singleton, and the ordered pair as clear and elementary set-theoretic concepts serves as amotif that reflects and illuminates larger and more significant developments in mathematical logic: the shift from the intensional to the extensional viewpoint, the development of type distinctions, the logical vs. the iterative conception of set, and the emergence of various concepts and principles as distinctively set-theoretic rather than purely logical. Here there is a loose analogy with Tarski's recursive definition of truth for formal languages: The mathematical interest lies mainly in the procedure of recursion and the attendant formal semantics in model theory, whereas the philosophical interest lies mainly in the basis of the recursion, truth and meaning at the level of basic predication. Circling back to the beginning, we shall see how central the empty set, the singleton, and the ordered pair were, after all. (shrink)

The status of the equality predicate as a logical constant is problematic. In the paper we look at the problem from the proof-theoretic standpoint and survey several ways of treating equality in formal systems of different sorts. In particular, we focus on the framework of sequent calculus and examine equality in the light of criteria of logicality proposed by Hacking and Došen. Both attempts were formulated in terms of sequent calculus rules, although in the case of Došen it has a (...) nonstandard character. It will be shown that equality can be characterised in a way which satisfies Došen’s criteria of logicality. In the case of Hacking’s approach the fully satisfying result can be obtained only for languages with a nonempty, finite set of predicate constants other than equality. Otherwise, cut elimination theorem fails to hold. (shrink)

Formal semantic theories are generally thought to make contact with pre-theoretic semantic notions of aboutness and reference. The nature of that contact is, however, not always straightforward. This paper addresses two debates where that issue assumes a significant role. I begin with Simchen’s recent argument that Lewisian Interpretationism succumbs to referential indeterminacy. I develop a proposal about the relationship between the theoretical notion of a term’s semantic value and the pre-theoretic notion of reference, and argue that the indeterminacy Simchen identifies (...) does not constitute a form of referential indeterminacy. In the second part, I apply these resources to the debate between singularist and pluralist approaches to the semantics of plural terms, arguing that a certain form of singularism that emerges from the dialectic ends up agreeing with the pluralist at the level of reference, if not semantic value. The paper concludes with some remarks on what a properly referential style of singularism might look like. (shrink)

W.V. Quine is a well-known proponent of naturalism, the view on which reality is described only in science. He is also well-known for arguing that our current scientific theories commit us to the existence of abstract objects. It is tempting to believe that the naturalistic philosopher should think scientists outside of philosophy are in the best position to assess the merits of revising our current commitment to abstract objects. But Quine rejects this deferential view. On the reading of Quine’s philosophical (...) methodology that I defend in this paper, the naturalistic philosopher not only may assess the merits of revising the commitments of our scientific theories, but also will recommend we make such revisions if doing so simplifies and clarifies our science. To develop my reading, I will examine John Burgess and Gideon Rosen’s naturalism in ontology that includes the deferential view Quine rejects. By explaining how Quine’s naturalism differs from the anti-revisionist, deferential naturalism in philosophy of mathematics that Burgess and Rosen advance, I seek to clarify and advance contemporary debates on naturalism. (shrink)

Quine often argued for a simple, untyped system of logic rather than the typed systems that were championed by Russell and Carnap, among others. He claimed that nothing important would be lost by eliminating sorts, and the result would be additional simplicity and elegance. In support of this claim, Quine conjectured that every many-sorted theory is equivalent to a single-sorted theory. We make this conjecture precise, and prove that it is true, at least according to one reasonable notion of theoretical (...) equivalence. Our clarification of Quine’s conjecture, however, exposes the shortcomings of his argument against many-sorted logic. (shrink)

In his seminal work “The Concept of Truth in Formalized Languages”, Alfred Tarski showed how to construct a formally correct and materially adequate definition of true sentence for certain formalized languages. These results have, eventually, been accepted and applauded by philosophers and logicians nearly in unison. Its Postscript, written two years later, however, has given rise to a considerable amount of controversy. There is an ongoing debate on what Tarski really said in the postscript. These discussions often regard Tarski as (...) putatively changing his logical framework from type theory to set theory. In what follows, we will compare the original results with those presented two years later. After a brief outline of Carnap’s program in The Logical Syntax of Language we will determine its significance for Tarski’s final results. (shrink)

The contemporary popularity of semantic externalism has arisen from so-called Twin Earth thought experiments which suggest that the representational content of a natural kind term cannot be wholly determined by processes within a speaker's body. Such arguments depend on the intuition that the extensions of natural kind terms cannot have changed as the result of the scientific investigation of natural kinds' constitutions. I demonstrate that this externalist intuition depends on an assumption about the mentality of isomorphic doppelgangers which has never (...) been questioned but which is nonetheless arguably false. I develop an alternative view of the instantiation of mind which entails a revision of our understanding of the constitution of environmental objects. The picture seems to be fully coherent despite its oddity and I can find no good reason to reject it. The conclusion must be that the case for semantic externalism is thus less compelling than is often supposed. (shrink)

This paper draws its title from the recent symposium of which it was part; it attempts to respond to the question raised by that title, taking current work in set theory into account. To this end the paper contrasts set theory with number theory, examines a severe brand of set-theoretic realism that is suggested by a passage from Godel, and sketches a first-order way of looking at the results about competing extensions of Zermelo-Fraenkel set theory. A formalistic sentiment may be (...) detectable in some portions of the paper. (shrink)

Although the notion of logical object plays a key role in Frege's foundational project, it has hardly been analyzed in depth so far. I argue that Marco Ruffino's attempt to fill this gap by establishing a close link between Frege's treatment of expressions of the form ‘the concept F’ and the privileged status Frege assigns to extensions of concepts as logical objects is bound to fail. I argue, in particular, that Frege's principal motive for introducing extensions into his logical theory (...) is not to be able to make in-direct statements about concepts, but rather to define all numbers as logical objects of a fundamental kind in order to ensure that we have the right cognitive access to them qua logical objects via Axiom V. Contrary to what Ruffino claims, reducibility to extensions cannot be the ‘ultimate criterion’ for Frege of what is to be regarded as a logical object. (shrink)

I compare Russell’s theory of mathematical functions, the “descriptive functions” from Principia Mathematica ∗30, with Frege’s well known account of functions as “unsaturated” entities. Russell analyses functional terms with propositional functions and the theory of definite descriptions. This is the primary technical role of the theory of descriptions in P M . In Principles of Mathematics and some unpublished writings from before 1905, Russell offered explicit criticisms of Frege’s account of functions. Consequenly, the theory of descriptions in “On Denoting” can (...) be seen as a crucial part of Russell’s larger logicist reduction of mathematics,aswellasanexcursionintothetheoryof reference.
. (shrink)

The purported fact that geometric theories formulated in terms of points and geometric theories formulated in terms of lines are “equally correct” is often invoked in arguments for conceptual relativity, in particular by Putnam and Goodman. We discuss a few notions of equivalence between first-order theories, and we then demonstrate a precise sense in which this purported fact is true. We argue, however, that this fact does not undermine metaphysical realism.

The semantic rules that govern ordinary property discourse appear to give rise to a version of Russell's antinomy. Do we therefore have an inconsistent conception of properties? This paper firstly develops a consistent conception of properties and secondly argues that we may indeed interpret ordinary property discourse as expressing the consistent conception rather than an inconsistent one.

It is fairly well known that Wittgenstein's criticisms of Russell's multiple‐relation theory of judgement had a devastating effect on the latter's philosophical enterprise. The exact nature of those criticisms however, and the explanation for the severity of their consequences, has been a source of confusion and disagreement amongst both Russell and Wittgenstein scholars. In this paper, I offer an interpretation of those criticisms which shows them to be consonant with Wittgenstein's general critique of Russell's conception of logic and which serves (...) to elucidate some of the notoriously enigmatic passages of the Tractatus. In particular, I seek to show the continuity of Wittgenstein's criticisms of the theory of judgement with his remarks on Russell's paradox and the theory of types. In addition, I place these issues in the context of Russell's own philosophical ambitions in order to reveal the deep divisions between the two over the nature of logical form and the analysis of propositional content. (shrink)

In recent years philosophers have been interested in the methodology of metaphysics. Most of these developments are related to formal work in logic or physics, often against the backdrop of the Carnap-Quine debate on ontology. Drawing on Quine’s later work, I argue that a psychological or cognitive perspective on metaphysical topics may be a valuable addition to contemporary metametaphysics. The method is illustrated by means of cognitive studies of the notions “identity,” “vagueness,” and “object” and is compared to other extant (...) metametaphysical positions. (shrink)

In his late philosophy, Quine generalized the structuralist view in the philosophy of mathematics that mathematical theories are indifferent to the ontology we choose for them. According to his ‘global structuralism’, the choice of objects does not matter to any scientific theory. In the literature, this doctrine is mainly understood as an epistemological thesis claiming that the empirical evidence for a theory does not depend on the choice of its objects. The present paper proposes a new interpretation suggested by Quine’s (...) recently published Kant Lectures from 1980 according to which his global structuralism is a semantic thesis that belongs to his theory of ontological reduction. It claims that a theory can always be reformulated in such a way that its truth does not presuppose the existence of the original objects, but only of some objects that can be considered as their proxies. Quine derives this claim from the principle of the semantic primacy of sentences, which is supposed to license the ontological reductions he uses to establish his global structuralism. It is argued that these reductions do not actually work because they do not account for some hidden ontological commitments that are not detected by his criterion of ontological commitment. (shrink)

It is shown that two formally consistent type-free second-order systems, due to Cocchiarella, and based on the notion of homogeneous stratification, are subject to a contingent version of Russell's paradox.

Four progressively ambitious systems of modal propositional logic are set forth, together with decision procedures. The simultaneous employment of parenthesis notation and parenthesis-free notation, the dual use of symbols as primitive and defined, and the introduction of a new modal operator (the truth operator) are the principal devices used to effect the development of these logics. The first two logics turn out to be "the same" as two of von Wright's systems.

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