The Computational Theory of Possible Worlds

In this project, we used PROVER9 to prove the fundamental theorems of possible worlds theory, as developed in the paper by E. Zalta, ‘25 Basic Theorems in Situation and World Theory’ (in PDF). These are laid out in detail in the corresponding sections below.

The Tools You Will Need

We have proved all of the theorems below using the June2006B version of Prover9. However, we have also redeveloped almost all of the theorems for later versions of Prover9. The later versions of Prover9 don't require special commands at the top of the file (e.g., they don't require a "set(auto)." line at the top of the file).

The links to the input and output files below all assume the June 2006B version of PROVER9 and MACE4. However, newer versions of these files, that work with newer versions of PROVER9, and with the graphical application, can be found here.

So, you can obtain the June 2006B version, and either the later versions or the graphical version, by following one of these links:
Tools You Will Need/June2006B
Tools You Will Need/VersionsAfter June 2006B
Tools You Will Need/Graphical Application

The Theorems for the Theory of Possible Worlds

In this section, we prove the theorems found in E. Zalta, ‘25 Basic Theorems in Situation and World Theory’, published in the Journal of Philosophical Logic, 22 (1993): 385–428.[1] The following definitions are fully motivated and explained in that paper:

Situation(x) = A!x & ∀F(xF → ∃p(F=[λzp]))

p is true in situation s ("s ⊨ p") = szp]

x is a part of y ("x ⊴y") = ∀F(xFyF)

Persistent(p) = ∀s[s ⊨ p → ∀s′(ss′ → s′ ⊨ p)].

Actual(s) = ∀p(s ⊨ pp)     (i.e., s is actual iff every proposition true in s is true)

World(s) = Situation(x) & ◊∀p(s ⊨ pp)

Maximal1(s) = ∀p(s ⊨ ps ⊨ ¬p)

Partial1(s) = ∃p(sp & s⊭¬p)

Maximal2(s) = ∀p(s ⊨ p)

Partial2(s) = ∃p(sp)

Possible(s) = ◊Actual(s)

Consistent(s) = ¬∃p(s ⊨ p & s ⊨ ¬p)
[Note: The definition of consistency used here differs slightly from that in Zalta 1993.]

In terms of these definitions, we can now prove the following theorems in PROVER9. The reader should examine how the representations in second-order logic are translated into PROVER9's first-order syntax.


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.