The question before us is this. Instead of formulating
Theorem 2 ("The Form of *G* encodes *G*") as:

Theorem 2: IsTheFormOf(why don't we introduce the functional term "TheFormOf(x,G) →xG

Theorem 2:x=TheFormOf(G) →xG

The answer has to do with a problem that arises with the principles
that would be needed to sort the object "TheFormOf(*G*)". In
object theory, the Platonic notion the Form of *G*
(‘Φ_{G}’) is defined as:

ΦSuppose we tried to represent the description Φ_{G}=_{df}ιx(A!x& ∀F(xF≡G⇒F))

all z all G ((Object(z) & Property(G)) -> (AFormOf(z,G) <-> (Ex1(A,z,W) & (all F (Property(F) -> (Enc(z,F) <-> Implies(G,F))))))). all z all G ((Object(z) & Property(G)) -> (z=TheFormOf(G) <-> (AFormOf(z,G) & (all y ((Object(y) & AFormOf(y,G)) -> y=z))))).

In the usual way, the second definition tells us that an object
*z* is *the Form of G* whenever *z* is a
Form of *G* and any other Form of *G* is identical
to *z*.

So far so good. But if PROVER9 is to find proofs of
theorems involving TheFormOf(*G*), it will need to infer, when
it finds an object *x* that is identical to
TheFormOf(*G*), that Object(*x*) and
Property(*G*). Similarly, to cut down its search space, it
will need to ignore any identity of the form
*x*=TheFormOf(*G*) when either *x* is not an
object or *G* is not a property. (Recall that since
PROVER9 is first order and every domain object is an
individual, it will populate the domain with all sorts of domain
instances of concepts, relations, and identity claims even when the
individuals are not of the right sort to serve as the arguments of
those concepts, relations, and claims.)

Thus, it would be necessary to place the following sorting constraint
on TheFormOf(*G*):

all G all x (x=TheFormOf(G) -> (Object(x) & Property(G))).

But if we do this, PROVER9 will find contradiction in the presence of the following sorting constraint on objects, namely:

all x (Property(x) -> -Object(x)).

i.e.,

all x (Object(x) -> -Property(x)).

To see how all these correct-looking constraints lead to a
contradiction, consider any element of the domain, say *b*,
such that Object(*b*). Sorting on the concept Object(*x*)
immediately tells PROVER9 that -Property(*b*).
But then the above sorting constraint on TheFormOf(*G*)} will
be invoked. PROVER9 will instantiate the variable
*G* to *b* in the sorting contraint on
TheFormOf(*G*), to get:

all x (x=TheFormOf(b) -> (Object(x) & Property(b))).

But from -Property(*b*), PROVER9 will infer that the
consequent in this universal claim is false and therefore arrive,
essentially by Modus Tollens, at the generalization

all x -(x = TheFormOf(b)).

Then, PROVER9 will instantiate *x* to
TheFormOf(*b*), yielding:

-(TheFormOf(b) = TheFormOf(b))

This contradicts a clause that PROVER9 will infer
from *x*=*x*, which is part of its built-in theory of
identity:

TheFormOf(b) = TheFormOf(b)

This contradiction results because the quantifiers in
PROVER9 range over *everything* in the domain,
since the underlying system is unsorted, classical first-order logic.
As far as PROVER9 is concerned, the denotation of the
term TheFormOf(*b*) is part of the domain, since all terms
denote in classical first-order logic.

So we can't use the proposed sorting constraint on TheFormOf(G)} to
help PROVER9 cut down its search space and find proofs
of the theorems. Thus, our strategy has been to properly define and
use the *relation* IsTheFormOf(*x*,*G*) in our
theorems. Even if we place sorting constraints on the arguments to
this relation, the consequences of such constraints won't be
inconsistent with the instances of identity generated by
PROVER9.

**Acknowledgments**: The authors would like to thank
Chris Menzel for helping us to work through this issue.