Can the right to private property be claimed as one of the `rights of mankind'? This is the central question of this comprehensive and critical examination of the subject of private property. Jeremy Waldron contrasts two types of arguments about rights: those based on historical entitlement, and those based on the importance of property to freedom. He provides a detailed discussion of the theories of property found in Locke's Second Treatise and Hegel's Philosophy of Right to illustrate this contrast. (...) The book contains original analyses of the concept of ownership, the ideas of rights, and the relation between property and equality. The author's overriding determination throughout is to follow through the arguments and values used to justify private ownership. He finds that the traditional arguments about property yield some surprisingly radical conclusions. (shrink)

"Arguing that debates over legitimacy, political violence, freedom, and justice would benefit greatly from cross-tradition theorizing, this book shows how putting analytic and continental political theory in conversation would help us to overcome these intractable problems"--.

Philosophers of science have insisted that evidence of underlying mechanisms is required to support claims about the effects of medical interventions. Yet evidence about mechanisms does not feature on dominant evidence-based medicine “hierarchies.” After arguing that only inferences from mechanisms (“mechanistic reasoning”)—not mechanisms themselves—count as evidence, I argue for a middle ground. Mechanistic reasoning is not required to establish causation when we have high-quality controlled studies; moreover, mechanistic reasoning is more problematic than has been assumed. Yet where the problems can (...) be overcome, mechanistic reasoning can and should be used as evidence. (shrink)

We review three broadly geometrodynamical---and in part, Machian or relational---projects, from the perspective of spacetime functionalism. We show how all three are examples of functionalist reduction of the type that was advocated by D. Lewis, and nowadays goes by the label `the Canberra Plan’. The projects are: the recovery of geometrodynamics by Hojman et al. ; the programme of Schuller and collaborators to deduce a metric from the physics of matter fields; the deduction of the ADM Hamiltonian by Gomes and (...) Shyam. We end by drawing a positive corollary about shape dynamics: namely, it has a good rationale for the Hamiltonian it postulates. (shrink)

In this paper we present a schema for describing dualities between physical theories, and illustrate it in detail with the example of bosonization: a boson-fermion duality in two-dimensional quantum field theory. The schema develops proposals in De Haro : these proposals include construals of notions related to duality, like representation, model, symmetry and interpretation. The aim of the schema is to give a more precise criterion for duality than has so far been considered. The bosonization example, or boson-fermion duality, has (...) the feature of being simple, yet rich enough, to illustrate the most relevant aspects of our schema, which also apply to more sophisticated dualities. The richness of the example consists, mainly, in its concern with two non-trivial quantum field theories: including massive Thirring-sine-Gordon duality, and non-abelian bosonization. This prompts two comparisons with the recent philosophical literature on dualities:--- Unlike the standard cases of duality in quantum field theory and string theory, where only specific simplifying limits of the theories are explicitly known, the boson-fermion duality is known to hold {\it exactly}. This exactness can be exhibited explicitly. The bosonization example illustrates both the cases of isomorphic and {\it non-isomorphic} models: which we believe the literature on dualities has not so far discussed. (shrink)

Plato is often acknowledged as the first philosophical critic of democracy and his Republic is regularly taken as a paradigm of an anti-democratic work. While it is true that Plato objected to much about the democracy of his own time, Plato’s political theorizing also reveals an interest in improving democratic institutions. This chapter explores three themes in Plato’s thinking about democracy: firstly, Plato's insistence that rulers should be knowledgeable and his claim that most people are politically incompetent (§1); secondly, Plato's (...) criticisms of oratory and the corrupting effects of public rhetoric (§2); thirdly, Plato's use of democratic institutions in the Laws (§3). Once we appreciate these different evaluations of democratic practices, we can see that Plato was not simply ‘anti-democratic’ or ‘pro-democratic’ but thought some democratic practices should be abandoned, some reformed, and some adopted. (shrink)

