[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 20:18:09 -0700
Message-id: <20101013031814.6013E138CD8@xxxxxxxxxxxxxxxxx>

Hi Chris,


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 Christopher Menzel
Sent: Tuesday, October 12, 2010 7:41 PM
To: ontolog-forum@xxxxxxxxxxxxxxxx
Subject: Re: [ontolog-forum] HOL decidability [Was: using SKOS for controlled values for controlledvocabulary]


Well, Gödel's theorem is a different topic, and one rather dearer to

my heart than higher-order logic.  I can't let Rich's errors here go



On 12/10/2010 6:48 PM, Rich Cooper wrote:

> John wrote:

>> 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. 


Of course there is.  For any given number n>1, it is easy to test

whether n is prime.  For a particularly crude algorithm, for each i<n

(i>1), look for a number j<n (j>1) such that ij=n.  If you fail to find such an i, then n is prime.  To construct a list of the primes, apply the above procedure to each number in turn, starting with 2, adding the primes you discover to the list as you go.  This informal procedure is easily expressed formally as a recursive function; one typically demonstrates this in the first week or two of a course on computability.


RC: I didn’t say there was no way to calculate them; I said there is no function that iterates them.  And your algorithm above iterates integers till it starts to factor, then continues to factor forever without returning if the number is unfactorable (i.e., if its prime).  Your program does not iterate primes. 


> Godel showed that there are theorems which though true cannot be

> proven,  


No, he didn't.   First of all, theorems are by definition statements

that have been proved. 


RC: From Google:

Definition:A proposition that has been or is to be proved on the basis of certain assumptions Context:In Book 1 of Elements, Euclid's proposition 41 is the theorem "if a parallelogram has the same base with a triangle and is in the same parallels, then the parallelogram is double the triangle."


CM: So what you are trying to say is that Gödel

showed that there are arithmetical statements which, though true, cannot

be proven.  But that's not true either.  Provability is relative to a

system and *any* arithmetical statement can be proven in some system or

other -- just take that statement as an axiom.


RC: The “some system or other” is the whole point.  That is the part that you can’t iterate over for every observed case.  There are primes, remember, and you will encounter them in iteration of supersets of the primes.


CM: Here's what Gödel proved: Given any consistent, decidable set S of

axioms in the language of arithmetic** capable of proving a certain

minimal amount of arithmetic, there will be statements in the language

that are neither provable nor disprovable *in S*.  From this it follows

that, for any such set S, there are statements that are true in the

natural numbers but which S cannot prove.


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.   


> and theorems which though false cannot be disproved, all based

> on the primes.


CM: This is just nonsense.  The key to Gödel's result, for a given system S,

is the "arithmetization" of S's syntax, which refers to any method of

encoding the terms and formulas of S (and, indeed, sequences of such) as

numbers.  This enables, not requires, one to represent the proof theoretic apparatus of S in S itself as actual functions and relations on the numbers. 


RC: I didn’t say anything about defining S in S itself, you did, and your formulation of Godel is not the only way to formulate it.  So by enabling self reference, it’s nice that you have moved ahead of the conversation, but not relevant to the issue at hand, which neither requires nor disallows self reference.  


Perhaps you should completely read posts before you reply. 


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>