ontolog-forum
[Top] [All Lists]

Re: [ontolog-forum] Role of definitions (Remember the poor human)

To: Christopher Menzel <cmenzel@xxxxxxxx>
Cc: "[ontolog-forum] " <ontolog-forum@xxxxxxxxxxxxxxxx>
From: Pat Hayes <phayes@xxxxxxx>
Date: Tue, 13 Feb 2007 16:38:58 -0600
Message-id: <p06230908c1f7e9765c00@[10.100.0.26]>
>On Feb 13, 2007, at 2:18 PM, Pat Hayes wrote:
>>  ...For example, adding the power to make
>>  definitions to IKL would make the entire logic paradoxical, and
>>  re-create the Russell paradox in CL.
>
>Pat, I agree strongly with your general point, but I think what you 
>say here is not true about CL and moreover reflects an incorrect 
>concept of definitions (which puzzles me because I know you know what 
>a good definition of "definition" is!).  What you say above seems to 
>identify "the power to make definitions" with the ability to call 
>things into existence ex nihilo.  But that is *exactly* what one 
>cannot do in giving a definition.  A critical condition on a genuine 
>definition is that it be *non-creative*: A definition (within a 
>theory) cannot entail the existence of anything that was not already 
>entailed by the theory.  Hence, any purported definition in IKL of a 
>Russell set (property, class, type, whatever), or any other 
>paradoxical entity, would be illegitimate, for the same reason that 
>the Russell set {x | x not in x} is illegitimate in ZF set theory.  
>You can't prove the existence of a set of all non-self-membered sets 
>in ZF, hence, you can't legitimately introduce the name "{x | x not 
>in x}", as it violates the non-creative condition on definitions.  
>Same for CL.    (01)

I wont argue with what you are saying, but you 
are here using a very sophisticated notion of 
what a "definition" is. I don't think this notion 
(which is informed by a century of 
post-Russellian thought about how to deal with 
paradoxes) is what people usually mean by 
"definition". You are, to use a philosophical 
semi-joke term, assuming that all definitions 
come pre-Quined; but that is not how they are 
usually understood.    (02)

<I know you know all this>
For example, take ANSI KIF. That had a provision 
for stating definitions which clearly and 
explicitly separated them from assertions, and 
had no provision for distinguishing what you are 
here calling legitimate from illegitimate 
'definitions'. If one defines, in this sense, R 
to be the relation (lambda (x)(not (x x))), then 
this is indeed what R *must* be; from which it is 
easy to generate the Russell paradox. The 
illegitimacy of this definition arises from the 
fact that if stated as an assertion, it would be 
contradictory: it implicitly assumes the 
existence of something (the Russell "set") that 
cannot exist. By your modern criteria, this means 
that it cannot be regarded as a 'genuine' 
definition: but it looks like a definition, and 
it smells like a definition, it can be used to 
draw conclusions like any other definition, and I 
suspect that to most people it simply IS a 
definition: and so the problem it gives rise to 
must be solved elsewhere, for example by 
restricting the syntax of the logic or invoking 
the majestic structure of Zermelo-Fraenkel set 
theory. For example, if you were to add a kind of 
lambda-conversion to CL and call it a definition 
feature (a common (ab?)use of terminology), this 
is what you would get. And look how awful the 
practical consequences of your sophistication 
are: to even use a definition in the most 
elementary way - to replace the defined term by 
its definition - I must first formally prove that 
the entity described by this instance of the 
definition exists. I am virtually certain that 
nobody but a professional set theorist would even 
consider this a useful notion of "definition". 
Most mathematicians would quaver at this 
condition if they took it seriously, let alone 
the medics and practical men that Barry is 
concerned about.
</I know you know all this>    (03)

What I meant by the remark about adding 
definitions to CL was adding a simple definition 
feature which is not protected by existence 
criteria in this way, like the ANSII KIF 
definitions. The problem is exactly that this 
does in fact add a power to "call things into 
existence" by defining them: or if you prefer, 
put that last 'defining' inside scare quotes.    (04)

Pat    (05)

>-chris
>
>
>
>
>_________________________________________________________________
>Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/ 
>Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/ 
>Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
>Shared Files: http://ontolog.cim3.net/file/
>Community Wiki: http://ontolog.cim3.net/wiki/
>To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx
>    (06)


-- 
---------------------------------------------------------------------
IHMC            (850)434 8903 or (650)494 3973   home
40 South Alcaniz St.    (850)202 4416   office
Pensacola                       (850)202 4440   fax
FL 32502                        (850)291 0667    cell
phayesAT-SIGNihmc.us       http://www.ihmc.us/users/phayes    (07)


_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/  
Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/  
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/ 
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx    (08)

<Prev in Thread] Current Thread [Next in Thread>