On 5/1/2022 12:24 AM, Jeff Barnett wrote:
> On 4/30/2022 9:15 PM, olcott wrote:
>> On 4/30/2022 10:11 PM, Richard Damon wrote:
>>> On 4/30/22 10:56 PM, olcott wrote:
>>>> On 4/30/2022 9:38 PM, Richard Damon wrote:
>>>>> On 4/30/22 10:21 PM, olcott wrote:
>>>>>> On 4/30/2022 9:00 PM, Richard Damon wrote:
>>>>>>> On 4/30/22 9:42 PM, olcott wrote:
>>>>>>>> On 4/30/2022 8:08 PM, Richard Damon wrote:
>>>>>>>>> On 4/30/22 3:02 AM, olcott wrote:
>>>>>>>>>> LP := ~True(LP) is translated to Prolog:
>>>>>>>>>>
>>>>>>>>>> ?- LP = not(true(LP)).
>>>>>>>>>> LP = not(true(LP)).
>>>>>>>>>>
>>>>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>> false.
>>>>>>>>>>
>>>>>>>>>> (SWI-Prolog (threaded, 64 bits, version 7.6.4)
>>>>>>>>>>
>>>>>>>>>> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>
>>>>>>>>> Since it isn't giving you a "syntax error", it is probably
>>>>>>>>> correct Prolog. Not sure if your interpretation of the results
>>>>>>>>> is correct.
>>>>>>>>>
>>>>>>>>> All that false means is that the statement
>>>>>>>>>
>>>>>>>>>
>>>>>>>>> LP = not(true(LP))
>>>>>>>>>
>>>>>>>>> is recursive and that Prolog can't actually evaluate it due to
>>>>>>>>> its limited logic rules.
>>>>>>>>>
>>>>>>>>
>>>>>>>> That is not what Clocksin & Mellish says. They say it is an
>>>>>>>> erroneous "infinite term" meaning that it specifies infinitely
>>>>>>>> nested definition like this:
>>>>>>>
>>>>>>> No, that IS what they say, that this sort of recursion fails the
>>>>>>> test of Unification, not that it is has no possible logical meaning.
>>>>>>>
>>>>>>> Prolog represents a somewhat basic form of logic, useful for many
>>>>>>> cases, but not encompassing all possible reasoning systems.
>>>>>>>
>>>>>>> Maybe it can handle every one that YOU can understand, but it
>>>>>>> can't handle many higher order logical structures.
>>>>>>>
>>>>>>> Note, for instance, at least some ways of writing factorial for
>>>>>>> an unknown value can lead to an infinite expansion, but the
>>>>>>> factorial is well defined for all positive integers. The fact
>>>>>>> that a "prolog like" expansion operator might not be able to
>>>>>>> handle the definition, doesn't mean it doesn't have meaning.
>>>>>>>
>>>>>>
>>>>>> It is really dumb that you continue to take wild guesses again the
>>>>>> verified facts.
>>>>>>
>>>>>> Please read the Clocksin & Mellish (on page 3 of my paper) text
>>>>>> and eliminate your ignorance.
>>>>>>
>>>>>
>>>>> I did. You just don't seem to understand what I am saying because
>>>>> it is above your head.
>>>>>
>>>>> Prolog is NOT the defining authority for what is a valid logical
>>>>> statement, but a system of programming to handle a subset of those
>>>>> statements (a useful subset, but a subset).
>>>>>
>>>>> The fact that Prolog doesn't allow something doesn't mean it
>>>>> doesn't have a logical meaning, only that it doesn't have a logical
>>>>> meaning in Prolog.
>>>> In this case it does. I have spent thousands of hours on the
>>>> semantic error of infinitely recursive definition and written a
>>>> dozen papers on it. Glancing at one of two of the words of Clocksin
>>>> & Mellish does not count as reading it.
>>>
>>> And it appears that you don't understand it, because you still make
>>> category errors when trying to talk about it.
>>>
>>>>
>>>> BEGIN:(Clocksin & Mellish 2003:254)
>>>> Finally, a note about how Prolog matching sometimes differs from the
>>>> unification used in Resolution. Most Prolog systems will allow you
>>>> to satisfy goals like:
>>>>
>>>>    equal(X, X).?-
>>>>    equal(foo(Y), Y).
>>>>
>>>> that is, they will allow you to match a term against an
>>>> uninstantiated subterm of itself. In this example, foo(Y) is matched
>>>> against Y, which appears within it. As a result, Y will stand for
>>>> foo(Y), which is foo(foo(Y)) (because of what Y stands for), which
>>>> is foo(foo(foo(Y))), and so on. So Y ends up standing for some kind
>>>> of infinite structure.
>>>> END:(Clocksin & Mellish 2003:254)
>>>>
>>>> foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))))))
>>>>
>>>
>>> Right. but some infinite structures might actually have meaning.
>> Not in this case, it is very obvious that no theorem prover can
>> possibly prove any infinite expression. It is the same thing as a
>> program that is stuck in an infinite loop.
>
> Richard wrote and the asshole (PO) snipped
> ------------------------------------------
> Right. but some infinite structures might actually have meaning. The
> fact that Prolog uses certain limited method to figure out meaning
> doesn't mean that other methods can't find the meaning.
>

