Is this correct Prolog?

[olcott]

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



--
Copyright 2022 Pete Olcott

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

[Richard Damon]

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.

I will condition this answer on the fact that I am not a prolog
specialist, but just reading the manual and providing basic
understanding, which I am not sure of your ability to do so.

[olcott]

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:

LP := ~True(LP) specifies:
~True(~True(~True(L~True(L~True(...))
The ellipses "..." mean "on and on forever"

One half a page of the Clocksin & Mellish text is quoted on page (3) of
my paper:

https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence

> I will condition this answer on the fact that I am not a prolog
> specialist, but just reading the manual and providing basic
> understanding, which I am not sure of your ability to do so.

[olcott]

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.

I asked the question incorrectly, what I really needed to know is
whether or not the Prolog correctly encodes this logic sentence:
LP := ~True(LP)

x := y means x is defined to be another name for y
https://en.wikipedia.org/wiki/List_of_logic_symbols

[Richard Damon]

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.

[olcott]

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.

>>
>> LP := ~True(LP) specifies:
>> ~True(~True(~True(L~True(L~True(...))
>> The ellipses "..." mean "on and on forever"
>>
>> One half a page of the Clocksin & Mellish text is quoted on page (3)
>> of my paper:
>>
>> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
>>
>>
>>> I will condition this answer on the fact that I am not a prolog
>>> specialist, but just reading the manual and providing basic
>>> understanding, which I am not sure of your ability to do so.
>>
>>
>

[Richard Damon]

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.

The inability of Prolog to "Unify" the expression, does not mean the
expression doesn't have logical meaning, just that PROLOG can't derive
meaning from the expression.

The Halting Problem and the incompleteness proofs never claims that they
is designed for the subset of logic that is Prolog, and in fact they may
be implicitly denying that, as I don't think Prolog handles enough
complexity of logic to reach the threshold needed to express "G" in
Godel's proof. (Your need to "simplify" it, is indicative of this, and
shows you don't understand the actual proof).

This means that the fact that Prolog rejects unification of the
statements doesn't actually say that much, just that the statement isn't
of the type that Prolog can fully process.

[olcott]

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.

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

[Richard Damon]

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. The
fact that Prolog uses certain limited method to figure out meaning
doesn't mean that other methods can't find the meaning.

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.

[olcott]

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.

[olcott]

On 4/30/2022 8:53 PM, André G. Isaak wrote:

> On 2022-04-30 19:47, 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.
>>
>> I asked the question incorrectly, what I really needed to know is
>> whether or not the Prolog correctly encodes this logic sentence:
>> LP := ~True(LP)
>

> Since that isn't a 'logic sentence', no one can answer this.
>
> André
>
>

What about this one?
LP ↔ ¬True(LP) // Tarski uses something like this
https://liarparadox.org/Tarski_275_276.pdf

or this one?
G ↔ ¬(F ⊢ G)

[Jeff Barnett]

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.

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

[olcott]

On 5/1/2022 4:24 AM, Mikko wrote:
> On 2022-04-30 18:15:19 +0000, Aleksy Grabowski said:
>
>> I just want to add some small note.
>>
>> This "not(true(_))" thing is misleading.
>> Please note that it is *not* a negation.
>> Functionally it is equivalent to:
>>
>> X = foo(bar(X)).
>
> That's correct. Prolog language does not give any inherent semantics to
> data structures. It only defines the execution semantics of language
> structures and standard library symbols. Those same synbols can be used
> in data structures with entirely different purposes.
>
> Mikko
>

negation, not, \+
The concept of logical negation in Prolog is problematical, in the sense
that the only method that Prolog can use to tell if a proposition is
false is to try to prove it (from the facts and rules that it has been
told about), and then if this attempt fails, it concludes that the
proposition is false. This is referred to as negation as failure.

http://www.cse.unsw.edu.au/~billw/dictionaries/prolog/negation.html
This is actually a superior model to convention logic in that it only
seeks to prove not true, thus detects expressions of language that are
simply not truth bearers.


Expressions of (formal or natural) language that can possibly be
resolved to a truth value are [truth bearers].

There are only two ways that an expression of language can be resolved
to a truth value:
(1) An expression of language is assigned a truth value such as "cats
are animals" is defined to be true.

(2) Truth preserving operations are applied to expressions of language
that are known to be true. {cats are animals} and {animals are living
things} therefore {cats are living things}. Copyright 2021 PL Olcott

[olcott]

On 5/1/2022 4:26 AM, Mikko wrote:

> On 2022-04-30 21:08:05 +0000, olcott said:
>
>> negation, not, \+
>> The concept of logical negation in Prolog is problematical, in the
>> sense that the only method that Prolog can use to tell if a
>> proposition is false is to try to prove it (from the facts and rules
>> that it has been told about), and then if this attempt fails, it
>> concludes that the proposition is false. This is referred to as
>> negation as failure.
>

> Note that the negation discussed above is not present in LP =
> not(true(LP)).
>
> Mikko
>

Is says that it is. It says that "not" is synonymous with \+.

[olcott]

On 5/1/2022 4:38 AM, Mikko wrote:
> On 2022-04-30 20:48:47 +0000, olcott said:
>
>> On 4/30/2022 4:31 AM, Mikko wrote:

>>> On 2022-04-30 07:02:23 +0000, olcott said:
>>>
>>>> LP := ~True(LP) is translated to Prolog:
>>>>
>>>> ?- LP = not(true(LP)).
>>>> LP = not(true(LP)).
>>>

>>> This is correct but to fail would also be correct.
>>>
>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>> false.
>>>
>>> unify_with_occurs_check must fail if the unified data structure
>>> would contain loops.
>>>
>>> Mikko
>>>
>>
>> The above is the actual execution of actual Prolog code using
>> (SWI-Prolog (threaded, 64 bits, version 7.6.4).
>
> Another Prolog implementation might interprete LP = not(true(LP))
> differently
> and still conform to the prolog standard.
>
>> According to Clocksin & Mellish it is not a mere loop, it is an
>> "infinite term" thus infinitely recursive definition.
>
> When discussing data structures, "infinite" and "loop" mean the same.
> The data structure is infinitely deep but contains only finitely many
> distinct objects and occupies only a finite amount of memory.
>

That is incorrect. any structure that is infinitely deep would take all
of the memory that is available yet specifies an infinite amount of memory.

>> I am trying to validate whether or not my Prolog code encodes the Liar
>> Paradox.
>
> That cannot be inferred from Prolog rules. Prolog defines some encodings
> like how to encode numbers with characters of Prolog character set but for
> more complex things you must make your own encoding rules.
>
> Mikko
>

This says that G is logically equivalent to its own unprovability in F
G ↔ ¬(F ⊢ G) and fails unify_with_occurs_check when encoded in Prolog.

[Richard Damon]

So you are sort of answering your own question. The model of logic that
Prolog handles isn't quite the same as "conventional" logic, in part due
to the way it (doesn't) define Logical Negation.

This seems to fit into your standard misunderstanding of things.

[Richard Damon]

As Jeff pointed out, your claim is shown false, that some statements
with infinite expansions can be worked with by some automatic solvers.
This just proves that you don't really understand the effects of
"recursion" and "self-reference", and perhaps a source of your error in
trying to reason about thing like this Halting Problem proof or Godels
Incompleteness Theory and his expression "G".

If something that is obviously undoable is your mind is shown to be in
fact doable, the problem isn't in the ability to do it, but in the
ability of your mind to understand. Your misconceptions don't change the
nature of reality, but reality proves you wrong.

[Richard Damon]

Nope, a tree that one branch points into itself higher up represents a
tree with infinite depth, but only needs a finite amount of memory.
Building such a structure may require the ability to forward declare
something or reference something not yet defined.

Some infinities have finite representation. You don't seem able to
understand that.

Yes, some naive ways of expanding them fail, but the answer to that is
you just don't do that, but need to use a less naive method.

[olcott]

On 5/1/2022 4:45 AM, Mikko wrote:

> On 2022-05-01 03:15:56 +0000, olcott said:
>
>> Not in this case, it is very obvious that no theorem prover can
>> possibly prove any infinite expression.
>

> Doesn't matter as you can't give an infinite expression to a theorem
> prover.
>
> Mikko
>

*You can and Prolog can detect and reject 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.

<inserted for clarity>
foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))
</inserted for clarity>

Note that, whereas they may allow you to construct something like this,
most Prolog systems will not be able to write it out at the end.
According to the formal definition of Unification, this kind of
“infinite term” should never come to exist. Thus Prolog systems that
allow a term to match an uninstantiated subterm of itself do not act
correctly as Resolution theorem provers. In order to make them do so, we
would have to add a check that a variable cannot be instantiated to
something containing itself. Such a check, an occurs check, would be
straightforward to implement, but would slow down the execution of
Prolog programs considerably. Since it would only affect very few
programs, most implementors have simply left it out 1.

1 The Prolog standard states that the result is undefined if a Prolog
system attempts to match a term against an uninstantiated subterm of
itself, which means that programs which cause this to happen will not
be portable. A portable program should ensure that wherever an occurs
check might be applicable the built-in predicate
unify_with_occurs_check/2 is used explicitly instead of the normal
unification operation of the Prolog implementation. As its name
suggests, this predicate acts like =/2 except that it fails if an occurs
check detects an illegal attempt to instantiate a variable.

END:(Clocksin & Mellish 2003:254)

Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog Using the
ISO Standard Fifth Edition, 254. Berlin Heidelberg: Springer-Verlag.

[olcott]

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

[olcott]

Prolog has a better model in that it can detect semantic paradoxes.
LP ↔ ¬True(LP) is correctly assessed as neither true nor false.

[olcott]

That is the dishonest dodge of the strawman error. The particular
expression at hand is inherently incorrect and thus any system that
proves it is a broken system.

> This just proves that you don't really understand the effects of
> "recursion" and "self-reference", and perhaps a source of your error in
> trying to reason about thing like this Halting Problem proof or Godels
> Incompleteness Theory and his expression "G".
>

foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))
The "..." indicates infinite expansion, thus this expression can never
be proved by any system.

> If something that is obviously undoable is your mind is shown to be in
> fact doable, the problem isn't in the ability to do it, but in the
> ability of your mind to understand. Your misconceptions don't change the
> nature of reality, but reality proves you wrong.

[olcott]

That is counter-factual. unify_with_occurs_check determines that it
would require infinite memory and then aborts its evaluation.

foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))
"..." indicates infinite depth, thus infinite string length.

> Some infinities have finite representation. You don't seem able to
> understand that.
>
> Yes, some naive ways of expanding them fail, but the answer to that is
> you just don't do that, but need to use a less naive method.
>

>
>>
>>>> I am trying to validate whether or not my Prolog code encodes the
>>>> Liar Paradox.
>>>
>>> That cannot be inferred from Prolog rules. Prolog defines some encodings
>>> like how to encode numbers with characters of Prolog character set
>>> but for
>>> more complex things you must make your own encoding rules.
>>>
>>> Mikko
>>>
>>
>> This says that G is logically equivalent to its own unprovability in F
>> G ↔ ¬(F ⊢ G) and fails unify_with_occurs_check when encoded in Prolog.
>>
>>
>

[Richard Damon]

On 5/1/22 7:28 AM, olcott wrote:
> On 5/1/2022 4:45 AM, Mikko wrote:
>> On 2022-05-01 03:15:56 +0000, olcott said:
>>
>>> Not in this case, it is very obvious that no theorem prover can
>>> possibly prove any infinite expression.
>>
>> Doesn't matter as you can't give an infinite expression to a theorem
>> prover.
>>
>> Mikko
>>
>
> *You can and Prolog can detect and reject it*

Which just shows PROLOG can't handle that sort of expression, not that
it logically doens't have a meaning.

So all Clocksin & Melish is saying is that such an expression fails in
PROLOG, not that it doesn't have a valid logical meaning.

The world is NOT Prolog, and I suspect Prolog isn't sufficient to handle
the logic needed to process the Godel Sentence, so can't be used to
disprove it.

[Richard Damon]

"Better" is as subjective word unless you define an objective criteria.
The fact that Prolog doesn't have the expresiability to actually write
the Godel sentence, means it can't actually be used to disprove it.

Misusing notations to show something is invalid logic.

I don't know Prolog well enough, but if the statement doesn't actaully
mean what you want it to mean to Prolog (as others have said), then the
fact that Prolog gives you the answer you want doesn't mean anything.

[olcott]

It correctly says that this is what the expression means:
foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))
Which means that it does not have a valid logical meaning.

