ontolog-forum
[Top] [All Lists]

Re: [ontolog-forum] HOL decidability [Was: using SKOS forcontrolled valu

To: "[ontolog-forum]" <ontolog-forum@xxxxxxxxxxxxxxxx>
From: "doug foxvog" <doug@xxxxxxxxxx>
Date: Fri, 15 Oct 2010 01:56:01 -0400 (EDT)
Message-id: <60245.71.178.11.66.1287122161.squirrel@xxxxxxxxxxxxxx>
On Thu, October 14, 2010 13:15, Rich Cooper said:
> Hi Doug,    (01)

> Thanks for you post, you seem to be honestly trying to understand what I
> meant by the statement "there is no function that can iterate the primes",
> and perhaps I should have originally said "directly, without iterating
> other types", which seems to have set off this mess.
>
> The point is that there is no function which takes primes as its domain
> and ranges over the primes.    (02)

?
Any function that took primes as its range would range over them.    (03)

>  For example, you could write a loop like this:
>
> For I := 2,3,5,7,11,13,...
>
> Do f(I);
>
> Which would loop the domain of f(I) over the primes,
> but only in a fixed set
> of primes given at compile time, not over an infinite set of primes,
> limited only by computer word length precision.    (04)

If we were limited by computer word length precision, we could do this
with the fixed set of primes that were at most that precision.    (05)

> Your example function    (06)

> G(I) := [calculate new value of nextPrime];    (07)

> is a good example because it does not exist as an iterator.    (08)

It was inside the iteration.  It was not the iterator    (09)

> There is no
> G(I) which will directly calculate the Ith prime (without ineffectively    (010)

I think you mean "inefficiently".    (011)

> iterating over something other than primes in an inner loop), as in:    (012)

>       I := 1;
>       Do G(I);    (013)

It could iterate over a table of primes which was being filled by a
different thread.  The iterator would merely step through the array.
It could block, not loop, if the array were not full enough.    (014)

Since you are not interested in computing the primes, but merely
iterating over a list of them, would this be sufficient?    (015)

> I didn't say that primes are not computable; I said there is no iterator
> of them.    (016)



> As to expressiveness, the idea is to generate an infinite set of sentences
> based on combinations of a finite set of primitives, such as AND, OR, NOT,
> and a finite set of variables and constant symbols.    (017)

If this were randomly generated, most combinations would be syntactically
invalid.  I'm presuming your generator would only generate syntactically
valid sentences.    (018)

> Associating this sequence of primes
[1]
> with expressions made up of the primitives of logic
[2]
>    (e.g., AND, OR, NOT and variables),
> you can generate an infinite number of primes
[3]
>    (which by definition are not factorable) and which
> cannot be expressed as combinations of the primitive symbols.    (019)

Forgive me, but i can not make sense out of this sentence.
If
 [1] is the sequence of all primes
    and
 [2] is the sequence of all combinations of primitive logic symbols
    and
 every element of [1] is associated with an element of [2]
then
 one can generate an infinite set of primes [3]
   (which would be a subset of [1])
 such that the elements of [3] can not be expressed as combinations
  of primitive symbols.    (020)

Trivially, this is so, since no integers (including primes) can be so
expressed.  But you can not mean that the elements of [3] are not
associated with the elements of [2], since [3] is a subset of [1] and
each element of [1] is by definition associated with an element of [2].    (021)


However, this seems like a discussion of syntax, not of proof.    (022)


I'm guessing that what you intended was to associate each of a finite set
of axioms with a separate prime.  You then map each possible proof with
the product of the axioms which are used in that proof.  Simplification
rules are also axioms that are mapped to primes.    (023)

Using this method, every statement that can be proved or disproved maps
to (at least) one non-prime positive integer.  And it doesn't matter if
multiple statements might map to the same non-prime positive integer.
Note that mathematically, A*B = B*A, but if A' and B' are the sentences
that A & B map to, "A' B'" is a different sentence from "B' A'".    (024)

Your conclusion appears to be that since there are an infinite number of
primes, each of them is mapped to a syntactically valid sentence that
can be neither proved nor disproved.    (025)

However, since you haven't given a rule as to how sentences are mapped
to positive integers, you have not shown that even one prime that was
not originally assigned an axiom is mapped to by a syntactically valid
sentence.    (026)



> The result demonstrates that the newly generated primes are unique
> expressions that cannot be formed from combinations of the finite set of
> FOL primitives.    (027)

The primes are not expressions.  You presumably mean that they are
mapped to such expressions.  However, you have not provided any mapping
or demonstrated that one exists.  You have not shown that any integers
map to unique expressions (except the primes which have been defined as
being mapped to unique sentences).    (028)

> The only feasible conclusion is that there is an infinite number of
> sentences (since there is an infinite number of primes) which CANNOT be
> expressed as combinations of the finite starting set of AND, OR, NOT and
> variables and constants.    (029)

Without defining a mapping of positive integers to logical sentences
that will have the property of primes being mapped to sentences that
are non-provable true or false, this does not follow.    (030)

> Therefore there are expressions (like in Escher's drawings) which are not
> well formed, yet which express sentences that have meaning to the
> observer.    (031)

Were you referring to whether sentences are well formed, instead of
provable?  Similar points apply to those which i brought up above.
And how do you ensure that primes are mapped to sentences that have
meaning to the observer, but are not well formed?    (032)

> Just not to observers who refuse to look at them - the observer has to
> understand that the Escher drawings are expressions which are not in
> reality, but which do have meaning nonetheless.    (033)

I fail to see what what that has to do with primes or expressions in
a formal logic.    (034)

> Encapsulation of a function that iterates other things than primes is
> merely
> a distraction from the claim.  It doesn't change the fact that there is no
> DIRECT iterator of primes.    (035)

I also fail to see that the existence or not of an iterator of primes
(by any definition) has anything to do with the discussion of the
mapping of primes to logical sentences.    (036)

> Q.E.D.    (037)



> If anything looks strange to you, please comment.    (038)

It looks quite strange to me.  You need to explain your mapping of
sentences to integers in such a way that each integer maps to one or
more sentences and that those which the composite numbers map to
can be proven or disproven, while those which the primes map to can
not.    (039)

> I can see you are posting in good faith.    (040)

I am sincerely trying to understand what you are writing.    (041)

-- doug    (042)

> -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 doug foxvog
> Sent: Thursday, October 14, 2010 5:46 AM
> To: [ontolog-forum]
> Subject: Re: [ontolog-forum] HOL decidability [Was: using SKOS
> forcontrolled
> values for controlledvocabulary]
>
>
>
> It appears that Rich Cooper's definition of "iterate" is to loop with
>
> a counter that advances from one element of a set to the next.  It is
>
> unclear what restriction there is on the step that does the advancement.
>
> It probably has to be a fixed value (like a FORTRAN DO statement), but
>
> may not be restricted to the number 1.  Rich, do you allow positive
>
> integers other than 1, negative integers, and non-integers as iterative
>
> steps?  It evidently does not include taking the next element from a
>
> list.
>
>
>
> Rich Cooper's "iterate" does not cover the more advanced C FOR statement
>
> which allows an arbitrary reassignment of the loop counter for each
>
> step of the loop.  If this were allowed, the following would be an
>
> iteration of primes.
>
>   nextPrime = 2;
>
>   for (i = 2, i < upperLimit, i = nextPrime)
>
>     [calculate new value of nextPrime];
>
>
>
> If the loop counter for Rich Cooper's iterate has to be a fixed value,
>
> the statement that "there is no function that can iterate the primes
>
> directly" seems to simply mean that there is not a fixed integer
>
> difference between all primes.
>
>
>
> Rich, please clarify if this your meaning of the term "iterate", or
>
> if not, what restrictions you place on the assignment of the next
>
> value in the iteration.  If it has to be taking the next value from
>
> a list, wouldn't the list of calculated primes be acceptable?  That
>
> could have been done in the 1970s with C, although not in the 1950s
>
> with FORTRAN II.  E.g.:
>
>   sieve[0] = 2;
>
>   primeCounter = 0;
>
>   for (i = sieve[primeCounter++], i < upperLimit,
>
>        i = sieve[primeCounter++])
>
>     <calculate next prime and store it into sieve[primeCounter]>;
>
>
>
> My definition of "iterate" would consider this to iterate through the
>
> primes.
>
>
>
> == doug foxvog
>
>
>
> On Thu, October 14, 2010 1:19, Randall R Schulz said:
>
>> On Wednesday October 13 2010, Rich Cooper wrote:
>
>
>
>>> The whole point is that there is no function that will iterate the
>
>>> primes directly.  The code you wrote will EVENTUALLY iterate primes
>
>>> as a BYPRODUCT of iterating integers and testing them, but that code
>
>>> doesn't produce each prime directly, once per iteration, without
>
>>> iterating other types.
>
>>
>
>> Then there is no iterator that directly iterates anything. It's all
>
>> by-products of something else down to the level of electrons and holes
>
>> cascading through the semiconductor material from which transistors are
>
>> fabricated. And while the electrons are (putatively) primitive,
>
>> semiconductor materials are aggregates and the phenomenon of
>
>> semiconductivity is a bulk property, so there are deeper levels even
>
>> than that.
>
>>
>
>>
>
>>> The method you are using is often called Eratosthenes' Sieve, which
>
>>> is a well known method to calculate primes, but NOT to iterate them.
>
>>>   The difference is in what is being enumerated inside the code.
>
>>
>
>> I gotta' say, this sounds like an entirely specious distinction to me.
>
>> But what do I know? I've only been writing computer code for 34 years.
>
>>
>
>>
>
>>> -Rich
>
>>
>
>>
>
>> Randall Schulz
>
>>
>
>> _________________________________________________________________
>
>> 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
>
>>
>
>>
>
>
>
>
>
> =============================================================
>
> doug foxvog    doug@xxxxxxxxxx   http://ProgressiveAustin.org
>
>
>
> "I speak as an American to the leaders of my own nation. The great
>
> initiative in this war is ours. The initiative to stop it must be ours."
>
>     - Dr. Martin Luther King Jr.
>
> =============================================================
>
>
>
> =============================================================
>
> doug foxvog    doug@xxxxxxxxxx   http://ProgressiveAustin.org
>
>
>
> "I speak as an American to the leaders of my own nation. The great
>
> initiative in this war is ours. The initiative to stop it must be ours."
>
>     - Dr. Martin Luther King Jr.
>
> =============================================================
>
>
>
>
>
> _________________________________________________________________
>
> 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
>
>
>
>    (043)


=============================================================
doug foxvog    doug@xxxxxxxxxx   http://ProgressiveAustin.org    (044)

"I speak as an American to the leaders of my own nation. The great
initiative in this war is ours. The initiative to stop it must be ours."
    - Dr. Martin Luther King Jr.
=============================================================    (045)


_________________________________________________________________
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    (046)

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