[Top] [All Lists]

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

To: ontolog-forum@xxxxxxxxxxxxxxxx
From: Christopher Menzel <cmenzel@xxxxxxxx>
Date: Tue, 12 Oct 2010 21:41:16 -0500
Message-id: <4CB51C4C.3050708@xxxxxxxx>
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
uncorrected.    (01)

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.      (02)

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.    (03)

> Godel showed that there are theorems which though true cannot be
> proven,       (04)

No, he didn't.   First of all, theorems are by definition statements
that have been proved.  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.    (05)

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.    (06)

> and theorems which though false cannot be disproved, all based
> on the primes.    (07)

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 one to represent the proof theoretic apparatus of
S in S itself as actual functions and relations on the numbers.  Thus,
given such an encoding, any system of arithmetic (so long as it includes
that certain minimal amount of arithmetic noted above) is able, in an
indirect sense, to "talk about itself"; in particular, it becomes
possible to construct a sentence -- known as the Gödel sentence for the
system -- that "says of itself" that it is not provable in the system.    (08)

Now, here is the point your are confused about: Gödel himself used the
primes (in an extraordinarily clever and beautiful way) in his own
arithmetization but there is *nothing* about Gödel's result per se that
depends in any way upon that particular method; there are plenty of
alternative encodings available that do not use the primes at all.
Nothing about Gödel's result, therefore, is "based on the primes" and
any inferences you draw from this misinformation are simply nonsense.    (09)

You're 0-for-2 here, dude.  Really, you should study up on this stuff
before you start pontificating about it in public.    (010)

-chris    (011)

**The language of arithmetic is a language that contains the numeral 0
and function symbols for the successor, addition, and multiplication
operations).  "*The* language" is a bit of misnomer, as there are first-
and higher-order versions and, moreover, rather different languages that
amount to the same thing.  But such details aren't really important
here.    (012)

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    (013)

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