> The world is NOT Prolog, and I suspect Prolog isn't sufficient to handle
> the logic needed to process the Godel Sentence, so can't be used to
> disprove it.

This says that G is logically equivalent to its own unprovability in F

G ↔ ¬Provable(F, G) and fails unify_with_occurs_check when encoded in
Prolog.

Because
14 Every epistemological antinomy can likewise be used for a similar
undecidability proof
then G ↔ ¬Provable(F, G) can likewise be used for a similar
undecidability proof.

[Richard Damon]

You misunderstand what it says. It says that it can't figure how to
express the statement without a cycle. That is different then taking
infinite memory. It only possibly implies infinite memory in a naive
expansion, which isn't the only method.

As was pointed out, the recursive factorial definition, if naively
expanded, becomes unbounded in size, but the recursive factorial
definition, to a logic system that understands recursion, is usable and
has meaning.

So all you have shown is that these forms CAN cause failure to some
forms of naive logic.

You are just stuck in your own false thinking, and have convinced
youself of a lie.

[olcott]

Semantically incorrect expressions of language are totally invisible to
conventional logic because conventional logic incorrectly assumes that
every expression is true or false. Prolog can detect expressions that
are neither true nor false, thus semantically erroneous.

> The fact that Prolog doesn't have the expresiability to actually write
> the Godel sentence, means it can't actually be used to disprove it.
>

This says that G is logically equivalent to its own unprovability in F

G ↔ ¬Provable(F, G) and fails unify_with_occurs_check when encoded in
Prolog.

Because
14 Every epistemological antinomy can likewise be used for a similar
undecidability proof
then G ↔ ¬Provable(F, G) can likewise be used for a similar
undecidability proof.

Prolog has a way to say {not provable} in its native tongue.

> Misusing notations to show something is invalid logic.
>
> I don't know Prolog well enough, but if the statement doesn't actaully
> mean what you want it to mean to Prolog (as others have said), then the
> fact that Prolog gives you the answer you want doesn't mean anything.

[Richard Damon]

So, factorials don't nave valid logical meaning? That is the logical
conclusion of your statement since fact does the same expansion.

Shows the capability of your logic system.

>
>> The world is NOT Prolog, and I suspect Prolog isn't sufficient to
>> handle the logic needed to process the Godel Sentence, so can't be
>> used to disprove it.
>
> This says that G is logically equivalent to its own unprovability in F
> G ↔ ¬Provable(F, G) and fails unify_with_occurs_check when encoded in
> Prolog.

"encoded in Prolog", nope, becuase G uses logic that is beyond the
expression of Prolog, you have changed the meaning of the statement.

You statement even has an undefined term F.

>
> Because
> 14 Every epistemological antinomy can likewise be used for a similar
> undecidability proof
> then G ↔ ¬Provable(F, G) can likewise be used for a similar
> undecidability proof.
>

FAIL. You clearly don't understand the meaning of the words, in
particular what it means to "use" something.

[olcott]

The expression inherently has an infinite cycle, making it erroneous.

> That is different then taking
> infinite memory. It only possibly implies infinite memory in a naive
> expansion, which isn't the only method.
>
> As was pointed out, the recursive factorial definition, if naively
> expanded, becomes unbounded in size, but the recursive factorial
> definition, to a logic system that understands recursion, is usable and
> has meaning.
>

Does not have an infinite cycle. It always begins with a finite integer
that specifies the finite number of cycles.

> So all you have shown is that these forms CAN cause failure to some
> forms of naive logic.
>

An infinite cycle is the same thing as an infinite loop inherently
incorrect.

> You are just stuck in your own false thinking, and have convinced
> youself of a lie.
>

You are simply ignoring key details. You are pretending that a finite
thing is an infinite thing.

>
>>
>> foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))
>> "..." indicates infinite depth, thus infinite string length.
>>
>>> Some infinities have finite representation. You don't seem able to
>>> understand that.
>>>
>>> Yes, some naive ways of expanding them fail, but the answer to that
>>> is you just don't do that, but need to use a less naive method.
>>>
>>
>>>
>>>>
>>>>>> I am trying to validate whether or not my Prolog code encodes the
>>>>>> Liar Paradox.
>>>>>
>>>>> That cannot be inferred from Prolog rules. Prolog defines some
>>>>> encodings
>>>>> like how to encode numbers with characters of Prolog character set
>>>>> but for
>>>>> more complex things you must make your own encoding rules.
>>>>>
>>>>> Mikko
>>>>>
>>>>
>>>> This says that G is logically equivalent to its own unprovability in F
>>>> G ↔ ¬(F ⊢ G) and fails unify_with_occurs_check when encoded in Prolog.
>>>>
>>>>
>>>
>>
>>
>

[Mr Flibble]

Are you mental? That definition isn't infinitely recursive as it
terminates when N equals 1 given a set of constraints on N (positive
integer greater or equal to 1).

/Flibble

[polcott]

Brilliantly well put.

[olcott]

On 5/1/2022 8:35 AM, André G. Isaak wrote:
> On 2022-05-01 05:40, olcott wrote:
>> On 5/1/2022 12:34 AM, André G. Isaak wrote:

>>> On 2022-04-30 22:49, olcott wrote:
>>>> On 4/30/2022 8:53 PM, André G. Isaak wrote:
>>>>> On 2022-04-30 19:47, 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.
>>>>>>
>>>>>> I asked the question incorrectly, what I really needed to know is
>>>>>> whether or not the Prolog correctly encodes this logic sentence:
>>>>>> LP := ~True(LP)
>>>>>
>>>>> Since that isn't a 'logic sentence', no one can answer this.
>>>>>
>>>>> André
>>>>>
>>>>>
>>>>
>>>> What about this one?
>>>> LP ↔ ¬True(LP)  // Tarski uses something like this
>>>

>>> That requires that you define some predicate 'True'. Presumably
>>> True(LP) must mean something other than LP or it would be purely
>>> redundant.
>>>
>>
>> For the purpose of verifying that it is semantically incorrect True()
>> can simply be an empty placeholder. The result is that no matter how
>> True() is defined the above logic sentence is semantically incorrect.
>
> You're missing my point. Unless you are claiming that there is a
> difference between 'x if and only if y' and 'x is true if and only if y
> is true', then there is no reason for such a predicate at all. The fact
> that you insist on including it suggests you *do* think there is a
> difference in meaning between these two examples. So what is that
> difference?
>
> But whatever it means, LP ↔ ¬True(LP) is either simply true or simply
> false. It is *not* the liar paradox. Most likely it is simply false
> since I assume LP ↔ ¬True(LP) is simply the same as LP ↔ ¬LP.
>
>>> LP ↔ ¬LP
>>>
>>> is simply false. It is not a translation of 'This sentence is false'.

>>>
>>>> https://liarparadox.org/Tarski_275_276.pdf
>>>>
>>>> or this one?
>>>> G ↔ ¬(F ⊢ G)
>>>

>>> As a statement of logic, no. As a statement in the metalanguage of
>>> logic, sure. As a paraphrase of Gödel, not exactly.
>>>
>>
>> G ↔ ¬Provable(F, G)
>
> If you want to paraphrase Gödel, you need both G and ⌈G⌉ to be present
> in your statement.
>
> André

>


That it not what 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 sufficient.

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.

[olcott]

On 5/1/2022 11:15 AM, André G. Isaak wrote:

> On 2022-05-01 09:57, polcott wrote:
>> On 5/1/2022 8:35 AM, André G. Isaak wrote:
>>> On 2022-05-01 05:40, olcott wrote:

>>>> On 5/1/2022 12:34 AM, André G. Isaak wrote:

>>>>> On 2022-04-30 22:49, olcott wrote:
>>>>>> On 4/30/2022 8:53 PM, André G. Isaak wrote:
>>>>>>> On 2022-04-30 19:47, 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.
>>>>>>>>
>>>>>>>> I asked the question incorrectly, what I really needed to know
>>>>>>>> is whether or not the Prolog correctly encodes this logic sentence:
>>>>>>>> LP := ~True(LP)
>>>>>>>
>>>>>>> Since that isn't a 'logic sentence', no one can answer this.
>>>>>>>
>>>>>>> André
>>>>>>>
>>>>>>>
>>>>>>
>>>>>> What about this one?
>>>>>> LP ↔ ¬True(LP)  // Tarski uses something like this
>>>>>

