In this section below, we provide a set of links to input and output
files that prove one of the theorems connected with a distinct body of
results within abstract object theory. At present, we have used
PROVER9 to prove the fundamental theorems of Plato's
Theory of Forms. This theory was initially developed in E. Zalta,
*Abstract Objects: An Introduction to Axiomatic Metaphysics*
(Dordrecht: D. Reidel, 1983), Chapter II, Section 1. It was then refined
in a paper by F.J. Pelletier and E. Zalta
(‘How to Say Goodbye to the Third Man’)
(we give the full reference below). Indeed, as we shall see,
PROVER9 and MACE4 have helped us
identify an error in one of the "theorems" in Pelletier & Zalta
2000.

For the theorems proved below, you will need the June2006B version of Prover9. See the link to this version on the following page:

Tools You Will Need

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.

In this section, we follow closely the theorems proved in F.J. Pelletier and
E. Zalta,
‘How to Say Goodbye to the Third Man’,
published in *Noûs*, 34/2 (June 2000): 165–202.
This paper significantly enhances the original sketch of the theory
of Forms developed in Zalta 1983, *op. cit.*. It does so
by developing a "thick" theory of Forms, whereas in Zalta 1983,
a "thin" theory of Forms was used. The difference is this: in
the thin theory of Forms, the Form of *F* is identified as the
abstract object that encodes exactly one property, namely, *F*.
However, on the thick theory of Forms, the Form of *F* is
identified as the abstract object that encodes all and only the
properties necessarily impled by *F*. Though Pelletier
& Zalta 2000 show text-based reasons for thinking that Plato had the
thick theory of Forms in mind, the subsequent development of the
theory has a lacuna. One of the "theorems" is in fact not a
theorem (though the proposition in question is a theorem in
the thin theory of Forms, it is not a theorem in the thick
theory). This was discovered using PROVER9 and
MACE4. We discuss this more fully below.

The following definitions are fully motivated and explained in that
paper. However, the definitions below take on a form that varies
slightly from the paper. We can't translate
"Φ_{G}" ("The Form of *G*") as "the
abstract object *x* that encodes all and only the properties
*F* implied by *G*", since PROVER9
doesn't have definite descriptions. Thus, to represent claims
involving Φ_{G}, we define a relation
"*IsTheFormOf*(*x*,*G*)". Therefore, the reader
may need to consider how the definitions below correlate with the
definitions in Pelletier & Zalta
2000:^{[1]}

There is one question that will arise when the reader examines how
we solve this problem of representing "The Form of *G*" (i.e,
Φ_{G}) in object theory. In what follows, we use
the relation statement "IsTheFormOf(*x*,*G*)" instead of
the identity claim "*x*=TheFormOf(*G*)" to help us
represent object theoretic claims about "The Form of *G*". Our
decision to use the relation statement was motivated by an
inconsistency that PROVER9 will generate from
innocuous-looking "sorting constraints" on the claims
"Object(*x*)", "AConcept(*x*,*G*)" and
"*x*=TheFormOf(*G*)". This inconsistency doesn't arise
when we use the relational statement
"IsTheFormOf(*x*,*G*)" instead of the identity claim
"*x*=TheFormOf(*G*)" in formulating the theorems of
object theory. A full description of the problem that arises can be
found in the following supplementary document:

Sorting-Constraints Issue

We now turn to the definitions and theorems.

GimpliesF("G⇒F") = □&forallx(Gx→Fx)

xis a Form ofG("IsAFormOf(x,G)") =A!x& ∀F(xF≡G⇒F)

Form(x) =_{df}∃G(IsAFormOf(x,G))∃!

xφ ("there is a uniquexsuch that φ") = ∃x[φ & ∀y(φ(y/x) →y=x)],

where φ(y/x) is the result of substitutingyfor every occurrence ofxin φ, providedyis substitutable forx

IsTheFormOf(x,G) =_{df}IsAFormOf(x,G) & ∀y(IsAFormOf(y,G) →y=x)

yparticipates_{PTA}inx("Participates_{PTA}(y,x)") = ∃F(IsTheFormOf(x,F) &Fy)

yparticipates_{PH}inx("Participates_{PH}(y,x)") = ∃F(IsTheFormOf(x,F) &yF)

Now we have the following theorems:

- Theorem 1: There is a unique Form of
*G*, for every property*G*.∀

*G*∃!*x*[*IsAFormOf*(*x*,*G*)]- See Theorems 1a and 1b.

- Theorem 1a: There is at least one Form of
*G*, for every property*G*.∀

*G*∃*x*[*IsAFormOf*(*x*,*G*)] - Theorem 1b: There is at most one Form of
*G*, for every*G*.∀

