On 5/1/22 7:35 AM, olcott wrote:
> 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(...))))))))))))

No, not "incorrect", just "can't be handled by Prolog".

If foo is my fact() function, it is definitely "defined".

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