>>>>> That requires that you define some predicate 'True'. Presumably
>>>>> True(LP) must mean something other than LP or it would be purely
>>>>> redundant.
>>>>>
>>>>
>>>> For the purpose of verifying that it is semantically incorrect
>>>> True() can simply be an empty placeholder. The result is that no
>>>> matter how True() is defined the above logic sentence is
>>>> semantically incorrect.
>>>
>>> You're missing my point. Unless you are claiming that there is a
>>> difference between 'x if and only if y' and 'x is true if and only if
>>> y is true', then there is no reason for such a predicate at all. The
>>> fact that you insist on including it suggests you *do* think there is
>>> a difference in meaning between these two examples. So what is that
>>> difference?
>>>
>>> But whatever it means, LP ↔ ¬True(LP) is either simply true or simply
>>> false. It is *not* the liar paradox. Most likely it is simply false
>>> since I assume LP ↔ ¬True(LP) is simply the same as LP ↔ ¬LP.
>>>
>>>>> LP ↔ ¬LP
>>>>>
>>>>> is simply false. It is not a translation of 'This sentence is false'.
>>>>>

>>>>>> https://liarparadox.org/Tarski_275_276.pdf
>>>>>>
>>>>>> or this one?
>>>>>> G ↔ ¬(F ⊢ G)
>>>>>

>>>>> As a statement of logic, no. As a statement in the metalanguage of
>>>>> logic, sure. As a paraphrase of Gödel, not exactly.
>>>>>
>>>>
>>>> G ↔ ¬Provable(F, G)
>>>
>>> If you want to paraphrase Gödel, you need both G and ⌈G⌉ to be
>>> present in your statement.
>>>
>>> André
>>>
>>
>> That it not what this says:
>> 14 Every epistemological antinomy can likewise be used for a similar
>> undecidability proof
>

> That footnote says absolutely nothing about how to formalize Gödel's
> Theorem.
>

It says that Every epistemological antinomy can likewise be used for a
similar undecidability proof

thus even English epistemological antinomies such as the Liar antinomy
can be used.

Gödel says:
"There is also a close relationship with the “liar” antinomy"

>> G ↔ ¬Provable(F, G) is an epistemological antinomy therefore it is
>> necessarily sufficient.
>

> There is no antinomy involved in that formula, epistemological or
> otherwise.
>

Prolog disagrees.
To boil the Gödel proof down to its bare essence we use the simplest
Liar epistemological antinomy: LP ↔ ¬True(LP)

This way we don't need dozens pages of hundreds of formulas and Prolog
is smart enough to detect and reject it as erroneous.

?- LP = not(true(LP)).
LP = not(true(LP)).

?- unify_with_occurs_check(LP, not(true(LP))).
false.

False means that LP ↔ ¬True(LP) specifies:
¬True(¬True(¬True(¬True(¬True(¬True(¬True(¬True(¬True(¬True(...))))))))))

(SWI-Prolog (threaded, 64 bits, version 7.6.4)

> If you wish to know how to best formalize Gödel, simply read Gödel; he
> provides the proper formalization for you.

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

> There's nothing 'semantically incorrect' about it. It evaluates to
> false. It's not the Liar's Paradox.
>

?- unify_with_occurs_check(LP, not(true(LP))).
false.

false means that LP ↔ ¬True(LP) specifies:
¬True(¬True(¬True(¬True(¬True(¬True(¬True(¬True(¬True(¬True(...))))))))))

> The reason I keep asking you to define your 'True' predicate is simply
> that it seems utterly unnecessary and pointless.

Any logic sentence having the self-referential form of the Liar Paradox
specifies infinitely recursive definition, thus is semantically incorrect.

From Clocksin and Mellish:
equal(X, X).?-
equal(foo(Y), Y).

specifies:
foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))


> If you believe
> otherwise, then please explain what the difference between the following
> formulae might possibly be:
>

I never waste time carefully examining every possible permutation of an
idea because this would guarantee that I am dead long before my proof is
complete. That I have proved my point with one is them is entirely
sufficient. My example corresponds to the definitive example provided by
the worlds best experts on the Prolog language.

> (1) LP ↔ ¬True(LP)
> (2) True(LP) ↔ ¬True(LP)
> (3) LP ↔ ¬LP
> (4) True(LP) ↔ ¬LP
>
> André

[Richard Damon]

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

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

[Richard Damon]

But if you don't know N, you don't know when to terminate the expansion.

If all you know is that N is a positive integer, then you don't know
when to stop.

That is the issue, Fact of N isn't just defined for know values of N,
but you can do logic with unknow values (and especially with multiple
instances of Fact with related parameters).

[André G. Isaak]

On 2022-05-01 10:57, olcott wrote:
> On 5/1/2022 11:15 AM, André G. Isaak wrote:
>> On 2022-05-01 09:57, polcott wrote:

> It says that Every epistemological antinomy can likewise be used for a
> similar undecidability proof
>
> thus even English epistemological antinomies such as the Liar antinomy
> can be used.
>
> Gödel says:
> "There is also a close relationship with the “liar” antinomy"

Yes. There is a close *relationship* between his G and The Liar. That
does *not* mean that G *is* The Liar. It is not. But you refuse to read
Gödel's actual math to see the *very* significant differences between
the two.

Similarly one can construct sentences which bear a close relationship to
other antinomies. Again, that does not mean those sentences *are* those
antinomies.

You need to stop trying to analyze Gödel's footnotes as if this were
some exercise in literary analysis and focus on the actual math.

>>> G ↔ ¬Provable(F, G) is an epistemological antinomy therefore it is
>>> necessarily sufficient.
>>
>> There is no antinomy involved in that formula, epistemological or
>> otherwise.
>>
>
> Prolog disagrees.
> To boil the Gödel proof down to its bare essence we use the simplest
> Liar epistemological antinomy: LP ↔ ¬True(LP)

Again, that formula is not The Liar. That says that LP is true if and
only if LP is not true. Even a simple truth table suffices to show that
this statement is false. There is no self-reference involved in that
formula, and the self-reference is the key to The Liar.

> This way we don't need dozens pages of hundreds of formulas and Prolog
> is smart enough to detect and reject it as erroneous.

Whether Prolog likes something or not is irrelevant. Prolog can't even
deal with first order logic, let alone higher order logic. Prolog deals
with Horn clauses. It is a very simple system designed to deal with very
simple proofs. It's the wrong tool for dealing with substantive theorems
of math or logic.

> ?- LP = not(true(LP)).
> LP = not(true(LP)).
>
> ?- unify_with_occurs_check(LP, not(true(LP))).
> false.

Where in the above have you encoded the ↔ ?

As I note above, what Prolog has to say isn't particularly relevant, but
it is even *less* relevant if your Prolog doesn't even encode the
formula you're talking about.

<snip more junk about Prolog>

>
>> If you believe otherwise, then please explain what the difference
>> between the following formulae might possibly be:
>>
>
> I never waste time carefully examining every possible permutation of an
> idea because this would guarantee that I am dead long before my proof is
> complete. That I have proved my point with one is them is entirely
> sufficient. My example corresponds to the definitive example provided by
> the worlds best experts on the Prolog language.

This is a really simple question. It should consume no time at all. Let
me phrase my question in a more direct way: All I am asking is for you
to clarify whether your True() predicate is anything other than
syntactic sugar.

In logic an expression X evaluates to true if X is true. So True(X) and
X would seem to be identical. So why bother with this predicate at all?

>> (1) LP ↔ ¬True(LP)
>> (2) True(LP) ↔ ¬True(LP)
>> (3) LP ↔ ¬LP
>> (4) True(LP) ↔ ¬LP

André

--

To email remove 'invalid' & replace 'gm' with well known Google mail
service.

[Jeff Barnett]

I see that you, like the asshole, are snipping too. there was another
line just above: "if naively expanded has an infinite expansion." That
was the context of my remarks.

Also note that there isn't anything left that I wrote (other than the
partial quote of someone else above). So what does your remark apply to?
Your contribution sounds like a wounded Parrot squawking in the night. A
horrible sound, especially when trying to imitate human communications.

> Are you mental? That definition isn't infinitely recursive as it
> terminates when N equals 1 given a set of constraints on N (positive
> integer greater or equal to 1).

I take this as a sign that you might have a glimmer of understanding;
otherwise, why snip that particular line above? Ah! We know an other
jerk trolling for sport. I must say though, that I'm not ready to
upgrade you from ignoramus just yet - this was your first and only
visible sign of sentience so far. I'll reconsider if I see others.
--
Jeff Barnett

[Richard Damon]

You think? depends on what you know about the definition of foo.

Perhaps you can't do anything with the infinitely expanded version,
since you can't actually express it, but the self-referential version
might be able to be analyzed.

You problem is you seem to think if YOU can't understand it, it doesn't
have meaning, but that is NOT an actual fact. There seems to be MANY
things that you do not understand that are actually well established.
Maybe you need to get off your incorrect assumption that you are the
source of Truth.

[Richard Damon]

Incorrect, conventional logic understand that some statements are not
truth bearers. Now, a lot of rules are pre-conditioned on the assumption
that their inputs ARE truth bearers, so you need to be careful in just
applying rules to statements that they do not apply to.

>
>> The fact that Prolog doesn't have the expresiability to actually write
>> the Godel sentence, means it can't actually be used to disprove it.
>>
>
> This says that G is logically equivalent to its own unprovability in F
> G ↔ ¬Provable(F, G) and fails unify_with_occurs_check when encoded in
> Prolog.

No, that is NOT what G says.

>
> Because
> 14 Every epistemological antinomy can likewise be used for a similar
> undecidability proof
> then G ↔ ¬Provable(F, G) can likewise be used for a similar
> undecidability proof.

except that isn't G, so you are just starting from a false start, so
your logic doesn't mean anything (not that much of your logic ever means
anything because this seems a common error, you assume things that just
are not).

>
> Prolog has a way to say {not provable} in its native tongue.

Fine, but can it express the statement that Godel's G actually is, not
your over-simplification is.

[Richard Damon]