Debates about the ethics and effects of placebos and whether ‘placebos’ in clinical trials of complex treatments such as acupuncture are adequate rage. Yet there is currently no widely accepted definition of the ‘placebo’. A definition of the placebo is likely to inform these controversies. Grünbaum’s characterization of placebos and placebo effects has been touted by some authors as the best attempt thus far, but has not won widespread acceptance largely because Grünbaum failed to specify what he means by a (...) therapeutic theory and because he does not stipulate a special role for expectation effects. Grünbaum claims that placebos are treatments whose ‘characteristic features’ do not have therapeutic effects on the target disorder. I show that with four modifications, Grünbaum’s definition provides a defensible account of placebos for the purpose of constructing placebo controls within clinical trials. The modifications I introduce are: adding a special role for expectations, insisting that placebo controls control for all and only the effects of the incidental treatment features, relativizing the definition of placebos to patients, and introducing harmful interventions and nocebos to the definitional scheme. I also provide guidance for classifying treatment features as characteristic or incidental. (shrink)

Some propositions are true, and it is true that some propositions are true. Each of these facts looks like an impeccable ground of the other. But they cannot both ground each other, since grounding is asymmetric. This paper explores two new diagnoses of this much discussed puzzle. The tools of higher-order logic are used to show how both diagnoses can be fleshed out into strong and consistent theories of grounding. These theories of grounding in turn demand new theories of the (...) granularity of propositions, properties, and relations. Even those who are uninterested in grounding should take seriously these pictures of reality’s logical structure, which are in many ways reminiscent of Russell’s and Wittgenstein’s logical atomism. (shrink)

Written as a series of lectures, The Ecological Life offers a humanistic perspective on environmental philosophy that challenges some of the dogmas of deep ecology and radical environmentalism while speaking for their best desires. The book argues that being human-centered leaves us open to ecological identifications, rather than the opposite. Bendik-Keymer draws on analytic and continental traditions of philosophy as well as literature and visual media. He argues for a sense of ecological justice consonant with human rights, and shows how (...) humanistic thinking is committed to deepening respect for life and our ecological orientation. In a clear, jargon-free and conversational tone, The Ecological Life presents a timely and important contribution to civic engagement in an ecological century. (shrink)

Ernst Cassirer’s book Substanzbegriff und Funktionsbegriff is a difficult book for contemporary readers to understand. Its topic, the theory of concept formation, engages with debates and authors that are largely unknown today. And its “historical” style violates the philosophical standards of clarity first propounded by early analytic philosophers. Cassirer, for instance, never says explicitly what he means by “substance-concept” and “function-concept.” In this article, I answer three questions: Why did Cassirer choose to focus on the topic of concept formation? What (...) did Cassirer mean in contrasting “substance-concepts” and “function-concepts”? How does Cassirer’s polemic against traditional theories of concept formation lead to the distinctive philosophy of mathematics that he defends in the book? I argue that Cassirer’s contrast between substance-concepts and function-concepts includes a series of interrelated contrasts—contrasts that touch on issues in logic, metaphysics, epistemology, and the theory of objectivity. Cassirer’s defense of mathematical structuralism flows out of a progressively unfolding and intricate argument that begins with epistemological problems in the theory of concept formation. (shrink)

In this paper, I propose a theory of living organisms that captures the insights of both traditional Aristotelian hylomorphism and John Dupré's “biological processualism”. Like traditional Aristotelian hylomorphism, the proposed theory understands material objects to be comprised of both matter and form. Unlike contemporary structural varieties of hylomorphism, however, it does not understand the form of a material object to be a relation, configuration, or structure exhibited by its parts but an activity or process in which its matter is continuously (...) engaged. Following Mark Steen, I call the proposed theory “Hyloenergeism”. As a version of hylomorphism, hyloenergeism better captures the inherent dynamism of living organisms than contemporary structural approaches. And it does so not by abandoning the substantialist paradigm, as Dupré's biological processualism does, but by reconceptualizing the nature of material substances as possessing a processual core. Hyloenergeism, then, paves a middle way for those looking for a substance view of living organisms sensitive to the concerns raised by contemporary processualist philosophers of biology. (shrink)

A resilient issue in research ethics is whether and when a placebo-controlled trial is justified if it deprives research subjects of a recognized treatment. The clinicians' moral duty to provide the best available care seems to require the use of ‘active’ controlled trials that use an established treatment as a control whenever such a therapy is available. In another regard, ACTs are supposedly methodologically inferior to PCTs. Hence, the moral duty of the clinical researcher to use the best methods will (...) favor PCTs. In this target article, I analyze the three reasons for believing that ACTs are inferior to PCTs namely: 1) ACTs lack ‘assay sensitivity’; 2) ACTs do not measure absolute effect size; and 3) ACTs require more participants; and I contend that none are acceptable. Consequently the tension between clinical and research ethics dissolves: the moral duty of the clinician to avoid PCTs is unopposed by methodological considerations. (shrink)

