The Computational Theory of Plato's Forms

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.

The Tools You Will Need

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.

The Theorems for the Theory of Forms

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.

G implies F ("G ⇒ F") = □∀x(Gx → Fx)

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

Form(x)  =_df  ∃G(IsAFormOf(x,G))

∃!xφ ("there is a unique x such that φ") = ∃x[φ & ∀y(φ(y/x) → y=x)],
    where φ(y/x) is the result of substituting y for every occurrence of x in φ, provided y is substitutable for x

IsTheFormOf(x,G)   =_df   IsAFormOf(x,G) & ∀y(IsAFormOf(y,G) → y=x)

y participates_PTA in x ("Participates_PTA(y,x)") = ∃F(IsTheFormOf(x,F) & Fy)

y participates_PH in x ("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)]

  • theorem1a.in
  • theorem1a.out
  • model1a.in
  • model1a.out

• Theorem 1b: There is at most one Form of G, for every G.

  ∀x,y,G[(IsAFormOf(x,G) & IsAFormOf(y,G)) → x=y].

  • theorem1b.in
  • theorem1b.out
  • model1b.in
  • model1b.out

• Lemma: The Form of G encodes a property F iff G implies F.

  IsTheFormOf(x,G) → ∀F(xF ≡ G⇒F)

  • lemma.in
  • lemma.out
  • lemma-model.in
  • lemma-model.out

• Theorem 2: The Form of F encodes F.

  IsTheFormOf(x,F)  →  xF

  • theorem2.in
  • theorem2.out
  • model2.in
  • model2.out

• Theorem 3: An object y exemplifies F iff it participates_PTA in the Form of F

  IsTheFormOf(x,F)  → [Fy ≡ Participates_PTA(y,x)]

  • theorem3.in
  • theorem3.out
  • model3.in
  • model3.out

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

  • theorem4*.in
  • theorem4*.out
  • model4*.in
  • model4*.out

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

  • theorem5.in
  • theorem5.out
  • model5.in
  • model5.out

• 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)]

  • theorem6.in
  • theorem6.out
  • model6.in
  • model6.out

• 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)]

  • theorem7.in
  • theorem7.out
  • model7.in
  • model7.out

• Theorem 8: Every Form participates_PH in itself.

  ∀x[Form(x) → Participates_PH(x,x)]

  • theorem8.in
  • theorem8.out
  • model8.in
  • model8.out

• 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)]

  • theorem9.in
  • theorem9.out
  • model9.in
  • model9.out

• Theorem 10: Encoding a property doesn't imply exemplifying that property.

  ¬∀F∀x(xF → Fx)

  • theorem10.in
  • theorem10.out
  • model10.in
  • model10.out

Footnotes

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.