ontolog-forum
[Top] [All Lists]

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

To: ontolog-forum@xxxxxxxxxxxxxxxx
From: Christopher Menzel <cmenzel@xxxxxxxx>
Date: Wed, 13 Oct 2010 18:57:38 -0500
Message-id: <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)

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