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)

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

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)

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)

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)

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)

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)