Existence proofs for defined terms

sowa@watson.ibm.com
Message-id: <199201062016.AA05980@venera.isi.edu>
Date: Mon, 6 Jan 92 15:15:24 EST
From: sowa@watson.ibm.com
To: INTERLINGUA@isi.edu
Cc: JMC@cs.stanford.edu
Subject: Existence proofs for defined terms
I agree with John McCarthy's desire for conservative definitions.
But I disagree that existence is a requirement.  It is certainly
desirable, but even in mathematics, existence is not logically
required for a definition.  There are in fact different philosophies
about what it means for something to exist in mathematics.  Some people
will not admit any proof that does not show how to construct the object,
while others permit existence proofs that are highly nonconstructive.

The reason why mathematicians are fond of existence proofs is that they
would like to avoid the embarrassment of publishing a paper that proves
many weird and wonderful properties about the empty set.  There are many
published books and papers in the mathematical literature that do exactly
that.  Such theories are worthless, but they are not illogical.

> 1. Keeping definitions conservative has the advantage that during
> an argument or in connection with a communication, a definition
> may be introduced at any time by a human or a computer program.

I agree with that point, but I don't agree with the following:

> All that needs to be verified is that an object exists satisfying
> the defining sentence exists.  As discussed previously, for the
> most common forms of definition, e.g. <new symbol> = <rhs>, this
> is immediate.

If the defining statement is inconsistent, then nothing of the
desired type will exist.  But it should be possible for someone to
define a Meinongian round-square as an intermediate step in a proof
that roundness and squareness are mutually inconsistent.

> 2. Someone introduced and I discussed the idea of a partial definition
> that is successively refined.  I proposed something, found a
> bug in my proposal, and opined that it could be worked out.
> My present opinion is that the bug is rather fundamental,
> because it jeopardizes the conservative character of definitions.

> Suppose someone introduces a partial definition of some set.  Then
> suppose he (or some program) shows that an object exists satisfying
> this partial definition and with some <other property> as well.  Now
> suppose he (or it) refines the original partial definition.  Of
> course he still must show that an object satisfying the extended
> definition exists.  However, his use of the unextended definition
> is now jeopardized, because there may not exist an object satisfying
> the extended definition and the <other property>.

The definition as a syntactic form is not jeopardized.  If nothing
of the defined type exists, the definition is useless, but it causes
no harm to anything else.

John Sowa