Maybe it just says that PROLOG can't express the statement without an
infinite cycle due to the limitiations in Prologs logic system?

Better logic systems can handle and work with statements that are
self-referential or recursive.

Your reliance on Prolog just limits the fields you can discuss. Like I
think Prolog isn't able to express all the properties of the Natural
Numbers, which means that it BY DEFINITION isn't capable of handling a
full incompleteness prooof.

>
>>  That is different then taking infinite memory. It only possibly
>> implies infinite memory in a naive expansion, which isn't the only
>> method.
>>
>> As was pointed out, the recursive factorial definition, if naively
>> expanded, becomes unbounded in size, but the recursive factorial
>> definition, to a logic system that understands recursion, is usable
>> and has meaning.
>>
>
> Does not have an infinite cycle. It always begins with a finite integer
> that specifies the finite number of cycles.

Nope. I can write Fact(n), where n is an unknow integer and do logic
with it.

Just like H(H^,H^) has a finite expansion if H will answer the question,
and thus does not have infinite recursion, and thus H^(H^) does not
either as it is a finite extension of the expansion of H(H^,H^).

Only your failure to inplement that limit makes it infinite, which just
proves that such an H never answers.

>
>> So all you have shown is that these forms CAN cause failure to some
>> forms of naive logic.
>>
>
> An infinite cycle is the same thing as an infinite loop inherently
> incorrect.
>

Yes, but a finite loop can expand infinitely if not done correctly or
naively. The fact that one method expanse something infinitely doesn't
mean the expression is in fact an infinte loop.

>> You are just stuck in your own false thinking, and have convinced
>> youself of a lie.
>>
>
> You are simply ignoring key details. You are pretending that a finite
> thing is an infinite thing.

Yes, any expansion of fact for a KNOWN n will be finite, but if n is not
known, generates what appears to be an infinite expansion that will
colapse to finite once a value is known.

Tell me how many cycles your logic is going to expand fact, and I will
give you an n that it didn't handle.

[olcott]

On 5/1/2022 12:59 PM, Mr Flibble wrote:
> On Sun, 1 May 2022 12:01:01 -0500
> olcott <No...@NoWhere.com> wrote:
>
>> On 5/1/2022 11:21 AM, André G. Isaak wrote:
>>> On 2022-05-01 10:08, olcott wrote:
>>>
>>> <snip>
>>>
>>> Why are you making the same reply twice under two different
>>> handles? A single reply should suffice.
>>>
>>> André
>>>
>>
>> I wanted Flibble to see what I said. He may have me on Plonk
>
> You are not in my kill file: I don't always reply to what you say
> because I either agree with what you are saying or the point is
> uninteresting to me.
>
> /Flibble
>

I do think that your idea of "category error" is a brilliant new insight
into pathological self-reference problems such as:
(1) The Halting Problem proofs
(2) Gödel's 1930 Incompleteness
(3) The 1936 Undefinability theorem

It very succinctly sums up the entire gist of the semantic error in all
of these cases. When it is summed up so effectively it becomes much
easier to see exactly what is going on. I have said that it is a
semantic error, you pointed out exactly what kind of semantic error.

[olcott]

On 5/1/2022 1:33 PM, André G. Isaak wrote:

> On 2022-05-01 12:28, olcott wrote:
>> On 5/1/2022 12:59 PM, Mr Flibble wrote:
>>> On Sun, 1 May 2022 12:01:01 -0500
>>> olcott <No...@NoWhere.com> wrote:
>>>
>>>> On 5/1/2022 11:21 AM, André G. Isaak wrote:
>>>>> On 2022-05-01 10:08, olcott wrote:
>>>>>
>>>>> <snip>
>>>>>
>>>>> Why are you making the same reply twice under two different
>>>>> handles? A single reply should suffice.
>>>>>
>>>>> André
>>>>
>>>> I wanted Flibble to see what I said. He may have me on Plonk
>>> You are not in my kill file: I don't always reply to what you say
>>> because I either agree with what you are saying or the point is
>>> uninteresting to me.
>>>
>>> /Flibble
>>>
>>
>> I do think that your idea of "category error" is a brilliant new
>> insight into pathological self-reference problems such as:
>> (1) The Halting Problem proofs
>> (2) Gödel's 1930 Incompleteness
>> (3) The 1936 Undefinability theorem
>>
>> It very succinctly sums up the entire gist of the semantic error in
>> all of these cases. When it is summed up so effectively it becomes
>> much easier to see exactly what is going on. I have said that it is a
>> semantic error, you pointed out exactly what kind of semantic error.
>

> So which categories are you claiming are involved? Claiming something is
> a 'category error' means nothing if you don't specify the actual
> categories involved.
>
> André
>

My original thinking was that (1) and (2) and the Liar Paradox all
demonstrate the exact same error. I only have considered (3) in recent
years, prior to that I never heard of (3).

The category error would be that none of them is in the category of
truth bearers. For Gödel's G and Tarski's p it would mean that the
category error is that G and p are not logic sentences.
https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)

https://liarparadox.org/Tarski_275_276.pdf

My current thinking on (1) is that a TM is smart enough to see this
issue and report on it.

[Richard Damon]

Well, for Godel's G, since it is just that a statement that some
statement x is provable, and the provability of a statement is ALWAYS a
Truth Bearer, as you can't prove a non-sense sentence, so provable(x)
would be false is x is not a valid statement, G is by definition a Truth
Bearer.

[olcott]

On 5/1/2022 2:22 PM, André G. Isaak wrote:

> On 2022-05-01 13:00, olcott wrote:
>> On 5/1/2022 1:33 PM, André G. Isaak wrote:
>
>>> So which categories are you claiming are involved? Claiming something
>>> is a 'category error' means nothing if you don't specify the actual
>>> categories involved.
>>>
>>> André
>>>
>>
>> My original thinking was that (1) and (2) and the Liar Paradox all
>> demonstrate the exact same error. I only have considered (3) in recent
>> years, prior to that I never heard of (3).
>>
>> The category error would be that none of them is in the category of
>> truth bearers. For Gödel's G and Tarski's p it would mean that the
>> category error is that G and p are not logic sentences.
>> https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)
>

> And how can you possibly justify your claim that Gödel's G is not a
> truth bearer?
>

Do I have to say the same thing 500 times before you bother to notice
that I said it once?

14 Every epistemological antinomy can likewise be used for a similar
undecidability proof

Therefore LP ↔ ~True(LP) can be used for a similar undecidability proof,
and LP ↔ ~True(LP) is clearly semantically ill-formed.

?- LP = not(true(LP)).
LP = not(true(LP)).

?- unify_with_occurs_check(LP, not(true(LP))).

false. // false means semantically ill-formed.


> Gödels G asserts that a specific polynomial equation has a solution.
>
> Since every polynomial equation either has a solution or doesn't have
> one, G *must* either be true or false which means it *must* be a truth
> bearer.
>
> André

[André G. Isaak]

And what does any of the above have to do with what I state below?
That's your faulty attempt at expressing The Liar in Prolog, which has
nothing to do with Gödel's G. G has *a relationship* to The Liar, but G
is *very* different from The Liar in crucial ways.

>
>> Gödels G asserts that a specific polynomial equation has a solution.

This is the part you don't seem to get. Gödel's G does *not* assert its
own unprovability. It asserts that a specific polynomial equation has a
solution.

That's very different from The Liar which asserts its own falsity.

Gödel's theorem constructs a G such that it can be demonstrated that the
polynomial which G asserts has a solution can only have a solution in
cases where it cannot be proven that that polynomial has a solution.

There is no self-reference involved. G asserts nothing about itself.

More importantly, the polynomial in question *must* either have a
solution or not. This means G *must* either be true or false, meaning G
*must* be a truth-bearer.

[olcott]

Therfore the liar paradox can likewise be used for a similar
undecidability proof, nitwit.

I would not call you a nitwit except that you so persistently make sure
to ignore my key points, thus probably making you a jackass rather than
a nitwit.

[Richard Damon]

So something based on another thing is that other thing?

Does that mean your automobile is just a pile of gasoline?

That IS the argument you are making boiled down to simple terms.

[olcott]

On 5/1/2022 3:37 PM, André G. Isaak wrote:
> On 2022-05-01 14:03, olcott wrote:
>> On 5/1/2022 2:54 PM, André G. Isaak wrote:

>>> And again, you snipped all of the
>>
>> God damned attempt to get away with the dishonest dodge of the
>> strawman error.
>>

>> 14 Every epistemological antinomy can likewise be used for a similar
>> undecidability proof
>>

>> Do you not know what the word "every" means?
>
> Do you understand the difference between 'close relationship' and 'the
> same'?

You freaking dishonest bastard

14 Every epistemological antinomy can likewise be used for a similar
undecidability proof

The Liar Paradox is an epistemological antinomy

[André G. Isaak]

The only one being dishonest here is you as you keep snipping the
substance of my post.

Gödel claims there is a *close relationship* between The Liar and G. He
most certainly does *not* claim that they are the same. (That one can
construct similar proofs which bear a similar close relationship to
other antinomies is hardly relevant since it is The Liar which is under
discussion).

There are two crucial differences between G and The Liar:

(a) G does *not* assert its own unprovability whereas The Liar *does*
assert its own falsity.

(b) G is most definitely a truth-bearer even if The Liar is not.

Your claim the Gödel's theorem is a 'category error' is predicated on
the fact that you don't grasp (b) above. I'm not going to retype my
explanation for this as I have already given it in a previous post.
You're more than welcome to go back and read that post. Unless you
actually have some comment on that explanation, there's no point
repeating yourself.

[Richard Damon]

Right, But G isn't, because it ISN'T the Liar's Paradox, but has a
structure based on the Liar's Paradox but transformed.

Your failure to understand this difference says you are unqualified to
talk about the meaning of words, or basic logical principles.

[olcott]

and the Liar Paradox is and is an epistemological antinomy you lying
bastard.

[olcott]

and the Liar Paradox is and is an epistemological antinomy you lying
bastard.

> (That one can
> construct similar proofs which bear a similar close relationship to
> other antinomies is hardly relevant since it is The Liar which is under
> discussion).
>
> There are two crucial differences between G and The Liar:
>
> (a) G does *not* assert its own unprovability whereas The Liar *does*
> assert its own falsity.
>
> (b) G is most definitely a truth-bearer even if The Liar is not.
>
> Your claim the Gödel's theorem is a 'category error' is predicated on
> the fact that you don't grasp (b) above. I'm not going to retype my
> explanation for this as I have already given it in a previous post.
> You're more than welcome to go back and read that post. Unless you
> actually have some comment on that explanation, there's no point
> repeating yourself.
>
> André
>


