ontolog-forum
[Top] [All Lists]

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

 To: ontolog-forum@xxxxxxxxxxxxxxxx "John F. Sowa" Tue, 12 Oct 2010 08:51:27 -0400 <4CB459CF.2010703@xxxxxxxxxxx>
 ```Chris, Rich, and Doug,    (01) I agree with Chris M. about the issues in this thread. But I'd like to add a few more points.    (02) 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:    (03) 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.    (04) 2. The basic quantifiers range over N. A typical FOL statement about integers would not use quantifiers over anything else.    (05) 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).    (06) 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).    (07) 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.    (08) 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.    (09) 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.    (010) CL lets you have quantifiers that range over functions and relations, but the proof procedures are purely first-order in style and complexity.    (011) RC: >> Higher-order languages are indeed more expressive [than FOL]. >> As a consequence, they are not even partially decidable.    (012) DF: > 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.    (013) 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.    (014) 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.    (015) John    (016) _________________________________________________________________ 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    (017) ```
 Current Thread [ontolog-forum] using SKOS for controlled values for controlled vocabulary, Ken Laskey Re: [ontolog-forum] using SKOS for controlled values for controlled vocabulary, John F. Sowa Re: [ontolog-forum] using SKOS for controlled values for controlled vocabulary, Laskey, Ken Re: [ontolog-forum] using SKOS for controlled values for controlled vocabulary, John Bottoms Re: [ontolog-forum] using SKOS for controlled values for controlled vocabulary, John F. Sowa Re: [ontolog-forum] using SKOS for controlled values for controlled vocabulary, Christopher Menzel Re: [ontolog-forum] using SKOS for controlled values for controlledvocabulary, Rich Cooper Re: [ontolog-forum] using SKOS for controlled values for controlledvocabulary, Christopher Menzel [ontolog-forum] HOL decidability [Was: using SKOS for controlled values for controlledvocabulary], doug foxvog Re: [ontolog-forum] HOL decidability [Was: using SKOS for controlled values for controlledvocabulary], John F. Sowa <= [ontolog-forum] Conation as an explanation of human thought processes, Rich Cooper Re: [ontolog-forum] HOL decidability [Was: using SKOS for controlled values for controlledvocabulary], Rich Cooper Re: [ontolog-forum] HOL decidability [Was: using SKOS forcontrolled values for controlledvocabulary], Rich Cooper Re: [ontolog-forum] HOL decidability [Was: using SKOS for controlled values for controlledvocabulary], Christopher Menzel Re: [ontolog-forum] HOL decidability [Was: using SKOS for controlled values for controlledvocabulary], Rich Cooper Re: [ontolog-forum] HOL decidability [Was: using SKOS for controlled values for controlledvocabulary], Christopher Menzel Re: [ontolog-forum] HOL decidability [Was: using SKOS for controlled values for controlledvocabulary], Rich Cooper Re: [ontolog-forum] HOL decidability [Was: using SKOS for controlled values for controlledvocabulary], Duane Nickull Re: [ontolog-forum] HOL decidability [Was: using SKOS for controlled values for controlledvocabulary], Rich Cooper Re: [ontolog-forum] HOL decidability [Was: using SKOS for controlled values for controlledvocabulary], Bill Andersen