Our computational metaphysics group describes its use of automated reasoning tools to study Leibniz’s theory of concepts. We start with a reconstruction of Leibniz’s theory within the theory of abstract objects (henceforth ‘object theory’). Leibniz’s theory of concepts, under this reconstruction, has a non-modal algebra of concepts, a concept-containment theory of truth, and a modal metaphysics of complete individual concepts. We show how the object-theoretic reconstruction of these components of Leibniz’s theory can be represented for investigation by means of automated (...) theorem provers and finite model builders. The fundamental theorem of Leibniz’s theory is derived using these tools. (shrink)

Alan Gewirth’s claim that agents contradict that they are agents if they do not accept that the principle of generic consistency (PGC) is the supreme principle of practical rationality has been greeted with widespread scepticism. The aim of this article is not to defend this claim but to show that if the first and least controversial of the three stages of Gewirth’s argument for the PGC is sound, then agents must interpret and give effect to human rights in ways consistent (...) with the PGC, or deny that human beings are equal in dignity and rights (which idea defines human rights) or that they are agents (and hence subject to any rules at all). Implications for the interpretation of the international legal system of human rights inspired by the Universal Declaration of Human Rights 1948 are sketched. (shrink)

In this paper, the authors describe their initial investigations in computational metaphysics. Our method is to implement axiomatic metaphysics in an automated reasoning system. In this paper, we describe what we have discovered when the theory of abstract objects is implemented in PROVER9 (a first-order automated reasoning system which is the successor to OTTER). After reviewing the second-order, axiomatic theory of abstract objects, we show (1) how to represent a fragment of that theory in PROVER9's first-order syntax, and (2) how (...) PROVER9 then finds proofs of interesting theorems of metaphysics, such as that every possible world is maximal. We conclude the paper by discussing some issues for further research. (shrink)

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

It has been argued that ethically correct robots should be able to reason about right and wrong. In order to do so, they must have a set of do’s and don’ts at their disposal. However, such a list may be inconsistent, incomplete or otherwise unsatisfactory, depending on the reasoning principles that one employs. For this reason, it might be desirable if robots were to some extent able to reason about their own reasoning—in other words, if they had some meta-ethical capacities. (...) In this paper, we sketch how one might go about designing robots that have such capacities. We show that the field of computational meta-ethics can profit from the same tools as have been used in computational metaphysics. (shrink)

Sections 1 through 3 present all of the main ideas behind the probabilistic logic of evidential support. For most readers these three sections will suffice to provide an adequate understanding of the subject. Those readers who want to know more about how the logic applies when the implications of hypotheses about evidence claims (called likelihoods) are vague or imprecise may, after reading sections 1-3, skip to section 6. Sections 4 and 5 are for the more advanced reader who wants a (...) detailed understanding of some telling results about how this logic may bring about convergence to the truth. (shrink)

"Most modern philosophers attempt to solve the problem of morality from within the epistemological assumptions that define the dominant cultural perspective of our age. Alan Gewirth's Reason and Morality is a major work in this ongoing enterprise. Gewirth develops, with patience and skill, what he calls a 'modified naturalism' in which morality is derived by logic alone from the concept of action.... I think that the publication of Reason and Morality is a major event in the history of moral philosophy. (...) It develops with great power a new and exciting position in ethical naturalism. No one, regardless of philosophical stance, can read this work without an enlargement of mind. It illuminates morality and agency for all."—E. M. Adams, The Review of Metaphysics "This is a fascinating study of an apparently intractable problem. Gewirth has provided plenty of material for further discussion, and his theory deserves serious consideration. He is always aware of possible rejoinders and argues in a rigorous manner, showing a firm grasp of the current state of moral and political philosophy."—Mind. (shrink)

This entry traces the historical development of the Square of Opposition, a collection of logical relationships traditionally embodied in a square diagram. This body of doctrine provided a foundation for work in logic for over two millenia. For most of this history, logicians assumed that negative particular propositions ("Some S is not P") are vacuously true if their subjects are empty. This validates the logical laws embodied in the diagram, and preserves the doctrine against modern criticisms. Certain additional principles ("contraposition" (...) and "obversion") were sometimes adopted along with the Square, and they genuinely yielded inconsistency. By the nineteenth century an inconsistent set of doctrines was widely adopted. Strawson's 1952 attempt to rehabilitate the Square does not apply to the traditional doctrine; it does salvage the nineteenth century version but at the cost of yielding inferences that lead from truth to falsity when strung together. (shrink)

Critique of Computationalism as merely projecting hermeneutics (i.e., meaning originating from the mind of an external interpreter) onto otherwise intrinsically meaningless symbols.

Computational philosophy is the use of mechanized computational techniques to unearth philosophical insights that are either difficult or impossible to find using traditional philosophical methods. Computational metaphysics is computational philosophy with a focus on metaphysics. In this paper, we (a) develop results in modal metaphysics whose discovery was computer assisted, and (b) conclude that these results work not only to the obvious benefit of philosophy but also, less obviously, to the benefit of computer science, since the new computational techniques that (...) led to these results may be more broadly applicable within computer science. The paper includes a description of our background methodology and how it evolved, and a discussion of our new results. (shrink)