--

[Richard Damon]

So, there is a difference between being used for and being just like.

[André G. Isaak]

Since you're clearly not planning on addressing any of my points, I
think we're done.

I'll leave you with a small multiple choice quiz: Are you

(a) someone who was dropped on their head as a child.
(b) suffering from foetal alcohol syndrome.
(c) thick as a brick.
(d) all of the above.

[olcott]

sufficiently equivalent

[olcott]

I just proved that you are a lying bastard. I can very easily forgive
and forget, what I will not do is tolerate mistreatment

14 Every epistemological antinomy can likewise be used for a similar
undecidability proof

The Liar Paradox is an epistemological antinomy

Translating this to a syllogism

All X are a Y
The LP is and X
Therefore the LP is a Y.

That you disagree with this makes you a lying bastard.

[André G. Isaak]

For christ's sake. You can't even see the irrelevance of the above.

Let's consider what the X and Y are in the above:

X would be 'Is an Antinomy'

Since Gödel was *already* talking about The Liar, Y is "Can be used to
form an undecidability proof in a similar manner as Gödel has done with
The Liar"

So you've just proved that The Liar can be used to form a similar proof
as the one Gödel forms using The Liar.

Do you feel proud of yourself?

What you keep ignoring, which were the points my posts were actually
about was exactly *what* sort of relationship holds between The Liar and
Gödel's G. It is *not* one of identity.

There is a close relationship between the Book of Genesis and the Epic
of Gilgamesh.

Gilgamesh figures prominently in the Epic of Gilgamesh.

Therefore Gilgamesh figures prominently in the Book of Genesis.

According to the Epic of Gilgamesh, a savage can become civilized by
having sex with a prostitute.

Therefore the Book of Genesis advocates forcing the uncivilized to have
sex with prostitutes.

Do you see a problem with the above arguments? Saying there is a 'close
relationship' between two things doesn't mean you can conclude
*anything* about one based on the other. You need to consider exactly
*what* the relationship actually is. What are the similarities and what
are the differences? You insist on treating the two as if they were the
same thing. They aren't, anymore than the Book of Genesis and the Epic
of Gilgamesh are the same thing.

[olcott]

I just proved that you are a lying bastard. I can very easily forgive
and forget, what I will not do is tolerate mistreatment

14 Every epistemological antinomy can likewise be used for a similar
undecidability proof

The Liar Paradox is an epistemological antinomy

Translating this to a syllogism

All X are a Y
The LP is and X
Therefore the LP is a Y.

That you disagree with this makes you a lying bastard.

[Richard Damon]

You can PROVE it?

Note, that means you need to start with the ACTUAL G that Godel used,
not some "simplified" version. So you better know what all that means.

[Richard Damon]

As Andre pointed out, when you look at the statement to see what the
terms are, you just agreed with him and proved that YOU are the Liar.

[André G. Isaak]

On 2022-05-01 17:18, Richard Damon wrote:

> On 5/1/22 6:39 PM, olcott wrote:

>> sufficiently equivalent
>>
>
> You can PROVE it?

Presumably he will point to the (nonexistent) footnote where Gödel
claims that The Liar and G are "sufficiently equivalent" rather than the
(actual) footnote where Gödel rather explicitly denies this.

[olcott]

Not quite.
X = is an epistemological antinomy

> Since Gödel was *already* talking about The Liar, Y is "Can be used to
> form an undecidability proof in a similar manner as Gödel has done with
> The Liar"
>
> So you've just proved that The Liar can be used to form a similar proof
> as the one Gödel forms using The Liar.
>
> Do you feel proud of yourself?
>
> What you keep ignoring, which were the points my posts were actually
> about was exactly *what* sort of relationship holds between The Liar and
> Gödel's G. It is *not* one of identity.
>

Of course not nitwit, you know that I mean equivalence.

What kind of stupid fool would believe that I mean that G and LP are one
and the same thing? I know, I know, a jackass that wants to play head
games.

> There is a close relationship between the Book of Genesis and the Epic
> of Gilgamesh.

He says two different things about the Liar Paradox Jackass.
(1) About the Liar Paradox in particular.
(2) About the entire category that the Liar Paradox belongs:
epistemological antinomies.

If every epistemological antinomy can likewise be used for a similar
undecidability proof then the liar paradox can be used for a similar
undecidability proof.

X = set of epistemological antinomies.
Y = can be used for a similar undecidability proof.

All X are Y
The LP is an X

Therefore the LP is a Y.

You have known this all along you merely get sadistic pleasure by
gaslighting me. That may be the only reason why anyone here (besides
Malcolm) talks to me.

https://www.nbcnews.com/better/health/what-gaslighting-how-do-you-know-if-it-s-happening-ncna890866

>
> Gilgamesh figures prominently in the Epic of Gilgamesh.
>
> Therefore Gilgamesh figures prominently in the Book of Genesis.
>
> According to the Epic of Gilgamesh, a savage can become civilized by
> having sex with a prostitute.
>
> Therefore the Book of Genesis advocates forcing the uncivilized to have
> sex with prostitutes.
>
> Do you see a problem with the above arguments? Saying there is a 'close
> relationship' between two things doesn't mean you can conclude
> *anything* about one based on the other. You need to consider exactly
> *what* the relationship actually is. What are the similarities and what
> are the differences? You insist on treating the two as if they were the
> same thing. They aren't, anymore than the Book of Genesis and the Epic
> of Gilgamesh are the same thing.
>
> André
>


--

[André G. Isaak]

Equivalence with respect to *what*?

If two things are equivalent but not identical, it means they are
equivalent with respect to some things but not equivalent with respect
to others.

The entire point of my posts has been to clarify some senses in which
the two are *not* equivalent. But instead of addressing that you keep
trying to prove that The Liar is in the same class as The Liar.

> What kind of stupid fool would believe that I mean that G and LP are one
> and the same thing? I know, I know, a jackass that wants to play head
> games.
>
>> There is a close relationship between the Book of Genesis and the Epic
>> of Gilgamesh.
>
> He says two different things about the Liar Paradox Jackass.
> (1) About the Liar Paradox in particular.
> (2) About the entire category that the Liar Paradox belongs:
> epistemological antinomies.

Yes, and if the LP is *not* equivalent to G with respect to X, then none
of the analogous sentences based on other antinomies would be equivalent
with respect to X either.

> If every epistemological antinomy can likewise be used for a similar
> undecidability proof then the liar paradox can be used for a similar
> undecidability proof.
>
> X = set of epistemological antinomies.
> Y = can be used for a similar undecidability proof.
>
> All X are Y
> The LP is an X
> Therefore the LP is a Y.

Yes. The Liar and the Liar can be used for similar undecidability
proofs. I have no idea what it is you hope to achieve by arguing for a
truism.

[olcott]

See that I backed you into a corner to force you to quit lying.

[olcott]

I backed him into a corner and forced him to stop lying:

On 5/1/2022 6:44 PM, André G. Isaak wrote:
> Yes. The Liar and the Liar can be used for similar undecidability
> proofs. I have no idea what it is you hope to achieve by arguing for a
> truism.

Anyone that abuses me gets a metaphorical uppercut to the jaw.

[olcott]

I backed André into a corner and forced him to quit lying

On 5/1/2022 6:44 PM, André G. Isaak wrote:
> Yes. The Liar and the Liar can be used for similar undecidability
> proofs. I have no idea what it is you hope to achieve by arguing for a
> truism.

> Note, that means you need to start with the ACTUAL G that Godel used,
> not some "simplified" version. So you better know what all that means.

[Richard Damon]

So, No. Note a trimming to change meaning, the original was:

>>>>>
>>>>
>>>> 14 Every epistemological antinomy can likewise be used for a similar undecidability proof
>>>>
>>>> and the Liar Paradox is and is an epistemological antinomy you lying bastard.
>>>>
>>>
>>> So, there is a difference between being used for and being just like.
>>
>> sufficiently equivalent
>>
>
> You can PROVE it?

So, clearly the requested proof was that about USING the epistemolgocal
antinomy and it being just like one so not a Truth Bearer. Note, the
comment that you claimed you backed him into isn't about that, so you
are just proving yourself to be a deciver.

> On 5/1/2022 6:44 PM, André G. Isaak wrote:
> > Yes. The Liar and the Liar can be used for similar undecidability
> > proofs. I have no idea what it is you hope to achieve by arguing for a
> > truism.
>

Nice out of context quoting, showing again you are the deciver.

Fuller Quote:

>
>> All X are Y
>> The LP is an X

>> Therefore the LP is a Y.
>

> Yes. The Liar and the Liar can be used for similar undecidability proofs. I have no idea what it is you hope to achieve by arguing for a truism.
>

So he is agreeing that LP is your attempt to code the Liar's Paradox,
and that the Liar's paradox is one of the templates that you can use to
derive an undecidability proof from.

This doesn't say that such a use means anything.

You are just showing that you are a lying cheat that twists words to try
to show that your deceptions have a grain of truth in them.

They don't, but you are just proving that you don't understand what
Truth even is.

I pity you, and pray that your mind will snap out of fog that you seem
to have been in for decades, and you will see what Truth actually is.

[olcott]

If you look at the full context of many messages you will see that he
kept continuing to deny that the Liar Paradox can be used for similar
undecidability proofs at least a half dozen times. Only when I made
denying this look utterly ridiculously foolish did he finally quit lying
about it.

[Richard Damon]

No, he says that the use of the Liar Paradox in the form that Godel does
doesn't make the Godel Sentence a non-truth holder.

The fact that you have mis-interpreted him that many times, and even
snipped out his explanations shows you ignrance and lack of scruples.
You show a marked propensity to (apparently) intentionally twist the
words of others to match the script you are trying to write.

You are just solidifying your place in history as someone who does NOT
understand the basics of the field they are making grand claims in, who
does NOT understand the basics of logic, and who is just a pathological
liar that doesn't understand the first thing about truth.

In the past, I thought that maybe some of your philosophies about
Knowledge might have had some interesting concepts in them, but you have
convinced me that you are so filled with lies that there can't be any
understanding about the nature of Truth in anything you can say.

