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.

Theorem 01 is a theorem schema and, as such, can't be proved in PROVER9, which is a purely first-order automated reasoner. (Each instance of Theorem 1 can be proved in PROVER9, though.)

Theorem 02: For all situations s and s′, if s and s′ both make all the same propositions true, then s=s′.

(Situation(s) & Situation(s′)) → ∀p[(s⊨p ↔ s′⊨p) → s=s′]

The following input file helps PROVER9 find a proof of this theorem much more quickly, by setting the flag "set(auto2).".

theorem02.flags.in

To set the same flag using the graphical version of Prover9, select the "Prover9 Options" tab, then select "All Options" and "Meta Options", and check the box "auto2". auto2 is a meta-option that sets the following options:

   set(auto2) -> set(auto).
   set(auto) -> set(auto_inference).
   set(auto) -> set(auto_setup).
   set(auto_setup) -> set(predicate_elim).
   set(auto_setup) -> assign(eq_defs, unfold).
   set(auto) -> set(auto_limits).
   set(auto_limits) -> assign(max_weight, 100).
   set(auto_limits) -> assign(sos_limit, 20000).
   set(auto) -> set(auto_denials).
   set(auto) -> set(auto_process).
   set(auto2) -> assign(new_constants, 1).
   set(auto2) -> assign(fold_denial_max, 3).
   set(auto2) -> assign(max_weight, 200).
   set(auto2) -> assign(nest_penalty, 1).
   set(auto2) -> assign(skolem_penalty, 3).
   set(auto2) -> assign(sk_constant_weight, 0).
   set(auto2) -> assign(prop_atom_weight, 5).
   set(auto2) -> set(sort_initial_sos).
   set(auto2) -> assign(sos_limit, -1).
   set(auto2) -> assign(lrs_ticks, 3000).
   set(auto2) -> assign(max_megs, 400).
   set(auto2) -> assign(stats, some).
   set(auto2) -> clear(echo_input).
   set(auto2) -> set(quiet).
   set(auto2) -> clear(print_initial_clauses).
   set(auto2) -> clear(print_given).

