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.

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.

Tools You Will Need/June2006B

Tools You Will Need/VersionsAfter June 2006B

Tools You Will Need/Graphical Application

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:

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.

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

pistrue insituations("s⊨p") =s[λzp]

xis apart ofy("x⊴y") = ∀F(xF→yF)

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

Actual(s) = ∀p(s⊨p→p) (i.e.,sis actual iff every proposition true insis true)

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

Maximal_{1}(s) = ∀p(s⊨p∨s⊨ ¬p)

Partial_{1}(s) = ∃p(s⊭p&s⊭¬p)

Maximal_{2}(s) = ∀p(s⊨p)

Partial_{2}(s) = ∃p(s⊭p)

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.]

- 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*[(*s*⊨*p*↔*s*′ ⊨*p*) →*s*=*s*′] - Theorem 3: Every part of a situation is a situation
(Situation(

*s*) &*x*⊴*s*) → Situation(*x*). - 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*(*s*⊨*p*→*s*′ ⊨*p*)] - Theorem 5: 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*′ - 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*′] - Theorem 7: Part-of (⊴)
is reflexive, anti-symmetric and transitive.
*s*⊴*s*& [*s*⊴*s*′ → ¬(*s*′⊴*s*)] & [(*s*⊴*s*′ &*s*′⊴*s*″) →*s*⊴*s*″] - Theorem 8: Every proposition is persistent.
∀

*p**Persistent*(*p*). - Theorem 9: There are actual and non-actual situations.
∃

*s*(*Actual*(*s*)) & ∃*s*(¬*Actual*(*s*)) - Theorem 10: No proposition and its negation are true in
any actual situation.
∀

*x*[*Actual*(*x*) → ¬∃*p*(*s*⊨*p*&*s*⊨ ¬*p*)] - Theorem 11: Some propositions are not factual in any actual
situation.
∃

*p*∀*s*(*Actual*(*s*) → ¬*s*⊨*p*) - Theorem 12: For every two situations, there is a situation
of which they are both a part.
∀

*s*∀*s*′∃*s*″(*s*⊴*s*″ &*s*′⊴*s*″) - Theorem 13: There are maximal
_{1}and partial_{1}situations.(a) ∃s(

*Maximal*_{1}(*s*))

(b) ∃s(*Partial*_{1}(*s*)) - Theorem 14: There are maximal
_{2}and partial_{2}situations.(a) ∃s(

*Maximal*_{2}(*s*))

(b) ∃s(*Partial*_{2}(*s*)) - Theorem 15: All worlds are maximal
_{1}.∀

*x*(*World*(*x*) →*Maximal*_{1}(*x*)) - Theorem 16: All possible situations are consistent.
∀

*x*[(*Possible*(*x*) &*Situation*(*x*)) →*Consistent*(*x*)) - Theorem 17: All worlds are possible and consistent.
(a) ∀

*x*(*World*(*x*) →*Possible*(*x*))

(b) ∀*x*(*World*(*x*) →*Consistent*(*x*)) - Theorem 18: There is a unique actual world.
(a) ∃

*x*(*World*(x) &*Actual*(*x*)

(b) ∀*x**y*[(*World*(*x*) &*World*(*y*) &*Actual*(*x*) &*Actual*(*y*)) →*x*=*y*] - Theorem 19: All and only actual situations are part of the actual world.
∀

*x*[(*Situation*(*x*) &*Actual*(*s*)) ↔*x*⊴*w*_{α}] - Theorem 20: A proposition is true iff it is true in the actual world.
∀

*p*(*p*↔*w*_{α}⊨*p*) - Theorem 21: Actual situations exemplify every property they encode.
∀

*x*[(*Situation*(*x*) &*Actual*(*x*)) → ∀*F*(*xF*→*Fx*)] - 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*_{α} - 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*_{α} - 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 we introduced a variable "d" ranging 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 we 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)

We have used the variable "d" as an argument in the above relations, remember that they range over

*points*. Otherwise, the language would 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

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*

◊*x*⊨*p*→ □*x*⊨*p*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*((*x*⊨*p*) ↔*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

- L1: If
- Theorem 24: A proposition
*p*is necessarily true iff*p*is true in all worlds.

□*p*↔ ∀*w*(*w*⊨*p*)(a) □

*p*→ ∀*w*(*w*⊨*p*)

(b) ∀*w*(*w*⊨*p*) → □*p* - Theorem 25: A proposition
*p*is possibly true iff*p*is true in some world.

◊*p*↔ ∃*w*(*w*⊨*p*)

(a) ◊

*p*→ ∃*w*(*w*⊨*p*)

(b) ∃*w*(*w*⊨*p*) → ◊*p*

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.