You have basically just proved that you have wasted the last 2 decades
of your list, distroying any reputation you might have built up with
past works. You will forever be know as the Liar about Paradoxes.

[olcott]

If you look at the actual facts you will see that he continued to deny
that kept continuing to deny that the Liar Paradox can be used for

similar undecidability proofs at least a half dozen times.

If you make sure to knowingly contradict the verified facts then
Revelations 21:8 may eventually apply to you.

> The fact that you have mis-interpreted him that many times, and even
> snipped out his explanations shows you ignrance and lack of scruples.
> You show a marked propensity to (apparently) intentionally twist the
> words of others to match the script you are trying to write.
>
> You are just solidifying your place in history as someone who does NOT
> understand the basics of the field they are making grand claims in, who
> does NOT understand the basics of logic, and who is just a pathological
> liar that doesn't understand the first thing about truth.
>
> In the past, I thought that maybe some of your philosophies about
> Knowledge might have had some interesting concepts in them, but you have
> convinced me that you are so filled with lies that there can't be any
> understanding about the nature of Truth in anything you can say.
>
> You have basically just proved that you have wasted the last 2 decades
> of your list, distroying any reputation you might have built up with
> past works. You will forever be know as the Liar about Paradoxes.

[André G. Isaak]

On 2022-05-01 20:18, olcott wrote:
> On 5/1/2022 9:14 PM, Richard Damon wrote:
>>
>> On 5/1/22 9:53 PM, olcott wrote:

>>> If you look at the full context of many messages you will see that he
>>> kept continuing to deny that the Liar Paradox can be used for similar
>>> undecidability proofs at least a half dozen times. Only when I made
>>> denying this look utterly ridiculously foolish did he finally quit
>>> lying about it.
>>>
>>
>> No, he says that the use of the Liar Paradox in the form that Godel
>> does doesn't make the Godel Sentence a non-truth holder.
>>
>
> If you look at the actual facts you will see that he continued to deny
> that kept continuing to deny that the Liar Paradox can be used for
> similar undecidability proofs at least a half dozen times.

I didn't so much deny that as I did claim it was vacuous and irrelevant.

Gödel draws a parallel between his proof and The Liar.

He also notes that other antinomies could be used to construct similar
proofs.

That would seem to mean that OTHER ANTINOMIES could be used to construct
similar proofs to the one he based on The Liar.

To say that The Liar can be used to construct similar proofs is just
plain silly since that's the one he was talking about to begin with.

More importantly, though, it is absolutely irrelevant to any of the
points I was making which didn't deny some relationship between G and
The Liar but concerned the exact *nature* of the relationship between G
and The Liar, points which would hold for proofs based on other
antinomies as well.

And points which you still have not addressed.

[Richard Damon]

You mean like when he said (and you snipped):

>
> The only one being dishonest here is you as you keep snipping the substance of my post.
>
> Gödel claims there is a *close relationship* between The Liar and G. He most certainly does *not* claim that they are the same. (That one can construct similar proofs which bear a similar close relationship to other antinomies is hardly relevant since it is The Liar which is under discussion).
>
> There are two crucial differences between G and The Liar:
>
> (a) G does *not* assert its own unprovability whereas The Liar *does* assert its own falsity.
>
> (b) G is most definitely a truth-bearer even if The Liar is not.
>
> Your claim the Gödel's theorem is a 'category error' is predicated on the fact that you don't grasp (b) above. I'm not going to retype my explanation for this as I have already given it in a previous post. You're more than welcome to go back and read that post. Unless you actually have some comment on that explanation, there's no point repeating yourself.
>

Maybe you should check your OWN facts.

He is CLEARLY not saying that the Liar Paradox can't be used for this
sort of proof, because he talks about its form being used.

What he is denying, that seems beyound your ability to understand, so
much so tha that you remove it from your messages, that this fact
doesn't make the G itself a "Liar Paradox" that isn't a Truth Bearing
like you claim.

Maybe YOU should be looking at the actual facts of who said what, and
see who is guilty of lying.

I think you are getting very close to that Lake of Fire.

[olcott]

He is focusing on the dishonest dodge of the strawman error by making
sure to ignore that in another quote Gödel said that Gödel's G is
sufficiently equivalent to the Liar Paradox on the basis that the Liar
Paradox is an epistemological antinomy, whereas the quote he keeps
switching back to is less clear on this point.

Since I focused on correcting his mistake several times it finally got
down to the point where it was clear that he was a lying bastard.

I am utterly immune to gas lighting.

> He is CLEARLY not saying that the Liar Paradox can't be used for this
> sort of proof, because he talks about its form being used.
>

He continued to refer to the other quote of Gödel that is much more
vague on the equivalence between Gödel's G as his basis that equivalence
cannot be be determined even when I kept focusing him back on the quote
that does assert sufficient equivalence exists. I did this six times.

At this point my assessment that he was a lying bastard was sufficiently
validated.

Are you a lying bastard too, or will you acknowledge that my assessment
is correct?

> What he is denying, that seems beyound your ability to understand, so
> much so tha that you remove it from your messages, that this fact
> doesn't make the G itself a "Liar Paradox" that isn't a Truth Bearing
> like you claim.
>
> Maybe YOU should be looking at the actual facts of who said what, and
> see who is guilty of lying.
>
> I think you are getting very close to that Lake of Fire.
>
>>
>>> The fact that you have mis-interpreted him that many times, and even
>>> snipped out his explanations shows you ignrance and lack of scruples.
>>> You show a marked propensity to (apparently) intentionally twist the
>>> words of others to match the script you are trying to write.
>>>
>>> You are just solidifying your place in history as someone who does
>>> NOT understand the basics of the field they are making grand claims
>>> in, who does NOT understand the basics of logic, and who is just a
>>> pathological liar that doesn't understand the first thing about truth.
>>>
>>> In the past, I thought that maybe some of your philosophies about
>>> Knowledge might have had some interesting concepts in them, but you
>>> have convinced me that you are so filled with lies that there can't
>>> be any understanding about the nature of Truth in anything you can say.
>>>
>>> You have basically just proved that you have wasted the last 2
>>> decades of your list, distroying any reputation you might have built
>>> up with past works. You will forever be know as the Liar about
>>> Paradoxes.
>>
>>
>

[André G. Isaak]

On 2022-05-01 21:04, olcott wrote:

> He is focusing on the dishonest dodge of the strawman error by making
> sure to ignore that in another quote Gödel said that Gödel's G is
> sufficiently equivalent to the Liar Paradox on the basis that the Liar
> Paradox is an epistemological antinomy, whereas the quote he keeps
> switching back to is less clear on this point.

There is no quote where Gödel claims G is "sufficiently equivalent" to
the Liars Paradox. (And "sufficiently equivalent" for what, exactly? Is
a five dollar bill "sufficiently equivalent" to 20 quarters? It's a
meaningless question without specifying what type of equivalence you
have in mind -- equivalent value, sure. Equivalent usefulness in a
vending maching, not necessarily)

> Since I focused on correcting his mistake several times it finally got
> down to the point where it was clear that he was a lying bastard.

Since you seem to be claiming that I reject some nonexistent quote, I
can't imagine what mistake I might have made.

> I am utterly immune to gas lighting.
>
>> He is CLEARLY not saying that the Liar Paradox can't be used for this
>> sort of proof, because he talks about its form being used.
>>
>
> He continued to refer to the other quote of Gödel that is much more
> vague on the equivalence between Gödel's G as his basis that equivalence
> cannot be be determined even when I kept focusing him back on the quote
> that does assert sufficient equivalence exists. I did this six times.

What is this quote you are referring to where he asserts "sufficient
equivalence"? Unless I missed something, the quote you kept harping on
was "Every epistemological antinomy can likewise be used for a similar
undecidability proof". That makes no mention whatsoever of "equivalence"
(sufficient or otherwise) between The Liar and G.

[Richard Damon]

I will acknowledge that you have proven yourself to be the lying bastard.

YOU have REPEADTEDLY trimmed out important parts of the conversation
either to INTENTIONALLY be deceptive, or because you are so incompetent
at this material that you don't know what is important.

You see words which are not there and don't see the words that are there.

Godel talks of a way to use the form of any epistemological antinomy to
build a similar argument to his G.

I think one thing that maybe you don't understand about G and the Liar
Paradox is that this G IS built on the Liar Paradox so I think part of
your issue is that you are trying to argue about the possibility to make
a different G but from the Liar's Paradox, when this one was. The fact
you don't see that G, as is, as being based on the Liar's Paradox, means
you don't understand the way it is actually formed on the Liar's paradox.

[Aleksy Grabowski]

Wow, I went offline for a weekend, because we had such a nice weather,
and this thread exploded to enormous size 😲. I didn't read the whole
thread it's just too big.

On 5/1/22 13:00, olcott wrote:
> On 5/1/2022 4:26 AM, Mikko wrote:
>> On 2022-04-30 21:08:05 +0000, olcott said:
>>
>>> negation, not, \+
>>> The concept of logical negation in Prolog is problematical, in the
>>> sense that the only method that Prolog can use to tell if a
>>> proposition is false is to try to prove it (from the facts and rules
>>> that it has been told about), and then if this attempt fails, it
>>> concludes that the proposition is false. This is referred to as
>>> negation as failure.
>>
>> Note that the negation discussed above is not present in LP =
>> not(true(LP)).
>>
>> Mikko
>>
>
> Is says that it is. It says that "not" is synonymous with \+.

I don't want to undermine your knowledge in formal logic, but still
allow me to re-iterate my point, because it looks like it didn't come
through.

1. Prolog is *not* an automated theorem prover; it is a programming
language. Nevertheless you can /implement/ one in Prolog.
2. Prolog's syntax is somewhat original and requires some
understanding.

Let me elaborate on the 2nd point. Prolog is a homoiconic language that
means that same syntactical constructs (terms) can express data, or be
executable.

Consider this knowledge base¹:

foo :- not(true).

The following query will fail:

?- foo.
false.

When we asked the program to refute `foo/0` it *executed* predicates
`not/1` and `true/0`.

But, given this knowledge base:

bar(X) :- X = not(true).

The following query does succeed:

?- bar(X).
X = not(true).