The question is not whether some infinite structures have meaning that
is the dishonest dodge of the strawman error.

The question is whether on not the expression at hand has meaning or is
simply semantically incoherent. I just posted all of the Clocksin &
Mellish text in my prior post to make this more clear.

This example expanded from Clocksin & Mellish conclusively proves that
some expressions of language are incorrect:

foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))

> Just like:
>
> Fact(n) := (N == 1) ? 1 : N*Fact(n-1);
>
> if naively expanded has an infinite expansion.
>
> But, based on mathematical knowledge, and can actually be proven from
> the definition, something like Fact(n+1)/fact(n), even for an unknown n,
> can be reduced without the need to actually expend infinite operations.
>
> Note, this is actual shown in your case of H(H^,H^). Yes, if H doesn't
> abort its simulation, then for THAT H^, we have that H^(H^) is
> non-halting, but so is H(H^,H^), and thus THAT H / H^ pair fails to be a
> counter example
>
> When you program H to abort its simulation of H^ at some point, and
> build your H^ on that H, then H(H^,H^), will return the non-halting
> answer, and H^(H^) when PROPERLY run or simulated halts, because H has
> the same "cut off" logic at the factorial above.
>
> The naive expansion thinks it is infinite, but the correct expansion
> sees the cut off and sees that it is actually finite.
> ----------------------------------------------------------------------
>
> A good symbolic manipulation system or a theorem prover with appropriate
> axioms and rules of inference could surely handle forms such as
> Fact(n+1)/fact(n) without breathing hard. It is only you, an ignorant
> fool, who seems to think that the unthinking infinite unrolling of a
> form must occur. Only you would think that a solver system would
> completely unroll a form before analyzing it and applying
> transformations to it.
>
> Son, it don't work that way (unless you are defining and making a mess
> trying to write the system yourself). Systems usually have rules that
> make small incremental transformations and usually search breadth first
> with perhaps a limited amount of depth first interludes. If they don't
> use a breadth first strategy, they will not be able to claim the
> completeness property. (See resolution theorem prover literature for
> some explanation. You wont understand it but you can cite as if you did!)
>
> Richard was trying to explain this to you in the snipped portion I
> recited just above. Question for Peter holding his pecker: How do you
> always and I mean always manage to delete the part of a message you
> respond too that addresses the point you now try to make?
>
> A typically subsequence you might see in the trace: would include in
> order but not necessarily consecutively:
>    Fact(n+1)/Fact(n)
>    (n+1)*Fact(n)/Fact(n)
>    (n+1)
> Some interspersed terms such as Fact(n+1)/(n*Fact(n-1)) would be found
> too. In some circumstances, these other terms might be helpful. A
> theorem prover or manipulator does all of this, breadth first, hoping to
> blindly stumble on a solution. You can provide heuristics that might
> speed up the process but no advice short of an oracle will get you even
> one more result. (Another manifestation of HP.) It's the slow grinding
> through the possibilities that guarantees that if a result can be found,
> it will be found. And all the theory that you don't understand says
> that's the best you can do.
>
> Ben and I disagree on reasons for your type of total dishonesty. He
> thinks that you are so self deluded that you actual believe what you are
> saying; that you are so self deluded that the dishonest utterances are
> just your subconscious protecting your already damaged ego. To that, I
> say phooey; you are just a long term troll who lies a lot about math,
> about your history and health, and about your accomplishments.
>
> I don't believe that you will read this before you start to respond but
> that's okay. Understanding is not required. Neither is respect in either
> direction.

--
Copyright 2022 Pete Olcott

"Talent hits a target no one else can hit;
Genius hits a target no one else can see."
Arthur Schopenhauer