Issues pertaining to sex and gender continue to be some of the most hotly debated topics of our time. While many of the most heated disputes occur at the level of politics and public policy, metaphysics, too, has a crucial role to play in these debates. In this essay, I explore several key metaphysical debates concerning sex and gender through the lenses of two important areas in contemporary metaphysics: the metaphysics of essence and the ontology of the human person. The (...) goal here is not to advocate any particular position on these issues, but to show how the tools of contemporary metaphysics can help to offer a more comprehensive map of the conceptual terrain, indicating where major areas of agreement can be found and where the most important disagreements really lie. (shrink)

Since his death in 1986, Michel de Certeau's reputation as a thinker has steadily grown both in France and throughout the English-speaking world. His work is extraordinarily innovative and wide-ranging, cutting across issues in historiography, literary and cultural studies, anthropology, sociology, theology, philosophy and psychoanalysis. This book represents the first full-length study of Certeau's thought. It is organized around the central theme of interpretation and alterity, which Ahearne uses to illuminate Certeau's work as a whole. The author also examines Certeau's (...) theory and practice of historiography; his reflection on the relations between changing historical forms of writing, reading and orality; and his distinction between the "strategic" programmes of the politically powerful and the "tactics" of the relatively powerless. Ahearne places Certeau's work in its general intellectual context, relating it to the views of important contemporary thinkers, such as Pierre Bourdieu and Michel Foucault, and demonstrating the decisive importance to Certeau's thought of the writings of the early modern mystics and travellers. This book constitutes an excellent critical introduction to Certeau's work, while also providing a comprehensive and nuanced reading for those already familiar with his thought. (shrink)

This volume brings together a wide-ranging collection of the papers written by Jeremy Waldron, one of the most internationally respected political theorists writing today. The main focus of the collection is on substantive issues in modern political philosophy. The first six chapters deal with freedom, toleration and neutrality and argue for a robust conception of liberty. Waldron defends the idea that people have a right to act in ways others disapprove of, and that the state should be neutral vis-á-vis (...) religious and ethical systems. The chapters that follow are concerned with socio-economic rights. Waldron argues that poverty and homelessness are not to be understood apart from the value of freedom. On the contrary our moral response to them should be based on the same values that underlie traditional liberal philosophy. (shrink)

In this paper, I compare two prominent positions within contemporary “Analytic” and “Continental” political philosophy: philosophical anarchism and the paradox of politics. I compare each through an analysis of their respective criticisms of state legitimacy and the internal difficulties each position has in accounting for the legitimacy of state violence. I argue that these internal difficulties force each position to ask questions and criticize assumptions commonly found in the other position. I hope to show through this comparison that work across (...) the analytic/continental divide can tell us a great deal about a range of intractable political phenomena. (shrink)

According to Michael Friedman, Ernst Cassirer’s “outstanding contribution [to Neo-Kantianism] was to articulate, for the first time, a clear and coherent conception of formal logic within the context of the Marburg School” (Friedman 2000, p. 30). In his paper “Kant und die moderne Mathematik” (1907), Cassirer argued not only that the new relational logic of Frege1 and Russell was a major breakthrough with profound philosophical implications, but also that the logicist thesis itself was a “fact” of modern mathematics. Cassirer summarizes (...) his evaluation of Russell’s work: Here logic and mathematics have been fused into a true, henceforth indissoluble unity; and from this inner connection there arises for each... (shrink)

For a quarter of a century, the Council for Responsible Genetics has provided a unique historical lens into the modern history, science, ethics, and politics of genetic technologies. Since 1983 the Council has had leading scientists, activists, science writers, and public health advocates researching and reporting on a broad spectrum of issues, including genetically engineered foods, biological weapons, genetic privacy and discrimination, reproductive technologies, and human cloning. Biotechnology in Our Lives examines how these issues affect us daily whether we realize (...) it or not. Written for the nonscientist, it looks at the many applications of genetics on the world around us by posing questions such as: What should we know about genetics and childbirth? Can our genes keep us from qualifying for health insurance? Can gene therapy cure cancer? Is behavior genetically determined? Why would the FBI want our genes? Are foreign genes in our food? And much more Ultimately, this definitive book on the subject also encourages us to think about the social, environmental, and moral ramifications of where this technology is taking us. (shrink)

