Though Frege was interested primarily in reducing mathematics to logic, he succeeded in reducing an important part of logic to mathematics by defining relations in terms of functions. By contrast, Whitehead & Russell reduced an important part of mathematics to logic by defining functions in terms of relations (using the definite description operator). We argue that there is a reason to prefer Whitehead & Russell's reduction of functions to relations over Frege's reduction of relations to functions. There is an interesting (...) system having a logic that can be properly characterized in relational but not in functional type theory. This shows that relational type theory is more general than functional type theory. The simplification offered by Church in his functional type theory is an over-simplification: one can't assimilate predication to functional application.<br>. (shrink)

The exploration of metaphysical arguments in the symbolic AI environment provides clarification and raises unexpected questions about notions in philosophy of religion and theology. Recent attempts to apply automatic theorem prover technology to Anselm's ontological argument have led to a simplification of the argument. This computationally discovered simplification has given rise to logical observations. The article assesses one of these observations: the application of the diagonal method (in Cantor's version) to Anselm's argument. The evaluation of the applications of theorem provers (...) to metaphysical and theological arguments contributes to the following topics in philosophy of religion: the limits of natural theology, the relationship between religion and STEM, and theology's scientificity. (shrink)

Interactive theorem provers might seem particularly impractical in the history of philosophy. Journal articles in this discipline are generally not formalized. Interactive theorem provers involve a learning curve for which the payoffs might seem minimal. In this article I argue that interactive theorem provers have already demonstrated their potential as a useful tool for historians of philosophy; I do this by highlighting examples of work where this has already been done. Further, I argue that interactive theorem provers can continue to (...) be useful tools for historians of philosophy in the future; this claim is defended through a more conceptual analysis of what historians of philosophy do that identifies argument reconstruction as a core activity of such practitioners. It is then shown that interactive theorem provers can assist in this core practice by a description of what interactive theorem provers are and can do. If this is right, then computer verification for historians of philosophy is in the offing. (shrink)

(This is for the Cambridge Handbook of Analytic Philosophy, edited by Marcus Rossberg) In this handbook entry, I survey the different ways in which formal mathematical methods have been applied to philosophical questions throughout the history of analytic philosophy. I consider: formalization in symbolic logic, with examples such as Aquinas’ third way and Anselm’s ontological argument; Bayesian confirmation theory, with examples such as the fine-tuning argument for God and the paradox of the ravens; foundations of mathematics, with examples such as (...) Hilbert’s programme and Gödel’s incompleteness theorems; social choice theory, with examples such as Condorcet’s paradox and Arrow’s theorem; ‘how possibly’ results, with examples such as Condorcet’s jury theorem and recent work on intersectionality theory; and the application of advanced mathematics in philosophy, with examples such as accuracy-first epistemology. (shrink)

В монографии представлены несколько смысловых блоков, связанных с восприятием и интерпретацией человеком исторического бытия. Ранние греческие мыслители пытались получить доступ к исходникам (началам) бытия, и эти интенции легли в основу научного знания, а также привели к появлению метафизики. В классической (и в неклассической) метафизике за основу была принята догма Пифагора и Платона о неизменности подлинной реальности, из чего следовало отрицание бытийного характера времени. Автор монографии отказывается от этой догмы и предлагает стратегию обновления метафизики и перехода ее к новому — постнеклассическому (...) — этапу. Поскольку трансформационный потенциал реальности наиболее явно представлен в историческом становлении, авторская стратегия реализуется в метафизике истории. При этом выявляются начала истории, в каком качестве выступают «дух», «культурно-историческая матрица» и «метафизический проект организации бытия» («онтологический проект»). Исследуются формы и механизмы «работы» человека с прошлым, обсуждаются вопросы, связанные с постижением логики исторического процесса, а также с ролью (творческой) личности в истории. Анализируются причины цивилизационных кризисов и очерчиваются возможные пути их разрешения, предлагается метафизическая интерпретация социальных и военных конфликтов. Завершает исследование рассмотрение трансформации человеческого естества под влиянием информационных, био- и нанотехнологий. (shrink)

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)

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)

