The 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 (PROVER9/June2006B)

For your convenience, we've included links to the PROVER9 and MACE4 input and output files for each theorem, for the runs we have executed. You can compare your runs to ours.

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=[λz p]))

p is true in situation s ("sp") = s[λz p]

x is a part of y ("x y") = ∀F(xF → yF)

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

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

World(s) = Situation(x) & ◊∀p(sp ↔ p)

Maximal₁(s) = ∀p(sp s¬p)

Partial₁(s) = ∃p(sp & s¬p)

Maximal₂(s) = ∀p(sp)

Partial₂(s) = ∃p(sp)

Possible(s) = ◊Actual(s)
Consistent(s) = ¬∃p(sp & 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.

Theorem 1 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 2: 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[(sp ↔ s′p) → s=s′]
- theorem2.in
- theorem2.out
- model2.in
- model2.out
Theorem 3: Every part of a situation is a situation
(Situation(s) & x s) → Situation(x).
- theorem3.in
- theorem3.out
- model3.in
- model3.out
Theorem 4: 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(sp → s′p)]
- theorem4.in
- theorem4.out
- model4.in
- model4.out
Theorem 5: Situations s and s′ are parts of each other if and only if they are the same situation.
(Situation(s) & Situation(s′) & ss′ & s′s) → s=s′
- theorem5.in
- theorem5.out
- model5.in
- model5.out
Theorem 6: 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′]
- theorem6.in
- theorem6.out
- model6.in
- model6.out
Theorem 7: Part-of () is reflexive, anti-symmetric and transitive.
ss & [ss′ → ¬(s′s)] & [(ss′ & s′s″) → ss″]
- theorem7.in
- theorem7.out
- model7.in
- model7.out
Theorem 8: Every proposition is persistent.
∀pPersistent(p).
- theorem8.in
- theorem8.out
- model8.in
- model8.out
Theorem 9: There are actual and non-actual situations.
∃s(Actual(s)) & ∃s(¬Actual(s))
- theorem9.in
- theorem9.out
- model9.in
- model9.out
Theorem 10: No proposition and its negation are true in any actual situation.
∀x[Actual(x) → ¬∃p(sp & s¬p)]
- theorem10.in
- theorem10.out
- model10.in
- model10.out
Theorem 11: Some propositions are not factual in any actual situation.
∃p∀s(Actual(s) → ¬sp)
- theorem11.in
- theorem11.out
- model11.in
- model11.out
Theorem 12: For every two situations, there is a situation of which they are both a part.
∀s∀s′∃s″(ss″ & s′s″)
- theorem12.in
- theorem12.out
- model12.in
- model12.out
Theorem 13: There are maximal₁ and partial₁ situations.
(a) ∃s(Maximal₁(s))
(b) ∃s(Partial₁(s))
- theorem13a.in
- theorem13a.out
- model13a.in
- model13a.out
- theorem13b.in
- theorem13b.out
- model13b.in
- model13b.out
Theorem 14: There are maximal₂ and partial₂ situations.
(a) ∃s(Maximal₂(s))
(b) ∃s(Partial₂(s))
- theorem14a.in
- theorem14a.out
- model14a.in
- model14a.out
- theorem14b.in
- theorem14b.out
- model14b.in
- model14b.out
Theorem 15: All worlds are maximal₁.
∀x(World(x) → Maximal₁(x))
- theorem15.in
- theorem15.out
- model15.in
- model15.out
Theorem 16: All possible situations are consistent.
∀x[(Possible(x) & Situation(x)) → Consistent(x))
- theorem16.in
- theorem16.out
- model16.in
- model16.out
Theorem 17: All worlds are possible and consistent.
(a) ∀x(World(x) → Possible(x))
(b) ∀x(World(x) → Consistent(x))
- theorem17a.in
- theorem17a.out
- model17a.in
- model17a.out
- theorem17b.in
- theorem17b.out
- model17b.in
- model17b.out
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
- theorem18a.out
- model18a.in
- model18a.out
- theorem18b.in
- theorem18b.out
- model18b.in
- model18b.out
Theorem 19: All and only actual situations are part of the actual world.
∀x[(Situation(x) & Actual(s)) ↔ x w_α]
- theorem19.in
- theorem19.out
- model19.in
- model19.out
Theorem 20: A proposition is true iff it is true in the actual world.
∀p(p ↔ w_αp)
- theorem20.in
- theorem20.out
- model20.in
- model20.out
Theorem 21: Actual situations exemplify every property they encode.
∀x[(Situation(x) & Actual(x)) → ∀F(xF → Fx)]
- theorem21.in
- theorem21.out
- model21.in
- model21.out
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
- theorem22.out
- model22.in
- model22.out
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
- theorem23.out
- model23.in
- model23.out
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, and theorems 24 and 25, involve modal reasoning with respect to the notions that are defined in object theory. These notions therefore need to be modalized (i.e., relativized to the world). None of the previous theorems required modal reasoning with respect to the notions:
```
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 possible worlds). We must define and make use of the following notions:
```
EncAt(x,F,w)
EncpAt(x,p,w)
TrueInAt(p,x,w)
SituationAt(x,w)
WorldAt(x,w)
ActualAt(x,w)
```
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
  L1.out
  modelL1.in
  modelL1.out
- 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
  L2.out
  modelL2.in
  modelL2.out
- L2, Corollary: If it is possible that p is true in x, then it is necessary that p is true in x
  ◊xp → □xp
  L2-Corollary.in
  L2-Corollary.out
  modelL2-Corollary.in
  modelL2-Corollary.out
- 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((xp) ↔ p)]
  L3.in
  L3.out
  modelL3.in
  modelL3.out
- L4: Necessarily, there is an actual world.
  □∃x(World(x) & Actual(x))
  L4.in
  L4.out
  modelL4.in
  modelL4.out
Theorem 24: A proposition p is necessarily true iff p is true in all worlds.
(a) □p → ∀w(wp)
(b) ∀w(wp) → □p
- theorem24a.in
- theorem24a.out
- model24a.in
- model24a.out
- theorem24b.in
- theorem24b.out
- model24b.in
- model24b.out
Theorem 25: A proposition p is possibly true iff p is true in some world.
(a) ◊p → ∃w(wp)
(b) ∃w(wp) → ◊p
- theorem25a.in
- theorem25a.out
- model25a.in
- model25a.out
- theorem25b.in
- theorem25b.out
- model25b.in
- model25b.out

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.