An ambitious ethical theory ---Alan Gewirth's "Principle of Generic Consistency"--- is encoded and analysed in Isabelle/HOL. Gewirth's theory has stirred much attention in philosophy and ethics and has been proposed as a potential means to bound the impact of artificial general intelligence.

Alan Gewirth's _Reason and Morality_, in which he set forth the Principle of Generic Consistency, is a major work of modern ethical theory that, though much debated and highly respected, has yet to gain full acceptance. Deryck Beyleveld contends that this resistance stems from misunderstanding of the method and logical operations of Gewirth's central argument. In this book Beyleveld seeks to remedy this deficiency. His rigorous reconstruction of Gewirth's argument gives its various parts their most compelling formulation and clarifies its (...) essential logical structure. Beyleveld then classifies all the criticisms that Gewirth's argument has received and measures them against his reconstruction of the argument. The overall result is an immensely rich picture of the argument, in which all of its complex issues and key moves are clearly displayed and its validity can finally be discerned. The comprehensiveness of Beyleveld's treatment provides ready access to the entire debate surrounding the foundational argument of _Reason and Morality_. It will be required reading for all who are interested in Gewirth's theory and deontological ethics and will be of central importance to moral and legal theorists. (shrink)

A 'self-refutation argument' is any argument which aims at showing that a certain thesis is self-refuting. This study was the first book-length treatment of ancient self-refutation and provides a unified account of what is distinctive in the ancient approach to the self-refutation argument, on the basis of close philological, logical and historical analysis of a variety of sources. It examines the logic, force and prospects of this original style of argumentation within the context of ancient philosophical debates, dispelling various misconceptions (...) concerning its nature and purpose and elucidating some important differences which exist both within the ancient approach to self-refutation and between that approach, as a whole, and some modern counterparts of it. In providing a comprehensive account of ancient self-refutation, the book advances our understanding of influential and debated texts and arguments from philosophers like Democritus, Plato, Aristotle, Epicurus, the Stoics, the Academic sceptics, the Pyrrhonists and Augustine. (shrink)

Rarely has the history or philosophy of mathematics been written about by mathematicians, and the analysis of mathematical texts themselves has been an area almost entirely unexplored. _Figures of Thought_ looks at ways in which mathematical works can be read as texts, examines their textual strategies and demonstrates that such readings provide a rich source of philosophical issues regarding mathematics: issues which traditional approaches to the history and philosophy of mathematics have neglected. David Reed, a professional mathematician himself, offers the (...) first sustained and critical attempt to find a consistent argument or narrative thread in mathematical texts. In doing so he develops new and fascinating interpretations of mathematicians' work throughout history, from an in-depth analysis of Euclid's Elements, to the mathematics of Descartes and right up to the work of contemporary mathematicians such as Grothendeick. He also traces the implications of this approach to the understanding of the history and development of mathematics. (shrink)

We describe some of the ways that the field of content analysis is being transformed in an Era of Big Data. We argue that content analysis, from its beginning, has been concerned with extracting the main meanings of a text and mapping those meanings onto the space of a textual corpus. In contrast, we suggest that the emergence of new styles of text mining tools is creating an opportunity to develop a different kind of content analysis that we describe as (...) a computational hermeneutics. Here the goal is to go beyond a mapping of the main meaning of a text to mimic the kinds of questions and concerns that have traditionally been the focus of a hermeneutically grounded close reading, a reading that focuses on what Kenneth Burke described as the poetic meanings of a text. We illustrate this approach by referring to our own work concerning the rhetorical character of US National Security Strategy documents. (shrink)

Principia Logico-Metaphysica contains a foundational logical theory for metaphysics, mathematics, and the sciences. It includes a canonical development of Abstract Object Theory [AOT], a metaphysical theory that distinguishes between ordinary and abstract objects. This article reports on recent work in which AOT has been successfully represented and partly automated in the proof assistant system Isabelle/HOL. Initial experiments within this framework reveal a crucial but overlooked fact: a deeply-rooted and known paradox is reintroduced in AOT when the logic of complex terms (...) is simply adjoined to AOT’s specially formulated comprehension principle for relations. This result constitutes a new and important paradox, given how much expressive and analytic power is contributed by having the two kinds of complex terms in the system. Its discovery is the highlight of our joint project and provides strong evidence for a new kind of scientific practice in philosophy, namely, computational metaphysics. Our results were made technically possible by a suitable adaptation of Benzmüller’s metalogical approach to universal reasoning by semantically embedding theories in classical higher-order logic. This approach enables one to reuse state-of-the-art higher-order proof assistants, such as Isabelle/HOL, for mechanizing and experimentally exploring challenging logics and theories such as AOT. Our results also provide a fresh perspective on the question of whether relational type theory or functional type theory better serves as a foundation for logic and metaphysics. (shrink)

