The Computational Theory of Possible Worlds

WARNING: With the exception of Theorems 12 and 18b, the following input files (linked in below) lead to proofs of our theorems in newer versions of Prover9. We have tested the June2007 version, the 2008-09A version, and the graphical application v0.5B (which invokes the Dec 2007 version). Theorems 12 and 18b, however, do not yield proofs in the time and given the memory we allotted for the search. It may be that if the search is run for greater lengths of time or with more memory allocated, proofs will be found.

The theorems below are reported in E. Zalta, ‘25 Basic Theorems in Situation and World Theory’, published in the Journal of Philosophical Logic, 22 (1993): 385–428.[1] These theorems require certain definitions in object theory which are fully motivated and explained in that paper. We give the list of these definitions on the webpage one level up, where we offer input/output files for the June 2006B version of Prover9. The following input/output files, however, were simplified for use with later versions of Prover9. We have tested them on the June 2007 version, version 0.5B of the graphical application (which uses the Dec 2007 version of Prover9), and with the 2008-09A version of PROVER9. At present, however, we can't confirm that these later versions of Prover9 lead to proofs of Theorems 12 and 18b.


1. Note for purposes of correlating terminology: In what follows, we use the term “proposition’ instead of the term “state of affairs” (the latter was used in Zalta 1993) and we talk in terms of the truth of a proposition, instead talking in terms of a state of affairs obtaining. Similarly, we will speak of propositions being “true in” situations, instead of states of affairs being “factual” in situations.