In our contribution to this special issue on thought experiments and mathematics, we aim to insert theology into the conversation. There is a very long tradition of substantial inquiries into the relationship between theology and mathematics. Platonism has been provoking a consolidation of that tradition to some extent in recent decades. Accordingly, in this paper we look at James R. Brown’s Platonic account of thought experiments. Ultimately, we offer an analysis of some of the merits and perils inherent in framing (...) the use of thought experiments in mathematics and theology in terms of Platonism. (shrink)

Khemlani et al. (2018) mischaracterize logic in the course of seeking to show that mental model theory (MMT) can accommodate a form of inference (, let us label it) they find in a high percentage of their subjects. We reveal their mischaracterization and, in so doing, lay a landscape for future modeling by cognitive scientists who may wonder whether human reasoning is consistent with, or perhaps even capturable by, reasoning in a logic or family thereof. Along the way, we note (...) that the properties touted by Khemlani et al. as innovative aspects of MMT‐based modeling (e.g., nonmonotonicity) have for decades been, in logic, acknowledged and rigorously specified by families of (implemented) logics. Khemlani et al. (2018) further declare that is “invalid in any modal logic.” We demonstrate this to be false by our introduction (Appendix A) of a new propositional modal logic (within a family of such logics) in which is provably valid, and by the implementation of this logic. A second appendix, B, partially answers the two‐part question, “What is a formal logic, and what is it for one to capture empirical phenomena?”. (shrink)

The comments accompanying Proposition (Prop.) 11 (“God... necessarily exists”) in Part I of Spinoza’s The Ethics contain sketches of what appear to be at least three more or less distinct ontological arguments. The first of these is problematic even on its own terms. More is true: even the proposition “God exists” (GE), a consequence of Prop. 11, cannot be derived from the definitions and axioms of Part I (the “DAPI”) of The Ethics; thus, Prop. 11 cannot be derived from the (...) DAPI, either. To prove these claims, I use an automated deduction system (ADS) to show that Prop. 11 is independent of the DAPI. I then augment the DAPI with some auxiliary assumptions I believe Spinoza would accept and that sustain an automated derivation of (GE). The results illustrate how an ADS can facilitate the analysis of arguments and yield an apparently novel argument cast in the style of Spinoza. (shrink)

Oppenheimer & Zalta have re-formulated their non-modal version of the ontological argument, with the help of PROVER9, an automated reasoning engine. The authors end up rejecting the new argument; however, the theist has a rejoinder worth considering. But after presenting the rejoinder, I highlight that the conceivability of the being does not imply its possibility. One lesson is that even non-modal ontological arguments must engage modal matters concerning God. Another lesson is that if PROVER9 is able to derive a conclusion (...) from fewer premises, the proof is sometimes inferior as an argument. (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)

We use a mechanized verification system, PVS, to examine the argument from Anselm’s Proslogion Chapter III, the so-called “Modal Ontological Argument.” We consider several published formalizations for the argument and show they are all essentially similar. Furthermore, we show that the argument is trivial once the modal axioms are taken into account. This work is an illustration of Computational Philiosophy and, in addition, shows how these methods can help detect and rectify errors in modal reasoning.

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)

According to a common view, belief in God cannot be proved and is an issue that must be left to faith. Kant went even further and argued that he can prove this unprovability. But any argument implying that a certain sentence is not provable is challenged by Gödel’s second theorem. Indeed, one trivial consequence of GST is that for any formal system F that satisfies certain conditions and for every sentence K that is formulated in F it is impossible to (...) prove, from F, that K is not provable. In the article, I explore the general issue of proving the unprovability of the existence of God. Of special interest is the question of the relation between the existence of God and the conditions that F must satisfy in order to allow for its subjection to GST. (shrink)

This note discusses P. Oppenheimer and E. Zalta's ?A Computationally-Discovered Simplification of the Ontological Argument? [this journal, 2011]. I try to explain why the simplification presented there was successful and comment on the technical aspects of the method they applied.

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)

A universal reasoning approach based on shallow semantical embeddings of higher-order modal logics into classical higher-order logic is exemplarily employed to analyze several modern variants of the ontological argument on the computer. Several novel findings are reported which contribute to the clarification of a long-standing dispute between Anderson and Hájek. The technology employed in this work, which to some degree realizes Leibniz’s dream of a characteristica universalis and a calculus ratiocinator for solving philosophical controversies, is ready to be fruitfully adopted (...) in larger scale by philosophers. (shrink)

This paper presents detailed formalizations of ontological arguments in a simple modal natural deduction calculus. The first formal proof closely follows the hints in Scott’s manuscript about Gödel’s argument and fills in the gaps, thus verifying its correctness. The second formal proof improves the first one, by relying on the weaker modal logic KB instead of S5 and by avoiding the equality relation. The second proof is also technically shorter than the first one, because it eliminates unnecessary detours and uses (...) Axiom 1 for the positivity of properties only once. The third and fourth proofs formalize, respectively, Anderson’s and Bjørdal’s variants of the ontological argument, which are known to be immune to modal collapse. (shrink)

We investigate incomplete symbols, i.e. definite descriptions with scope-operators. Russell famously introduced definite descriptions by contextual definitions; in this article definite descriptions are introduced by rules in a specific calculus that is very well suited for proof-theoretic investigations. That is to say, the phrase ‘incomplete symbols’ is formally interpreted as to the existence of an elimination procedure. The last section offers semantical tools for interpreting the phrase ‘no meaning in isolation’ in a formal way.