*x*,*y*,*G*[(*IsAFormOf*(*x*,*G*) &*IsAFormOf*(*y*,*G*)) →*x*=*y*]. - Lemma: The Form of
*G*encodes a property*F*iff*G*implies*F*.*IsTheFormOf*(*x*,*G*) → ∀*F*(*xF*≡*G*⇒*F*) - Theorem 2: The Form of
*F*encodes*F*.*IsTheFormOf*(*x*,*F*) →*xF* - Theorem 3: An object
*y*exemplifies*F*iff it participates_{PTA}in the Form of*F**IsTheFormOf*(*x*,*F*) → [*Fy*≡*Participates*_{PTA}(*y*,*x*)]

At this point, we interrupt the procession of theorems to identify an error in Pelletier & Zalta 2000. It occurs in "Theorem" 4. In the paper, the "theorem" is stated as follows:

- Theorem 4: An object
*y*encodes*F*iff*y*participates_{PH}in the Form of*F**IsTheFormOf*(*x*,*F*) → [*yF*≡*Participates*_{PH}(*y*,*x*)]

However, with the help of MACE4, we found a countermodel, countermodel4.in, in which the antecedent is true but the right-to-left direction of the biconditional in the consequent is false. With this countermodel as a clue, we developed a counterexample by hand, which we fully describe here:

Countermodel to "Theorem" 4

However, if we weaken the "theorem" so that the consequent is the left-to-right conditional, then we do have as a theorem:

- Theorem 4*: If an object
*y*encodes*F*, then it participates_{PH}in the Form of*F*.*IsTheFormOf*(*x*,*F*) → [*yF*→*Participates*_{PH}(*y*,*x*)]

The theorems in Pelletier & Zalta 2000 continue:

- Theorem 5: If there are two distinct
*F*-things, then there is a Form of*F*in which they both participates_{PTA}. (One Over Many)[

*Fy*&*Fz*&*y*≠*z*] → ∃*x*[*IsTheFormOf*(*x*,*F*) &*Participates*_{PTA}(*y*,*x*) &*Participates*_{PTA}(*z*,*x*)] - Theorem 6: If there are two distinct
*F*-encoders, then there is a Form of*F*in which they both participates_{PH}. (One Over Many)[

*yF*&*zF*&*y*≠*z*] → ∃*x*[*IsTheFormOf*(*x*,*F*) &*Participates*_{PH}(*y*,*x*) &*Participates*_{PH}(*z*,*x*)] - Theorem 7: There are objects which participate
_{PH}in a Form and which are identical with that Form.∃

*x*∃*F*[*IsTheFormOf*(*x*,*F*) &*Participates*_{PH}(*x*,*x*)] - Theorem 8: Every Form participates
_{PH}in itself.∀

*x*[*Form*(*x*) →*Participates*_{PH}(*x*,*x*)] - Theorem 9: There are objects which participate
_{PTA}in a Form and which are identical with that Form.∃

*x*∃*F*[*IsTheFormOf*(*x*,*F*) &*Participates*_{PTA}(*x*,*x*)] - Theorem 10: Encoding a property doesn't imply
exemplifying that property.
¬∀

*F*∀*x*(*xF*→*Fx*)

1. For purposes of
correlating terminology, note that in addition to allowing for the
changes made to make up for missing definite description, we use the
term "abstract" object ("*A!x*") below instead of the term
"ideal" object ("*Ix*"). The latter was used in Pelletier
& Zalta 2000. Even with with change of terminology, the
definitions used on this page will need to be compared with those in
the paper.

2. Proof: Assume *F*
and *G* are necessarily equivalent. Now, for the left-to-right
direction, assume that for an arbitrary property *H*,
*F* ⇒ *H*, i.e., that
□∀*x*(*Fx* → *Hx*). If we can
show *G* ⇒ *H*, we are done (without loss of
generality, since the proof of the right-to-left direction goes
exactly the same way). To show □∀*x*(*Gx*
→ *Hx*), we first prove the embedded, non-modal universal
claim holds at an arbitrary world, say *w*. So, for an
arbitrary object, say *c*, suppose *Gc* at *w*.
Then since *G* and *F* are necessarily equivalent, they
are equivalent at *w*, so it follows that *Fc* at
*w*. But *F* necessarily implies *H*, and so
materially implies *H* at *w*. Thus, *Hc*. So,
we've proved, with respect to an arbitrary object *c* and world
*w*, that *Gc → Hc* at *w*. Thus, by
universal generalization on *c* and then *w*, we've
established □∀*x*(*Gx* → *Hx*),
i.e., *G*⇒*H*.