This paper gives a contextualized reading of Kant's theory of real definitions in geometry. Though Leibniz, Wolff, Lambert and Kant all believe that definitions in geometry must be ‘real’, they disagree about what a real definition is. These disagreements are made vivid by looking at two of Euclid's definitions. I argue that Kant accepted Euclid's definition of circle and rejected his definition of parallel lines because his conception of mathematics placed uniquely stringent requirements on real definitions in geometry. Leibniz, Wolff (...) and Lambert thus accept definitions that Kant rejects because they assign weaker roles to real definitions. (shrink)

We use model-theoretic methods described in [3] to obtain ordinal analyses of a number of theories of first- and second-order arithmetic, whose proof-theoretic ordinals are less than or equal to Γ0.

In the ‘analytic tradition’, Hans Sluga wrote thirty years ago in his book Gottlob Frege, there has been a ‘lack of interest in historical questions — even in the question of its own roots. Anti-historicism has been the baggage of the tradition since Frege’ (Sluga, 1980, p. 2). The state of the discussion of Frege among analytic philosophers, Sluga claimed, illustrated well this indifference. Despite the numbers of pages devoted to Frege, there was still, Sluga claimed, little understanding of the (...) sources of Frege’s ideas, his intellectual debts, and the historical circumstances of his thought. Sluga singled out Michael Dummett’s Frege: Philosophy of Language ‘as a paradigm for the failure of analytic philosophers to come to grips with the actual, historical Frege’. In that book, Dummett famously wrote that the logical system that Frege put forward in his 1879 Begriffsschrift ‘is astonishing because it has no predecessors: it appears to have been born from Frege’s brain unfertilized by external influences’ (Dummett, 1981a, p. xxxv) — and Dummett devoted almost none of its 700 pages to the relationship between Frege and his contemporaries. (shrink)

Using a social exchange perspective of narcissism as the foundation for study hypotheses, this study explored the relationship between leaders’ narcissism and the well-being of both leaders and subordinates at the individual and group levels. Results from a sample of 1017 subordinates working under 424 leaders generally support the hypothesized models finding leaders’ narcissism negatively relates to leader-member exchange, and that LMX subsequently relates to subordinates’ job satisfaction and emotional exhaustion. At the group level, leaders’ narcissism also negatively relates to (...) three forms of leaders’ personal well-being but these relationships go through average LMX. Elaboration on theoretical and empirical implications for business ethics is offered to provide a clearer direction for future research in this area. (shrink)

Definitions and distinctions -- Classification -- Of the ends of punishment -- Cases unmeet for punishment -- Expense of punishment -- Measure of punishment -- Of the properties to be given to a lot of punishment -- Of analogy between crimes and punishment -- Of retaliation -- Popularity -- Simple afflictive punishments -- Of complex afflictive punishments -- Of restrictive punishments--territorial confinement -- Imprisonment -- Imprisonment--fees -- Imprisonment examined -- General scheme of imprisonment -- Of other species of territorial confinement--quasi-imprisonment--relegation--banishment (...) -- Of simply restrictive punishments -- Of active or laborious punishment -- Capital punishment -- Capital punishment examined -- Punishment analyzed -- Of the punishments belonging to the moral sanction -- Forfeiture of reputation -- Of pecuniary forfeitures -- Forfeiture of condition -- Forfeiture of the protection of the law -- Naturally extravasting punishment--rules concerning it -- Punishment apparently, but not really, mis-seated--civil responsibility -- Mis-seated punishment, varieties of -- Vicarious punishment -- Transitive punishment -- Disadvantages of this mode of punishment -- Collective punishment -- Random punishment -- Cause of the frequency of mis-seated punishment -- Inconveniences of complex punishments -- Of transportation -- Panopticon penitentiary -- Felony -- Of præmunire -- Outlawry -- Excommunication -- Choice of punishment--latitude to be allowed to the judges -- Of subsidiary punishments -- Of surety for good conduct -- Defeazance of punishment. (shrink)

