Hi Chris,
Comments below,
-Rich
Sincerely,
Rich Cooper
EnglishLogicKernel.com
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
uncorrected.
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."
school.discoveryeducation.com/lessonplans/programs/conceptsInGeometry/
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.
-Rich