[Top] [All Lists]

Re: [ontolog-forum] HOL decidability [Was: using SKOS for controlled val

To: "'[ontolog-forum] '" <ontolog-forum@xxxxxxxxxxxxxxxx>
From: "Rich Cooper" <rich@xxxxxxxxxxxxxxxxxxxxxx>
Date: Tue, 12 Oct 2010 16:48:04 -0700
Message-id: <20101012234809.ABA13138CE9@xxxxxxxxxxxxxxxxx>

Dear John, Chris, Doug and Ed,


Comments below,




Rich Cooper


Rich AT EnglishLogicKernel DOT com

9 4 9 \ 5 2 5 - 5 7 1 2


-----Original Message-----
From: ontolog-forum-bounces@xxxxxxxxxxxxxxxx [mailto:ontolog-forum-bounces@xxxxxxxxxxxxxxxx] On Behalf Of John F. Sowa
Sent: Tuesday, October 12, 2010 5:51 AM
To: ontolog-forum@xxxxxxxxxxxxxxxx
Subject: Re: [ontolog-forum] HOL decidability [Was: using SKOS for controlled values for controlledvocabulary]


Chris, Rich, and Doug,


I agree with Chris M. about the issues in this thread.  But I'd like

to add a few more points.


Not so fast!  I'm sure you remember that the set of primes is infinite, and that there is no (known) function that can iterate them.  Godel showed that there are theorems which though true cannot be proven, and theorems which though false cannot be disproved, all based on the primes.  Chris and John, there are programs in Higher Order Logic (HOL) which cannot be proven or disproven, i.e., they cannot be constructed from AND, OR, NOT or any function you can think of.  Therefore HOL is more expressive (can express more truths) than FOL, period.  


Remember Hoftadter's Godel, Escher Bach which high school technophiles have read ever since its publication.  Here are some of those impossible constructions, expressed in a higher order logic than any strongly typed FOL CAD system can, even when its FOL primitives have been combined in well formed ways to generate something visually similar:





I’m sure you remember other Escher visualizations which don’t limit the observer to simplistic algebraic representations.  Higher order logic allows people to interpret experiences based on their similarity to previously experienced events.  Even events that cannot be cleanly decomposed into factors of logic can be expressed in HOLs.  That is why they are HIGHER order logics.


Yes, programs can be written that do not terminate, and yet which are valuable in themselves.  And yes, HOL really can express situations that FOL cannot.  

























The term HOL (higher-order logic) has been bandied about in many

different ways.  Logicians reserve it for a particular kind of

semantics that includes an infinite hierarchy of infinite sets.

There are several versions, but following is the basic idea:


  1. There is a starting set whose elements are called individuals.

     To be concrete, a typical example would be the set N of

     non-negative integers.  For that N, there are countably many

     individuals, but one could have larger or smaller sets.


  2. The basic quantifiers range over N.  A typical FOL statement

     about integers would not use quantifiers over anything else.


  3. Second-order logic would add another, much larger domain of

     quantification.  Depending on which variant of SOL one is

     talking about, that domain could include the set of all subsets

     of N, the set of all relations over N, the set of all functions

     over N, or the set that includes all of them.  In any case, if

     N is countable (Aleph 0), this set is uncountable (Aleph 1).


  4. The next level in the hierarchy has a domain of quantification

     that would include sets of all subsets of the previous domain

     (or all functions or all relations over that domain).  If the

     previous domain was of size (Aleph n), this one is of size

     (Aleph n+1).


Some logicians would say that this hierarchy goes beyond logic

to a very rich version of set theory.  (I agree with them.)

In any case, that huge hierarchy of increasingly larger infinities

creates huge problems about computational complexity, etc.


But most (perhaps all) of the computational systems that use the

term HOL *don't* assume this infinite hierarchy.  They just have

a single domain of quantification.  If you have a sorted logic,

that domain could be partitioned into separate subdomains for

individuals, sets, functions, and relations.


But whether or not you choose to partition the domain, this

approach is far more manageable.  And as a matter of fact, it

does not go beyond FOL methods of proof theory.  In fact, this

approach is the one that was adopted for Common Logic.


CL lets you have quantifiers that range over functions and

relations, but the proof procedures are purely first-order

in style and complexity.



>> Higher-order languages are indeed more expressive [than FOL].

>> As a consequence, they are not even partially decidable.



> Maybe Higher-order languages as a whole are not even partially decidable,

> but large numbers of statements in them are.  It was noted that normal

> computer languages embodied HOL.  Note that well-written programs in

> such languages are decidable.  Of course, it is possible to write

> programs which aren't.


I would avoid using the term HOL because it is ambiguous.  Logicians

think HOL implies that infinite hierarchy.  But programmers who have

implemented useful tools that allow quantifiers over functions and

relations have implemented something that is closer to the CL approach

than to the logicians' conception of HOL.


In short, you can let your quantifiers range over functions and

relations without going beyond FOL.  In fact, you can even have

decidable subsets of FOL that let quantifiers range over relations.





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


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    (01)

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