ontolog-forum
[Top] [All Lists]

## Re: [ontolog-forum] HOL decidability [Was: using SKOSfor controlled valu

 To: "'[ontolog-forum] '" "Rich Cooper" Wed, 13 Oct 2010 14:54:47 -0700 <20101013215452.C838E138D1A@xxxxxxxxxxxxxxxxx>
 Hi Bill,   Nicely analyzed; my comments are below, -Rich   Sincerely, Rich Cooper EnglishLogicKernel.com Rich AT EnglishLogicKernel DOT com 9 4 9 \ 5 2 5 - 5 7 1 2     Earlier, Rich said this   RC: The plurality of Systems, as you called them, are ordered in pairs with the integers (a superset of primes), but not with the primes.  That is how Godel constructed his proof.  So there are true theorems that can’t be proven (factored) and false theorems that can’t be disproved (factored), because in association with the integers, they occasionally designate a prime – which by definition can’t be factored.   BA:> From what I could gather, he was trying to claim that somehow, under Gödel's construction, the non-theorems were the only things represented as prime numbers.  As I understand Gödel's method, and as you pointed out earlier, the business of the use of primes for arithmetizing syntax had nothing to do with the theoremhood (or not) of the resulting sentences (or proofs) so arithmetized.  I can't recall how the construction went exactly, but it seems to me that the point was that all sentences (proofs) were represented by non-primes, the idea being you could then exploit their arithmetic structure to tear them apart into their constituents.    Yes, and the factors designate those constituents.   So you'd have some non-primes that represent non-sentences (proofs), some non-primes that represent sentences (proofs), and primes that either represent primitives in the construction or fail to represent any legal syntactic entity.  Is this about right?   That's correct - the primes, not being factorable, designate unique expressions, and cannot be factored into those "legal syntactic entity" elements.    The discussion started with the concept that HOLs are more expressive than just the combined FOL primitives can express.  The primes are not factorable into those FOL primitives, but are unique expressions which cannot be reached through sentences composed of combinations of AND, OR, NOT and ground instances.     Thanks for making this clearer, Bill.    -Rich     > Either way, some face time with an > introductory text on the latter subject is in order.  I'd suggest > Boolos, Jeffrey, and Burgess, _Computability and Logic_.   Yes.  We all could benefit from more such face time.   > -chris > > _________________________________________________________________ > 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 >   Bill Andersen Highfleet, Inc. (www.highfleet.com) 3600 O'Donnell Street, Suite 600 Baltimore, MD 21224 Office: +1.410.675.1201 Cell: +1.443.858.6444 Fax: +1.410.675.1204             _________________________________________________________________ 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)

```
 Current Thread Re: [ontolog-forum] HOL decidability [Was: using SKOS forcontrolled values for controlledvocabulary], (continued)