Sorting-Constraints Issue

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

Theorem 2: IsTheFormOf(x,G) → xG
why don't we introduce the functional term "TheFormOf(G)" and formulate theorems Theorem 2 (and others like it) as:
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:

ΦG =df ιx(A!x & ∀F(xF ≡ G ⇒ F))
Suppose we tried to represent the description ΦG in PROVER9 as TheFormOf(G). We might try to proceed as follows: first define z is a Form of G ("AFormOf(z,G)"), and then define the Form of G ("TheFormOf(G)"), as follows: 
 
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.