Why? — Here, both `not/1` and `true/0` were *not* executed, they were
used as a mere symbols, data without *any* meaning whatsoever. Also
please note that this has nothing to do with cyclic terms, they are
completely separate things, and the problem with your Prolog code
doesn't lie in cyclic term handling, but in basic misconception when
terms are executed and when they aren't. In your example:

> LP := ~True(LP) is translated to Prolog:

>
> ?- LP = not(true(LP)).
> LP = not(true(LP)).
>
> ?- unify_with_occurs_check(LP, not(true(LP))).
> false

None (!) of the predicates where executed in both unifications (with and
without occurs check).

Basically what I was trying to say is that `LP = not(true(LP))` is
incorrect encoding of the stated logical formula. What you have written
just tells to Prolog to unify variable `LP` with the term
`not(true(LP))`, it is similar to this query (`not` is used only as an
atom it isn't executed):

?- X = [not|X].
X = [not|X].

?- unify_with_occurs_check(X, [not|X]).
false.

I've skimmed through your paper and you encode logical formula G = ¬(F ⊢
G) as:

G = not(provable(F, G)).

Which is not correct for all the reasons I've laid down previously, at
least it is not correct with the default semantics of `=` operator.

I hope this will clear some thing out.

[¹] As a side note, according to the SWI-Prolog documentation `not/1`
predicate is deprecated and should be replaced with `'\+'/1`.
https://www.swi-prolog.org/pldoc/doc_for?object=not/1

--
Alex Grabowski

[olcott]

Here is what I understand of the relationship between logic and Prolog.
Prolog corrects all of the errors of classical and symbolic logic by
forming the underlying framework for the correct notion of truth and
provability. In all of the places where logic diverges from the Prolog
model logic fails to be correct.

Correct logic derives conclusions on the basis of applying truth
preserving operations to expressions of language known to be true. This
simple model refutes the Tarski undefinability theorem.

Tarski Undefinability Proof.
https://liarparadox.org/Tarski_275_276.pdf

If a set of rules (truth preserving operations) can be applied to a set
of facts (expressions of language known to be true) then the result is
the truth of the Prolog expression. This is the way that Truth really
works and both classical and Symbolic logic go astray of this.
https://en.wikipedia.org/wiki/Prolog#Rules_and_facts

It is also Good that Prolog as negation as failure because this detects
logic errors that are hidden from classical and symbolic logic. Logic
always assume that every expression of language that is not true must be
false. This makes semantic errors invisible to classical and symbolic
logic visible to Prolong.

This sentence is neither provable nor refutable in Prolog:
This sentence is not true. This is one of my best attempts at
formalizing that: LP ↔ ~True(LP)

The whole purpose of this thread is to find out exactly how to encode:
"This sentence is not true" in Prolog when we assume that True is
exactly the same thing as Provable in Prolog.

[olcott]

I trim so that we can stay focused on the point at hand and not diverge
into many unrelated points. The main way that all of the rebuttals of my
work are formed is changing the subject to another different subject and
the rebutting this different subject. I cut all that bullshit out.

> You see words which are not there and don't see the words that are there.
>
> Godel talks of a way to use the form of any epistemological antinomy to
> build a similar argument to his G.
>
> I think one thing that maybe you don't understand about G and the Liar
> Paradox is that this G IS built on the Liar Paradox

That is well put. G takes the exact same idea as the liar paradox and
then implements this liar paradox with 100,000-fold of additional purely
extraneous complexity.

> so I think part of
> your issue is that you are trying to argue about the possibility to make
> a different G but from the Liar's Paradox, when this one was. The fact
> you don't see that G, as is, as being based on the Liar's Paradox, means
> you don't understand the way it is actually formed on the Liar's paradox.
>

I have seen this all along since my research began in 2004.

[Aleksy Grabowski]

> The whole purpose of this thread is to find out exactly how to encode:
> "This sentence is not true" in Prolog when we assume that True is
> exactly the same thing as Provable in Prolog.

"This sentence is not provable" can be naïvely encoded:

g :- \+ g.

Then you can ask Prolog if this sentence is true:

?- g.

Prolog will give you the only correct answer — no answer 🙃.

> Here is what I understand of the relationship between logic and Prolog.
> Prolog corrects all of the errors of classical and symbolic logic by
> forming the underlying framework for the correct notion of truth and
> provability. In all of the places where logic diverges from the Prolog
> model logic fails to be correc

Prolog by itself is a very bad theorem prover and it is very limited
framework for formal logic, because it implements only Horn clauses.
However it is a very good programming language and you can implement any
theorem prover in it, like you can implement any theorem prover in C++
or Java.

--
Alex Grabowski

[olcott]

On 5/2/2022 8:35 AM, Aleksy Grabowski wrote:
>> The whole purpose of this thread is to find out exactly how to encode:
>> "This sentence is not true" in Prolog when we assume that True is
>> exactly the same thing as Provable in Prolog.
>
> "This sentence is not provable" can be naïvely encoded:
>
> g :- \+ g.
>
> Then you can ask Prolog if this sentence is true:
>
> ?- g.
>
> Prolog will give you the only correct answer — no answer 🙃.

That is great, now what happens when we encode:
"This sentence is provable" in Prolog?

What happens when we test both of these with
unify_with_occurs_check ?

>
>> Here is what I understand of the relationship between logic and Prolog.
>> Prolog corrects all of the errors of classical and symbolic logic by
>> forming the underlying framework for the correct notion of truth and
>> provability. In all of the places where logic diverges from the Prolog
>> model logic fails to be correc

> Prolog by itself is a very bad theorem prover and it is very limited
> framework for formal logic, because it implements only Horn clauses.

None-the-less by evaluating expressions on the basis of facts
(expression known to be true) and rules (truth preserving operations)
and having negation as failure then all of the errors of logic are
corrected and Tarski's undefinability theorem fails.
https://liarparadox.org/Tarski_275_276.pdf

Because there are ways to do Higher Order Logic in Prolog I don't see
how any of its limitations can make any actual difference.

> However it is a very good programming language and you can implement any
> theorem prover in it, like you can implement any theorem prover in C++
> or Java.
>


--

[Aleksy Grabowski]

On 5/2/22 15:55, olcott wrote:
> On 5/2/2022 8:35 AM, Aleksy Grabowski wrote:
>>> The whole purpose of this thread is to find out exactly how to
>>> encode: "This sentence is not true" in Prolog when we assume that
>>> True is exactly the same thing as Provable in Prolog.
>>
>> "This sentence is not provable" can be naïvely encoded:
>>
>> g :- \+ g.
>>
>> Then you can ask Prolog if this sentence is true:
>>
>> ?- g.
>>
>> Prolog will give you the only correct answer — no answer 🙃.
>
> That is great, now what happens when we encode:
> "This sentence is provable" in Prolog?
>
> What happens when we test both of these with
> unify_with_occurs_check ?

"This sentence is provable"

g.

Both of sentences are true at the same time:

both :- g, \+ g.

Then query:

?- both.

doesn't terminate, which is correct behavior for such paradoxical
statement. Did you expect some answer here? What it should be then? I'm
not very good at hardcore formal logic I'm just a programmer - not
mathematician, but I think there shouldn't be an answer.

Also I don't get how unification is even relevant here.

> None-the-less by evaluating expressions on the basis of facts
> (expression known to be true) and rules (truth preserving operations) and
> having negation as failure then all of the errors of logic are corrected
> and Tarski's undefinability theorem fails.
> https://liarparadox.org/Tarski_275_276.pdf

I'm afraid I can't comment on this

> Because there are ways to do Higher Order Logic in Prolog I don't see
> how any of its limitations can make any actual difference.

Agree, many limitation can be fixed, like unfair enumeration for some
predicates, bad termination qualities for some correct programs, or as
you said higher order logic (I don't know why you ever need it in a real
program, but that's another topic).

[olcott]

That is great. That shows when Gödel's 1931 Incompleteness Theorem is
transformed into its barest possible essence Prolog proves it to be
ill-formed.

What is happening internally that causes the expression to never terminate?

> Also I don't get how unification is even relevant here.
>
>> None-the-less by evaluating expressions on the basis of facts
>> (expression known to be true) and rules (truth preserving operations) and
>> having negation as failure then all of the errors of logic are corrected
>> and Tarski's undefinability theorem fails.
>> https://liarparadox.org/Tarski_275_276.pdf
>
> I'm afraid I can't comment on this
>
>> Because there are ways to do Higher Order Logic in Prolog I don't see
>> how any of its limitations can make any actual difference.
>
> Agree, many limitation can be fixed, like unfair enumeration for some
> predicates, bad termination qualities for some correct programs, or as
> you said higher order logic (I don't know why you ever need it in a real
> program, but that's another topic).
>

[Aleksy Grabowski]

Some definitions. The part before `:-` is called head, and after is
called body. Conceptually the model of execution of Prolog programs
looks more-or-less as follows:

0. If predicate doesn't have body it is always true.
1. Assume that head is false.
2. Check if we can find a counter-example by proving body.
3. If counter-example was found then previous assumption is incorrect
and in fact head should be true. If counter-example wasn't found then
our assumption was correct and head is false.
4. Recursively apply same rules for each clause in the body.

In our example Prolog will just execute `g` ad infinitum.

--
Alex Grabowski

[olcott]

That is beautiful and affirms the key element of all of my research on
incompleteness.

This is the mathematical definition of incompleteness:
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).

It says expression φ of formal system T can neither be proved or
refuted. A formal system is comparable to a Prolog database. I have
always known that the issue is that expression φ is semantically
ill-formed, now I have Prolog agreeing with me.

>>> both :- g, \+ g.
>>>
>>> Then query:
>>>
>>> ?- both.
>>> doesn't terminate, which is correct behavior for such paradoxical
>>> statement. Did you expect some answer here? What it should be then?

Is there any Prolog that can detect that the above will not terminate
prior to executing it?

Does it specify the same sort of infinite structure that the following
Clocksin & Mellish text describes?

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)

Clarification to: "foo(foo(foo(Y))), and so on":
foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))

[Aleksy Grabowski]

On 5/2/22 18:04, olcott wrote:
> Is there any Prolog that can detect that the above will not terminate
> prior to executing it?

As I have said previously, my example is naïve. Maybe if you will think
hard enough you can make it detect such conditions, probably by writing
meta-interpreter of some sort, and terminate. Personally, I don't think
that using Prolog can be accepted as a "rigorous proof" of anything.