The authors investigated the ontological argument computationally. The premises and conclusion of the argument are represented in the syntax understood by the automated reasoning engine PROVER9. Using the logic of definite descriptions, the authors developed a valid representation of the argument that required three non-logical premises. PROVER9, however, discovered a simpler valid argument for God's existence from a single non-logical premise. Reducing the argument to one non-logical premise brings the investigation of the soundness of the argument into better focus. Also, (...) the simpler representation of the argument brings out clearly how the ontological argument constitutes an early example of a ?diagonal argument? and, moreover, one used to establish a positive conclusion rather than a paradox. (shrink)

Computational philosophy is the use of mechanized computational techniques to instantiate, extend, and amplify philosophical research. Computational philosophy is not philosophy of computers or computational techniques; it is rather philosophy using computers and computational techniques. The idea is simply to apply advances in computer technology and techniques to advance discovery, exploration and argument within any philosophical area. -/- After touching on historical precursors, this article discusses contemporary computational philosophy across a variety of fields: epistemology, metaphysics, philosophy of science, ethics and (...) social philosophy, philosophy of language and philosophy of mind, often with examples of operating software. Far short of any attempt at an exhaustive treatment, the intention is to introduce the spirit of each application by using some representative examples. (shrink)

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)

Scientific research in the formal sciences comes in multiple degrees of formality: fully formal work; rigorous proofs that practitioners know to be formalizable in principle; and informal work like rough proof sketches and considerations about the advantages and disadvantages of various formal systems. This informal work includes informal and semi-formal debates between formal scientists, e.g. about the acceptability of foundational principles and proposed axiomatizations. In this paper, we propose to use the methodology of structured argumentation theory to produce a formal (...) model of such informal and semi-formal debates in the formal sciences. For this purpose, we propose ASPIC-END, an adaptation of the structured argumentation framework ASPIC+ which can incorporate natural deduction style arguments and explanations. We illustrate the applicability of the framework to debates in the formal sciences by presenting a simple model of some arguments about proposed solutions to the Liar paradox, and by discussing a more extensive—but still preliminary—model of parts of the debate that mathematicians had about the Axiom of Choice in the early twentieth century. (shrink)

Because the label "computing and philosophy" can seem like an ad hoc attempt to tie computing to philosophy, it is important to explain why it is not, what it studies (or does) and how it differs from research in, say, "computing and history," or "computing and biology". The American Association for History and Computing is "dedicated to the reasonable and productive marriage of history and computer technology for teaching, researching and representing history through scholarship and public history" (http://theaahc.org). More pervasive, (...) work in computing and biology enjoys the convenient name of "bioinformatics...the science of using information to understand biology..., a subset of the larger field of computational biology, the application of quantitative analytical techniques in modeling biological systems" (http://oreilly.com/catalog/bioskills/chapter/ ch01.html). The recent venture of the Association for Computing Machinery and the Institute of Electrical and Electronics Engineers to publish the Transactions on Computational Biology and Bioinformatics (TCBB) bears witness to the reach of computing and biology and underscores its objective. TCBB intends to report "archival research results related to the algorithmic, mathematical, statistical, and computational methods that are central in bioinformatics and computational biology; the development and testing of effective computer programs in bioinformatics; the development and optimization of biological databases; and important biological results that are obtained from the use of these methods, programs, and databases" (http://tcbb.acm.org). In the case of "computing and history" and "bioinformatics," each discipline stands in a particular relationship to computers that raises questions unique to itself. But both are devoted to the development of computational tools to aid discovery.. (shrink)

A shallow semantic embedding of an intensional higher-order modal logic in Isabelle/HOL is presented. IHOML draws on Montague/Gallin intensional logics and has been introduced by Melvin Fitting in his textbook Types, Tableaus and Gödel’s God in order to discuss his emendation of Gödel’s ontological argument for the existence of God. Utilizing IHOML, the most interesting parts of Fitting’s textbook are formalized, automated and verified in the Isabelle/HOL proof assistant. A particular focus thereby is on three variants of the ontological argument (...) which avoid the modal collapse, which is a strongly criticized side-effect in Gödel’s resp. Scott’s original work. (shrink)