ontolog-forum
[Top] [All Lists]

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

 To: ontolog-forum@xxxxxxxxxxxxxxxx Christopher Menzel Wed, 13 Oct 2010 18:57:38 -0500 <4CB64772.30506@xxxxxxxx>
 ```On 10/13/2010 04:32 PM, Bill Andersen wrote: >>> ... >>> Hi Rich >>> >>> Here's a fixed precision implementation of a prime iterator, along >>> the lines Chris Menzel described. >>> >>> Enjoy >> >> Clearly, Bill, your code must be flawed. ;-) >> >> It's really hard to figure out where the disconnect is here. It is >> so completely obvious that the simple algorithm I provided iterates >> the primes (i.e., lists them in order) that Rich simply must be >> attaching an entirely different meaning to "iterates" than the rest >> of us. Does his talk of keys suggests that maybe he is getting >> database stuff confused with basic computability? > > 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. > > 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.    (01) I commend you on your powers of interpretation; he does indeed seem to be saying something like that. And, like pretty much everything he has said about Gödel's theorem and its proof, it is not even remotely true.    (02) > 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,    (03) Correct; specifically, where formula A is the string c1...cn of lexical items in the language of arithmetic, #c is the number assigned to lexical item c in the initial encoding, and p(m) is the mth prime, the the Gödel number of A is exp(p(1),#c1) x ... x exp(p(n),#cn). So long as one is careful about one's initial encoding, the same construction can be used to assign numbers to proofs, using the Gödel number #Am of the mth formula in a given proof instead of #cm.    (04) > the idea being you could then exploit their arithmetic structure to > tear them apart into their constituents.    (05) Correct, in virtue of the fundamental theorem of arithmetic one can recover the component formulas of a proof from its Gödel number and the component subformulas and lexical items of a formula from its Gödel number.    (06) > 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?    (07) Yes, pretty much, although you could also have non-primes representing lexical primitives.    (08) -chris    (09) _________________________________________________________________ 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    (010) ```
 Current Thread Re: [ontolog-forum] HOL decidability [Was: using SKOS for controlled values for controlledvocabulary], (continued)