> Does it specify the same sort of infinite structure that the following
> Clocksin & Mellish text describes?
>
> 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)
>
> Clarification to: "foo(foo(foo(Y))), and so on":
> foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))
>

There can't be an infinite structure physically in computer memory, and
I think that programmers who implemented Prolog are smart enough not to
require large memory for such cases.

Maybe he refers for some abstract infinite structure, that need not to
exist on the hardware level.

--
Alex Grabowski

[olcott]

On 5/2/2022 11:38 AM, Aleksy Grabowski wrote:
> On 5/2/22 18:04, olcott wrote:
>> Is there any Prolog that can detect that the above will not terminate
>> prior to executing it?
>
> As I have said previously, my example is naïve. Maybe if you will think
> hard enough you can make it detect such conditions, probably by writing
> meta-interpreter of some sort, and terminate. Personally, I don't think
> that using Prolog can be accepted as a "rigorous proof" of anything.
>

I need to know more details about what is occurring internally (within
Prolog) when the expressions are executed.

>> Does it specify the same sort of infinite structure that the following
>> Clocksin & Mellish text describes?
>>
>> 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)
>>
>> Clarification to: "foo(foo(foo(Y))), and so on":
>> foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))
>>
>
> There can't be an infinite structure physically in computer memory, and
> I think that programmers who implemented Prolog are smart enough not to
> require large memory for such cases.
>
> Maybe he refers for some abstract infinite structure, that need not to
> exist on the hardware level.
>

The above quote from Clocksin & Mellish refers to getting
unify_with_occurs_check to check in advance that unification would
require infinite memory.

[Jeff Barnett]

On 5/2/2022 9:24 AM, olcott wrote: NOTHING OF VALUE


I will attempt to summarize the level of the idiot's understanding of
Prolog: The level is the same as of his understanding of math, logic, C,
C++, software engineering, programming, programming methodology, Turing
Machines, and other specific topics in these general categories. He is
capable of moving his eyes through a few paragraphs but not reading
anything. This is a common learning disability. He can cut and paste
from what little is eyes scan but, in general, he can neither comprehend
the little he's seen nor can he amalgamate concepts from the bits and
pieces he has visited.

His approach to gaining and demonstrating understanding is best
represented by a comic's view of monkeys exploring objects new to them:
biting things, hitting other objects with the new one, stirring feces
and seeing if it will stick and can be thrown etc. The problem with this
metaphor is that monkeys are intelligent and our idiot is not. When the
monkey is done with initial exploration, it has an idea whether the new
object can serve some useful purpose; in any event, the monkey had fun.
The idiot, on the other hand, never discoveries the usefulness of the
potential new knowledge because he doesn't have the attention span or
curiosity to do so. That's why he is an idiot and not as smart or as
wise as the monkey though he too has fun.
--
Jeff Barnett

[Mr Flibble]

The ad hominem attack is a logical fallacy: so it is in fact YOU who is
throwing excrement at the walls, not Olcott. Attack the argument not the
person, dear.

https://en.wikipedia.org/wiki/Ad_hominem

/Flibble

[olcott]

Yes Jeff is mostly a Jackass. Once in a very great while he says
something interesting. This is very rare yet thankfully more often than
never.

[olcott]

My key more important understanding of the fundamental architecture of
Prolog is that it is anchored in sound deductive inference thus
correctly all of the errors that have crept into logic since Aristotle's
syllogism.

Start with known truths (Prolog facts) and only apply truth preserving
operations (Prolog rules) to derive conclusions that can be relied on as
true.

Also helpful is Prolog's negation as failure that does not make the huge
mistake of assuming that every expression that is not true must be false.

[Richard Damon]

IF you are defining that your logic system is limited to what Prolog can
"Prove", that is fine. Just realize that you have just defined that your
logic system can't handle a lot of the real problems in the world, and
in particular, it is very limited in the mathematics it can handle.

I am pretty sure that Prolog is NOT up to handling the logic needed to
handle the mathematics needed to express Godel's G, or the Halting Problem.

Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you
have only proven that your limited logic system can't reach them in
expressibility.

[Richard Damon]

TRANSLATION: I trim out what will prove me wrong because I don't have
time to think up other excuses.

You are just admitting failure, if not to yourself, to anyone with a
real brain.

>
>> You see words which are not there and don't see the words that are there.
>>
>> Godel talks of a way to use the form of any epistemological antinomy
>> to build a similar argument to his G.
>>
>> I think one thing that maybe you don't understand about G and the Liar
>> Paradox is that this G IS built on the Liar Paradox
>
> That is well put. G takes the exact same idea as the liar paradox and
> then implements this liar paradox with 100,000-fold of additional purely
> extraneous complexity.

Nope, NOT extraneous, just apparently beyound your leve of comptehension.

>
>> so I think part of your issue is that you are trying to argue about
>> the possibility to make a different G but from the Liar's Paradox,
>> when this one was. The fact you don't see that G, as is, as being
>> based on the Liar's Paradox, means you don't understand the way it is
>> actually formed on the Liar's paradox.
>>
>
> I have seen this all along since my research began in 2004.
>

Nope, it is clear you don't understand it from your statements.

I have yet to see any statement from you showing any level of
understnading about the actual behavior of Turing Machines, or about the
actual structure of the Godel incompleteness proof. All I have seen are
ignorant non-sensical cut-and-paste quoting of material with no actually
understanding.

You gave up before showing even a typical first Turing Machine from a
basic course on Computation Theory, apparently because you just don't
understand the material. IT can't be the time involved, as for someone
with an actual understanding of Turing Machines, it is at most a 30
minute exercise, maybe even just a few minutes (depending on how fast
you can actually type).

[Aleksy Grabowski]

> IF you are defining that your logic system is limited to what Prolog can
> "Prove", that is fine. Just realize that you have just defined that your
> logic system can't handle a lot of the real problems in the world, and
> in particular, it is very limited in the mathematics it can handle.
>
> I am pretty sure that Prolog is NOT up to handling the logic needed to
> handle the mathematics needed to express Godel's G, or the Halting Problem.
>
> Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you
> have only proven that your limited logic system can't reach them in
> expressibility.
>

Thanks for confirmation, that's what exactly what I was trying to tell
to topic poster in one of my previous posts. Prolog in it's bare form is
a bad theorem solver. It wasn't designed a such.

If you want to deal with such problems maybe it is better to use Coq
theorem prover, I've never used it by myself, but it looks like one of
the best proving assistants out there.

--
Alex Grabowski

[Ben]

And indeed there is a fully formalised proof of GIT in Coq (though I
think it's the slightly tighter Gödel-Rosser version).

--
Ben.

[olcott]

I might take a look at it. The key advantage of Prolog that that by
basing its analysis on facts and rules and having negation as failure it
corrects all of the errors of formal logic systems.

Prolog does not make the mistake of assuming that when an expression is
not true that it must be false. Because of this Prolog can detect
semantically ill-formed expressions that formal logic simply assumes are
correct.

[olcott]

On 5/2/2022 7:11 PM, olcott wrote:
> On 5/2/2022 5:41 PM, Aleksy Grabowski wrote:
>>> IF you are defining that your logic system is limited to what Prolog
>>> can "Prove", that is fine. Just realize that you have just defined
>>> that your logic system can't handle a lot of the real problems in the
>>> world, and in particular, it is very limited in the mathematics it
>>> can handle.
>>>
>>> I am pretty sure that Prolog is NOT up to handling the logic needed
>>> to handle the mathematics needed to express Godel's G, or the Halting
>>> Problem.
>>>
>>> Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you
>>> have only proven that your limited logic system can't reach them in
>>> expressibility.
>>>
>>
>> Thanks for confirmation, that's what exactly what I was trying to tell
>> to topic poster in one of my previous posts. Prolog in it's bare form
>> is a bad theorem solver. It wasn't designed a such.
>>
>> If you want to deal with such problems maybe it is better to use Coq
>> theorem prover, I've never used it by myself, but it looks like one of
>> the best proving assistants out there.
>>
>
> I might take a look at it.

Coq is not an automated theorem prover
https://en.wikipedia.org/wiki/Coq

> The key advantage of Prolog that that by
> basing its analysis on facts and rules

In other words it is based on the sound deductive inference model.

[Richard Damon]

Except that, I believe, in Prolog, all expression are considered to be
either True or False (and default to being called false if they aren't
given as True or provable by the system as True.

Yes, there is a Unification test that allows you to ask if a statement
would create a recursive loop, but that is NOT the same as an ill-formed
expression.

Also, just because Prolog can't prove something doesn't mean it is not
actually provable.

As I said, if you want to limit your logic to what Prolog can determine,
go ahead, but realize you are leaving a lot of logical space as outside
your domain of discussion, and that doesn't mean all that outside is
"ill-formed", unless you are willing to say that Mathematics is ill-formed.

[olcott]

It is true that G is not provable. G is not provable because it is
semantically incorrect in the exactly same way that the Liar Paradox is
semantically incorrect.

Gödel says:
14 Every epistemological antinomy can likewise be used for a similar
undecidability proof

André denied this six times yesterday
The Liar Paradox is an epistemological antinomy, thus can likewise be
used for a similar undecidability proof.

Which means that the Liar Paradox is sufficiently equivalent to Gödel's
G. Which means if the basic mechanism of epistemological antinomy is
shown to be semantically incorrect then Gödel's G is shown to be
semantically incorrect.

[Ben]

olcott <polc...@gmail.com> writes:

> On 5/2/2022 6:43 PM, Ben wrote:
>> Aleksy Grabowski <hur...@gmail.com> writes:

>>> Thanks for confirmation, that's what exactly what I was trying to tell
>>> to topic poster in one of my previous posts. Prolog in it's bare form
>>> is a bad theorem solver. It wasn't designed a such.
>>>
>>> If you want to deal with such problems maybe it is better to use Coq
>>> theorem prover, I've never used it by myself, but it looks like one of
>>> the best proving assistants out there.
>>
>> And indeed there is a fully formalised proof of GIT in Coq (though I
>> think it's the slightly tighter Gödel-Rosser version).
>
> It is true that G is not provable.

G is provable. Proofs abound. I was pointing out one in a proper proof
assistant, Coq.

--
Ben.
"le génie humain a des limites, quand la bêtise humaine n’en a pas"
Alexandre Dumas (fils)