If unremunerated blood donors are willing to participate, and if the use of them is economical from the perspective of those collecting blood, I can see no objection to their use. But there seems to me no good reason, moral or practical, why they should be used. The system of paid plasmapheresis as it currently operates in the United States and in Canada would seem perfectly adequate, and while there may always be ways in which the safety and efficiency of (...) supply could be increased, there seems no reason whatever to think that there would be an improvement if the current system changed so as to rely entirely on unpaid donors. Further, given the adequacy of paid plasmapheresis, I could see no problem if the collection of whole blood were to take place on a similar, fully-commercial, basis. Such a view is controversial. To argue for it, this paper offers just one strand in a complex argument: a critique of Richard Titmuss’s Gift Relationship, which holds an iconic position in the critical literature on the paid provision of blood. As I conclude: all told, there seems no good basis for rejecting supply of whole blood for money—let alone the supply of blood plasma. (shrink)

Decision-making capacity (DMC) is, in many ways, a central organizing concept of modern health care ethics. Patients with DMC have the moral—if not always the legal—authority to make all manner of...

Scholars have wrestled with "consciousness", a major scholar calling it the "hard problem". Some thirty-plus years after the Towards a Science of Consciousness, we do not seem to be any closer to an answer to "What is consciousness?". Seemingly irresolvable metaphysical problems are addressed by bootstrapping, provisional assumptions, not unlike those used by logicians and mathematicians. I bootstrap with the same ontology and epistemology applicable to everything we apprehend. Here, I argue for a version of the unity of opposites, a (...) form of neutral monism. Something exists because of what it is not; nothing can exist by itself, singularities (analogous to monads), expressing the model. Applying this most fundamental law to the consciousness problem, the physical (movement) comes into being simultaneously as the mental (stasis), each displayed by a field that is variegated (ranging from creative to entropic processes). Such is in keeping with how the singularity emerged as our universe, the same form that may account for sub-Planck-scale phenomena. Overall, like the most fundamental law, deep structures are imminent in our universe, both as objects and processes. (shrink)

It is now standard to interpret Aquinas as recognizing two main types of material objects: substances and artifacts, where substances are those material objects that result from some particular substantial form inhering in prime matter, and artifacts are those material objects that result from some particular accidental form inhering in one or more material substances. There are two problems with this standard interpretation. First, there are passages in which Aquinas states that accidental forms should be understood not as inhering in (...) substances from the outside, but as entering into their composition so as to be included among their metaphysical parts. Second, there are passages in which Aquinas states that it is impossible for any accidental form to be shared by two or more substances. This article considers what implications these two observations might have for how we understand the metaphysical structure of artifacts in Aquinas’s ontology. (shrink)

The distinction between analytic and continental philosophy is not a philosophical distinction. It is a sociological one, incorporating political and psychological dimensions. I shall argue that this distinction is a symptom of, most relevantly, professionalization, and that professionalization excludes philosophy. As a result, the only philosophically meaningful consequence that the analytic/continental distinction has is to alert us by conceptual contrast to what it is that we should concern ourselves with instead. This alternative focus is the a-professional contexts and features of (...) actual philosophy. The analytic/continental distinction usefully points us to these as that to which the specific structure and disciplinary effects of this distinction are entirely irrelevant. (shrink)

The American Journal of Bioethics, Volume 12, Issue 3, Page 33-34, March 2012.

The standard conception of misleading evidence has it that e is misleading evidence that p iff e is evidence that p and p is false. I argue that this conception yields incorrect verdicts when we consider what it is for evidence to be misleading with respect to questions like whether p. Instead, we should adopt a conception of misleading evidence according to which e is misleading with respect to a question only if e is in-fact irrelevant to that question – (...) a relation that requires that e fail to be both explanatorily connected to and evidence for any truth that answers the question. This modified conception allows e to be non-misleading evidence with respect to a question even if e is evidence for the false answer to that question. It also points toward a new argument for and explanation of the truth of a central premise – what Maria Lasonen-Aarnio dubs “Entitlement” – that generates the infamous dogmatism puzzle. (shrink)

I take issue with Bernard Gert’s interpretation of Hobbes on two main points. First, I argue that Hobbes’s moral theory reduces to a sophisticated form of consequentialism. Second, I argue that Hobbes’s moral theory is more demanding than Gert’s interpretation, and some of Hobbes’s own remarks, make it appear. I focus on Gert’s reading of Hobbes’s second law of nature, and argue that the law presents us with a Hobson’s choice—that is, the appearance of a choice of how much liberty (...) to relinquish when really there is none. (shrink)

Given a convergence theorem in analysis, under very general conditions a model-theoretic compactness argument implies that there is a uniform bound on the rate of metastability. We illustrate with three examples from ergodic theory.

