[Top] [All Lists]

Re: [ontolog-forum] Ontologies as social mediators

To: "[ontolog-forum]" <ontolog-forum@xxxxxxxxxxxxxxxx>
From: Christopher Menzel <cmenzel@xxxxxxxx>
Date: Sun, 6 Dec 2009 13:54:12 -0600
Message-id: <8E53320E-DCC5-4BD7-A575-F3D081645D37@xxxxxxxx>
On Dec 5, 2009, at 10:48 AM, doug foxvog wrote:
> Ferenc wrote:
>> ... I have been trying to visualize the
>> condition where objects, properties and relations change theri character
>> and they become one of the other two as a result of mental operations.
>> ... So jsut a few examples
>> One of these operations is abstraction
>> that helps you see the properties of an object and create a list of such
>> properties.
>> Then by taking one of those properties as an OBJECT, you can go on to
>> define another set of properties.
> This is quite valid.  The issue of "chang[ing] their character" arises from
> the limitations of first order logic.  Computational complexity becomes
> greater when describing properties of properties and reasoning about them.    (01)

That is of course true in full higher-order systems but, as noted a couple of 
times in this forum by Pat Hayes and others, a system does not become 
higher-order in a sense that increases its complexity simply in virtue of 
permitting reasoning about properties and relations.  The complexity of such 
reasoning increases (from the semi-decidability of first-order logic to full 
undecidability) only under a very strong assumption: that every subset of the 
domain of an interpretation is (the extension of) a property; more generally, 
that every set of n-tuples of objects in the domain is (the extension of) an 
n-place relation.  This is the assumption that, from a purely theoretical 
perspective, separates first-order from higher-order logic.  But, importantly, 
this assumption cannot in fact be implemented in a reasoning system, as 
higher-order logics are semantically incomplete: given any proposed reasoning 
method for a second- or higher-order logic, there will be logically valid 
arguments whose validity cannot it cannot demonstrated by that method.    (02)

> In higher-order logic, one can treat relations, classes, and statements
> "relation instances", and instances of classes and make statements about
> them using relations which accept such classes.  The Cyc reasoner has been
> doing this since at least the mid-1990s.    (03)

As have many other higher-order systems (as I'm sure you know).  For the 
reasons above, however, the implemented reasoning methods for these systems -- 
even those whose formal semantics are fully higher-order -- are theoretically 
first-order (in the sense that they are complete relative to a weaker semantics 
for the systems (so-called "general semantics", based on the work of Henkin) 
that abandon the strong assumption above).  Indeed, some implementations of 
such systems (the HOL System, for example) translate the entire system into an 
explicit first-order theory to which standard first-order reasoning methods can 
then be applied directly.    (04)

Chris Menzel    (05)

Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/  
Config Subscr: 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 join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx    (06)

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