On 5/1/22 12:05 PM, polcott wrote:
> On 5/1/2022 9:39 AM, Ben wrote:
>> Mr Flibble <fli...@reddwarf.jmc> writes:
>>
>>> Recursive definitions are fine, infinitely recursive definitions (such
>>> as The Halting Problem) are INVALID.
>>
>> (1) The halting problem is not an infinitely recursive definition.
>>
>> (2) Infinitely recursive definitions are often fine. For example, the
>> list of Fibonacci numbers:
>>
>
> This type is never fine: // Adapted from Clocksin & Mellish
> foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))
Depends on the definition of foo.
If foo is the function "fact" I have presented, then the unwinding
becomes exactly that to a too dumb naive expansion.
Thus "never" is incorrect.
>
> Because Gödel says
> 14 Every epistemological antinomy can likewise be used for a similar
> undecidability proof
>
> G ↔ ¬Provable(F, G) is an epistemological antinomy therefore it is
> necessarily sufficiently equivalent to his G.
>
> Likewise with this one: LP ↔ ¬True(LP)
> It can be evaluated as semantically incorrect without the need to define
> True(). No matter how True() is defined LP ↔ ¬True(LP) is semantically
> incorrect because it specifies this:
>
> LP ↔ ¬True(¬True(¬True(¬True(¬True(¬True(¬True(¬True(LP))))))))
> and Prolog can detect and reject this with unify_with_occurs_check.
Because Prolog is too limited to be able to fully handle this sort of
recursion. Prolog apparently can't handle the recursive definition of
fact(n), which just proves that its rejection of something as
"infinitely recursive" is NOT "Proof" that it is invalid.