Theorem 03: Every part of a situation is a situation
(Situation(s) & x ⊴s) → Situation(x).
- theorem03.in
- model03.in
Theorem 04: A situation s is a part of situation s′ iff every proposition true in s is true in s′
(Situation(s) & Situation(s′)) → [s ⊴s′ ↔ ∀p(s⊨p → s′⊨p)]
- theorem04.in
- model04.in
The following input file includes some flags that help PROVER9 find a proof of this theorem much more quickly.
- theorem04.flags.in
Again, this sets the flag "set(auto2)" and if this flag is set in the graphical version, a proof is found very quickly.
Theorem 05: Situations s and s′ are parts of each other if and only if they are the same situation.
(Situation(s) & Situation(s′) & s⊴s′ & s′⊴s) → s=s′
- theorem05.in
- model05.in
Theorem 06: Situations s and s′ have the same parts iff they are the same situation.
(Situation(s) & Situation(s′)) → [∀s″(s″⊴s ↔ s″⊴s′) → s=s′]
- theorem06.in
- model06.in
Theorem 07: Part-of (⊴) is reflexive, anti-symmetric and transitive.
s⊴s & [s⊴s′ → ¬(s′⊴s)] & [(s⊴s′ & s′⊴s″) → s⊴s″]
- theorem07.in
- model07.in
The following input file includes some flags that help PROVER9 find a proof of this theorem much more quickly.
- theorem07.flags.in
Again, this sets the flag "set(auto2)" and if this flag is set in the graphical version, a proof is found very quickly.
Theorem 08: Every proposition is persistent.
∀pPersistent(p).
- theorem08.in
- model08.in
Theorem 09: There are actual and non-actual situations.
∃s(Actual(s)) & ∃s(¬Actual(s))
- theorem09.in
- model09.in
The following input file includes some flags that help PROVER9 find a proof of this theorem much more quickly.
- theorem09.flags.in
This sets the flag "set(auto2)" and if this flag is set in the graphical version, a proof is found very quickly.
Theorem 10: No proposition and its negation are true in any actual situation.
∀x[Actual(x) → ¬∃p(s⊨p & s⊨¬p)]
- theorem10.in
- model10.in
Theorem 11: Some propositions are not factual in any actual situation.
∃p∀s(Actual(s) → ¬s⊨p)
- theorem11.in
- model11.in
Theorem 12: For every two situations, there is a situation of which they are both a part.
∀s∀s′∃s″(s⊴s″ & s′⊴s″)
- theorem12.in [We are uncertain this completes in a proof.]
- model12.in
The above input file for the theorem, along with some added flags, leads to a proof relatively quickly in the June2006B version of Prover9, but so far, we can't confirm a proof in later versions of Prover9.
Theorem 13: There are maximal₁ and partial₁ situations.
(a) ∃s(Maximal₁(s))
(b) ∃s(Partial₁(s))
- theorem13a.in
- model13a.in
- theorem13b.in
- model13b.in
Theorem 14: There are maximal₂ and partial₂ situations.
(a) ∃s(Maximal₂(s))
(b) ∃s(Partial₂(s))
- theorem14a.in
- model14a.in
- theorem14b.in
- model14b.in
Theorem 15: All worlds are maximal₁.
∀x(World(x) → Maximal₁(x))
- theorem15.in
- model15.in
Theorem 16: All possible situations are consistent.
∀x[(Possible(x) & Situation(x)) → Consistent(x))
- theorem16.in
- model16.in
Theorem 17: All worlds are possible and consistent.
(a) ∀x(World(x) → Possible(x))
(b) ∀x(World(x) → Consistent(x))
- theorem17a.in
- model17a.in
- theorem17b.in
- model17b.in
Theorem 18: There is a unique actual world.
(a) ∃x(World(x) & Actual(x)
(b) ∀xy[(World(x) & World(y) & Actual(x) & Actual(y)) → x=y]
- theorem18a.in
- model18a.in
The following input file includes some flags that help PROVER9 find a proof of this theorem much more quickly.
- theorem18a.flags.in
Next we continue with Theorem 18b:
- theorem18b.in [We are uncertain this completes in a proof.]
- model18b.in
Theorem 19: All and only actual situations are part of the actual world.
∀x[(Situation(x) & Actual(s)) ↔ x ⊴ w_α]
- theorem19.in
- model19.in
Theorem 20: A proposition is true iff it is true in the actual world.
∀p(p ↔ w_α⊨p)
- theorem20.in
- model20.in
Theorem 21: Actual situations exemplify every property they encode.
∀x[(Situation(x) & Actual(x)) → ∀F(xF → Fx)]
- theorem21.in
- model21.in
Theorem 22: A proposition p is true in the actual world iff the actual world exemplifies being such that p.
w_α⊨p ↔ [λy p]w_α
- theorem22.in
- model22.in
Theorem 23: A proposition p is true iff the proposition that the actual world exemplifies being such that p is true in the actual world.
p ↔ w_α⊨[λy p]w_α
- theorem23.in
- model23.in
Lemmas for Theorems 24b and 25a. The following lemmas are needed to simplify the proof of theorems 24b and 25a. Some of these lemmas are corollaries to the following principle which defines the logic of encoding: ◊xF → □xF.
It is important to note that the following lemmas, which are needed for theorems 24 and 25, and theorems 24 and 25 themselves, require modal reasoning with respect to the notions that have defined in object theory. Now throughout the above input files, we have been translating modal claims in object theory, of the form "□p" and "◊p", into PROVER9 claims of the form:
```
 all d (Point(d) -> True(p,d)).
 exists d (Point(d) & True(p,d)).
```
Notice that de introduced a variable "d" to range over points. That is because automated reasoning engines don't allow modal operators. So to translate modal claims into first-order non-modal claims these engines can process, we expand the modal claims as quantifications over points. We use points instead of worlds because the latter is a defined notion in object theory. Indeed, World(x) is first defined in Theorem 15 above, in theorem15.in.

Now the final lemmas and theorems below require not only that de introduce points and translate modal claims as quantifications over points, but also that de relativize our predicates to points, for the reasoning depends on how the truth of claims involving these relativized predicates vary from point to point. That is, none of the previous theorems required us to reason about how the truth of the following varies from point to point:
```
Enc(x,F)
Encp(x,p)
TrueIn(p,x)
Situation(x)
World(x)
Actual(x)
```
But the proofs of the following lemmas and theorems turn on the behavior of these defined notions within modal contexts (i.e., they turn on the behavior of these notions at various points). We must define and make use of the following notions:
```
EncAt(x,F,d)
EncpAt(x,p,d)
TrueInAt(p,x,d)
SituationAt(x,d)
WorldAt(x,d)
ActualAt(x,d)
```
Remember that the variable "d" ranges over points and the language doesn't presuppose the notion of a world. The reader should be able come to understand why these notions need to be defined by studying the proofs in the original paper.
- L1: If x is possibly a world, x is necessarily a world.
  ◊World(x) → □World(x)
  L1.in
  modelL1.in
- L2: If a proposition p is possibly encoded in an object, it is necessarily encoded in that object.
  ◊x[λy p] → □x[λy p]
  L2.in
  modelL2.in
- L2, Corollary: If it is possible that p is true in x, then it is necessary that p is true in x
  ◊x⊨p → □x⊨p
  L2-Corollary.in
  modelL2-Corollary.in
- L3: Necessarily: if x is an actual world, then a proposition p is true in x iff p is true.
  □[(World(x) & Actual(x)) → ∀p((x⊨p) ↔ p)]
  L3.in
  modelL3.in
- L4: Necessarily, there is an actual world.
  □∃x(World(x) & Actual(x))
  L4.in
  modelL4.in

Theorem 24: A proposition p is necessarily true iff p is true in all worlds.
(a) □p → ∀w(w⊨p)
(b) ∀w(w⊨p) → □p
- theorem24a.in
- model24a.in
- theorem24b.in
- model24b.in
Theorem 25: A proposition p is possibly true iff p is true in some world.
(a) ◊p → ∃w(w⊨p)
(b) ∃w(w⊨p) → ◊p
- theorem25a.in
- model25a.in
- theorem25b.in
- model25b.in

Footnotes

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.