The dominated convergence theorem implies that if is a sequence of functions on a probability space taking values in the interval [0, 1], and converges pointwise a.e., then converges to the integral of the pointwise limit. Tao [26] has proved a quantitative version of this theorem: given a uniform bound on the rates of metastable convergence in the hypothesis, there is a bound on the rate of metastable convergence in the conclusion that is independent of the sequence and the underlying (...) space. We prove a slight strengthening of Tao’s theorem which, moreover, provides an explicit description of the second bound in terms of the first. Specifically, we show that when the first bound is given by a continuous functional, the bound in the conclusion can be computed by a recursion along the tree of unsecured sequences. We also establish a quantitative version of Egorov’s theorem, and introduce a new mode of convergence related to these notions. (shrink)

From ancient times to the beginning of the nineteenth century, mathematics was commonly viewed as the general science of quantity, with two main branches: geometry, which deals with continuous quantities, and arithmetic, which deals with quantities that are discrete. Mathematical logic does not fit neatly into this taxonomy. In 1847, George Boole [1] offered an alternative characterization of the subject in order to make room for this new discipline: mathematics should be understood to include the use of any symbolic calculus (...) “whose laws of combination are known and general, and whose results admit of a consistent interpretation.” Depending on the laws chosen, symbols can just as well be used to represent propositions instead of quantities; in that way, one can consider calculations with propositions on par with more familiar arithmetic calculations. Despite Boole’s efforts, logic has always held an uncertain place in the mathematical community. This can partially be attributed to its youth; while number theory and geometry have their origins in antiquity, mathematical logic did not emerge as a recognizable discipline until the latter half of the nineteenth century, and so lacks the provenance and prestige of its elder companions. Furthermore, the nature of the subject matter serves to set it apart; as objects of mathematical study, formulas and proofs do not have the same character as groups, topological spaces, and measures. Even distinctly mathematical branches of contemporary logic, like model theory and set theory, tend to employ linguistic classifications and measures of complexity that are alien to other mathematical disciplines. The Birth of Model Theory, by Calixto Badesa, describes a seminal step in the emergence of logic as a mature mathematical discipline. As its title suggests, the focus is on one particular result, now referred to as the L¨owenheim-Skolem theorem, as presented in a paper by L¨owenheim in 1915. But the book is, more broadly, about the story of the logic community’s gradual coming to the modern distinction between syntax and semantics, that is, between systems of symbolic expressions and the meanings that can be assigned to them.. (shrink)

Every branch of mathematics has its subject matter, and one of the distinguishing features of logic is that so many of its fundamental objects of study are rooted in language. The subject deals with terms, expressions, formulas, theorems, and proofs. When we speak about these notions informally, we are talking about things that can be written down and communicated with symbols. One of the goals of mathematical logic is to introduce formal definitions that capture our intuitions about such objects and (...) enable us to reason about them precisely. At the most basic level, syntactic objects can be viewed as strings of symbols. For concreteness, we can identify symbols with particular set-theoretic objects, but for most purposes, it doesn't matter what they are; all that is needed is that they are distinct from one another. (shrink)

On September 6, 2004, using the Isabelle proof assistant, I verified the following statement: (%x. pi x * ln (real x) / (real x)) ----> 1 The system thereby confirmed that the prime number theorem is a consequence of the axioms of higher-order logic together with an axiom asserting the existence of an infinite set. All told, our number theory session, including the proof of the prime number theorem and supporting libraries, constitutes 673 pages of proof scripts, or roughly 30,000 (...) lines. This count includes about 65 pages of elementary number theory that we had at the outset, developed by Larry Paulson and others; also about 50 pages devoted to a proof of the law of quadratic reciprocity and properties of Euler’s ϕ function, neither of which are used in the proof of the prime number theorem. The page count does not include the basic HOL library, or properties of the real numbers that we obtained from the HOL-Complex library. (shrink)

Hilbert’s program: • Formalize abstract, infinitary, nonconstructive mathematics. • Prove consistency using only finitary methods.

In the theory of programming languages, type inference is the process of inferring the type of an expression automatically, often making use of information from the context in which the expression appears. Such mechanisms turn out to be extremely useful in the practice of interactive theorem proving, whereby users interact with a computational proof assistant to constructformal axiomatic derivations of mathematical theorems. This article explains some of the mechanisms for type inference used by the "Mathematical Components" project, which is working (...) towards a verification of the Feit-Thompson theorem. (shrink)