We present a computer-supported approach for the logical analysis and conceptual explicitation of argumentative discourse. Computational hermeneutics harnesses recent progresses in automated reasoning for higher-order logics and aims at formalizing natural-language argumentative discourse using flexible combinations of expressive non-classical logics. In doing so, it allows us to render explicit the tacit conceptualizations implicit in argumentative discursive practices. Our approach operates on networks of structured arguments and is iterative and two-layered. At one layer we search for logically correct formalizations for each (...) of the individual arguments. At the next layer we select among those correct formalizations the ones which honor the argument’s dialectic role, i.e. attacking or supporting other arguments as intended. We operate at these two layers in parallel and continuously rate sentences’ formalizations by using, primarily, inferential adequacy criteria. An interpretive, logical theory will thus gradually evolve. This theory is composed of meaning postulates serving as explications for concepts playing a role in the analyzed arguments. Such a recursive, iterative approach to interpretation does justice to the inherent circularity of understanding: the whole is understood compositionally on the basis of its parts, while each part is understood only in the context of the whole. We summarily discuss previous work on exemplary applications of human-in-the-loop computational hermeneutics in metaphysical discourse. We also discuss some of the main challenges involved in fully-automating our approach. By sketching some design ideas and reviewing relevant technologies, we argue for the technological feasibility of a highly-automated computational hermeneutics. (shrink)

Figures of Thought looks at how mathematical works can be read as texts and examines their textual strategies. David Reed offers the first sustained and critical attempt to find a consistent argument or narrative thread in mathematical texts. Reed selects mathematicians from a range of historical periods and compares their approaches to organizing and arguing texts, using an extended commentary on Euclid's Elements as a central structuring framework. He develops fascinating interpretations of mathematicians' work throughout history, from Descartes to Hilbert, (...) Kronecker, Dedekind, Weil and Grothendieck. Reed traces the implications of this approach to the understanding of the history and development of mathematics. (shrink)

Principia Logico-Metaphysica contains a foundational logical theory for metaphysics, mathematics, and the sciences. It includes a canonical development of Abstract Object Theory [AOT], a metaphysical theory that distinguishes between ordinary and abstract objects.This article reports on recent work in which AOT has been successfully represented and partly automated in the proof assistant system Isabelle/HOL. Initial experiments within this framework reveal a crucial but overlooked fact: a deeply-rooted and known paradox is reintroduced in AOT when the logic of complex terms is (...) simply adjoined to AOT’s specially formulated comprehension principle for relations. This result constitutes a new and important paradox, given how much expressive and analytic power is contributed by having the two kinds of complex terms in the system. Its discovery is the highlight of our joint project and provides strong evidence for a new kind of scientific practice in philosophy, namely, computational metaphysics.Our results were made technically possible by a suitable adaptation of Benzmüller’s metalogical approach to universal reasoning by semantically embedding theories in classical higher-order logic. This approach enables one to reuse state-of-the-art higher-order proof assistants, such as Isabelle/HOL, for mechanizing and experimentally exploring challenging logics and theories such as AOT. Our results also provide a fresh perspective on the question of whether relational type theory or functional type theory better serves as a foundation for logic and metaphysics. (shrink)

This is an English translation of Plato presenting a new conception of the Theory of Forms. Socrates and others discuss the epistemological and metaphysical puzzles of the Parmenides, with aims to define the meaning of the Sophist. The glossary of key terms is a unique addition to Platonic literature by which concepts central to each dialogue are discussed and cross-referenced as to their occurrences throughout the work. In such a way students are encouraged to see beyond the words into concepts. (...) Focus Philosophical Library translations are close to and are non-interpretative of the original text, with the notes and a glossary intending to provide the reader with some sense of the terms and the concepts as they were understood by Plato’s immediate audience. (shrink)

English. This paper analyses two closely related but different concepts, digitization and digitalization, first discussed in an encyclopedia article by Brennen and Kreiss in 2016. Digital Humanities mainly uses the first term, whereas business and economics tend to use the second to praise the process of the digitalization of society. But digitalization was coined as a critical concept in 1971 by Wachal and is sometimes used in post-colonial studies. Consequently, humanist scholars are invited to avoid the "path of least resistance" (...) when using digitalization, and to explore its critical potential. The paper concludes by considering the effect of the digitalization perspective and by expressing author's point of view on the issue. Italiano. Questo articolo analizza due concetti correlati ma differenti fra loro, "digitization" e "digitalization", discussi la prima volta in una voce di enciclopedia da Brennen e Kreiss nel 2016. Nelle scienze umane digitali si utilizza sostanzialmente il primo termine, mentre in economia si tende a utilizzare il secondo per sottolineare il processo di digitalizzazione della società. Ma il termine "digitalization" era stato creato nel 1971 da Wachal come un concetto critico, ed era stato utilizzato in alcuni studi sul post-colonialismo. Di conseguenza, gli studiosi nelle scienze umane sono invitati a evitare di utilizzare "digitalization" in modo triviale, e ad esplorare il suo potenziale critico. L'articolo termina con alcune considerazioni sugli effetti della prospettiva della digitalizzazione, presentando il punto di vista dell'autore. (shrink)