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
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.
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.
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.
On 4/30/22 10:21 PM, olcott wrote:In this case it does. I have spent thousands of hours on the semantic
On 4/30/2022 9:00 PM, Richard Damon wrote:
On 4/30/22 9:42 PM, olcott wrote:
On 4/30/2022 8:08 PM, Richard Damon wrote:
On 4/30/22 3:02 AM, olcott wrote:
LP := ~True(LP) is translated to Prolog:
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
(SWI-Prolog (threaded, 64 bits, version 7.6.4)
https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
Since it isn't giving you a "syntax error", it is probably correct
Prolog. Not sure if your interpretation of the results is correct.
All that false means is that the statement
LP = not(true(LP))
is recursive and that Prolog can't actually evaluate it due to its
limited logic rules.
That is not what Clocksin & Mellish says. They say it is an
erroneous "infinite term" meaning that it specifies infinitely
nested definition like this:
No, that IS what they say, that this sort of recursion fails the test
of Unification, not that it is has no possible logical meaning.
Prolog represents a somewhat basic form of logic, useful for many
cases, but not encompassing all possible reasoning systems.
Maybe it can handle every one that YOU can understand, but it can't
handle many higher order logical structures.
Note, for instance, at least some ways of writing factorial for an
unknown value can lead to an infinite expansion, but the factorial is
well defined for all positive integers. The fact that a "prolog like"
expansion operator might not be able to handle the definition,
doesn't mean it doesn't have meaning.
It is really dumb that you continue to take wild guesses again the
verified facts.
Please read the Clocksin & Mellish (on page 3 of my paper) text and
eliminate your ignorance.
I did. You just don't seem to understand what I am saying because it is
above your head.
Prolog is NOT the defining authority for what is a valid logical
statement, but a system of programming to handle a subset of those
statements (a useful subset, but a subset).
The fact that Prolog doesn't allow something doesn't mean it doesn't
have a logical meaning, only that it doesn't have a logical meaning in Prolog.
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.
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.
On 4/30/2022 9:00 PM, Richard Damon wrote:
On 4/30/22 9:42 PM, olcott wrote:
On 4/30/2022 8:08 PM, Richard Damon wrote:
On 4/30/22 3:02 AM, olcott wrote:
LP := ~True(LP) is translated to Prolog:
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
(SWI-Prolog (threaded, 64 bits, version 7.6.4)
https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
Since it isn't giving you a "syntax error", it is probably correct
Prolog. Not sure if your interpretation of the results is correct.
All that false means is that the statement
LP = not(true(LP))
is recursive and that Prolog can't actually evaluate it due to its
limited logic rules.
That is not what Clocksin & Mellish says. They say it is an erroneous
"infinite term" meaning that it specifies infinitely nested
definition like this:
No, that IS what they say, that this sort of recursion fails the test
of Unification, not that it is has no possible logical meaning.
Prolog represents a somewhat basic form of logic, useful for many
cases, but not encompassing all possible reasoning systems.
Maybe it can handle every one that YOU can understand, but it can't
handle many higher order logical structures.
Note, for instance, at least some ways of writing factorial for an
unknown value can lead to an infinite expansion, but the factorial is
well defined for all positive integers. The fact that a "prolog like"
expansion operator might not be able to handle the definition, doesn't
mean it doesn't have meaning.
It is really dumb that you continue to take wild guesses again the
verified facts.
Please read the Clocksin & Mellish (on page 3 of my paper) text and
eliminate your ignorance.
On 4/30/2022 9:38 PM, Richard Damon wrote:
On 4/30/22 10:21 PM, olcott wrote:In this case it does. I have spent thousands of hours on the semantic
On 4/30/2022 9:00 PM, Richard Damon wrote:
On 4/30/22 9:42 PM, olcott wrote:
On 4/30/2022 8:08 PM, Richard Damon wrote:
On 4/30/22 3:02 AM, olcott wrote:
LP := ~True(LP) is translated to Prolog:
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
(SWI-Prolog (threaded, 64 bits, version 7.6.4)
https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
Since it isn't giving you a "syntax error", it is probably correct >>>>>> Prolog. Not sure if your interpretation of the results is correct. >>>>>>
All that false means is that the statement
LP = not(true(LP))
is recursive and that Prolog can't actually evaluate it due to its >>>>>> limited logic rules.
That is not what Clocksin & Mellish says. They say it is an
erroneous "infinite term" meaning that it specifies infinitely
nested definition like this:
No, that IS what they say, that this sort of recursion fails the
test of Unification, not that it is has no possible logical meaning.
Prolog represents a somewhat basic form of logic, useful for many
cases, but not encompassing all possible reasoning systems.
Maybe it can handle every one that YOU can understand, but it can't
handle many higher order logical structures.
Note, for instance, at least some ways of writing factorial for an
unknown value can lead to an infinite expansion, but the factorial
is well defined for all positive integers. The fact that a "prolog
like" expansion operator might not be able to handle the definition,
doesn't mean it doesn't have meaning.
It is really dumb that you continue to take wild guesses again the
verified facts.
Please read the Clocksin & Mellish (on page 3 of my paper) text and
eliminate your ignorance.
I did. You just don't seem to understand what I am saying because it
is above your head.
Prolog is NOT the defining authority for what is a valid logical
statement, but a system of programming to handle a subset of those
statements (a useful subset, but a subset).
The fact that Prolog doesn't allow something doesn't mean it doesn't
have a logical meaning, only that it doesn't have a logical meaning in
Prolog.
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(...)))))))))))))))
On 4/30/22 10:56 PM, olcott wrote:Not in this case, it is very obvious that no theorem prover can possibly
On 4/30/2022 9:38 PM, Richard Damon wrote:
On 4/30/22 10:21 PM, olcott wrote:In this case it does. I have spent thousands of hours on the semantic
On 4/30/2022 9:00 PM, Richard Damon wrote:
On 4/30/22 9:42 PM, olcott wrote:
On 4/30/2022 8:08 PM, Richard Damon wrote:
On 4/30/22 3:02 AM, olcott wrote:
LP := ~True(LP) is translated to Prolog:
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
(SWI-Prolog (threaded, 64 bits, version 7.6.4)
https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
Since it isn't giving you a "syntax error", it is probably
correct Prolog. Not sure if your interpretation of the results is >>>>>>> correct.
All that false means is that the statement
LP = not(true(LP))
is recursive and that Prolog can't actually evaluate it due to
its limited logic rules.
That is not what Clocksin & Mellish says. They say it is an
erroneous "infinite term" meaning that it specifies infinitely
nested definition like this:
No, that IS what they say, that this sort of recursion fails the
test of Unification, not that it is has no possible logical meaning. >>>>>
Prolog represents a somewhat basic form of logic, useful for many
cases, but not encompassing all possible reasoning systems.
Maybe it can handle every one that YOU can understand, but it can't
handle many higher order logical structures.
Note, for instance, at least some ways of writing factorial for an
unknown value can lead to an infinite expansion, but the factorial
is well defined for all positive integers. The fact that a "prolog
like" expansion operator might not be able to handle the
definition, doesn't mean it doesn't have meaning.
It is really dumb that you continue to take wild guesses again the
verified facts.
Please read the Clocksin & Mellish (on page 3 of my paper) text and
eliminate your ignorance.
I did. You just don't seem to understand what I am saying because it
is above your head.
Prolog is NOT the defining authority for what is a valid logical
statement, but a system of programming to handle a subset of those
statements (a useful subset, but a subset).
The fact that Prolog doesn't allow something doesn't mean it doesn't
have a logical meaning, only that it doesn't have a logical meaning
in Prolog.
error of infinitely recursive definition and written a dozen papers on
it. Glancing at one of two of the words of Clocksin & Mellish does not
count as reading it.
And it appears that you don't understand it, because you still make
category errors when trying to talk about it.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs from the
unification used in Resolution. Most Prolog systems will allow you to
satisfy goals like:
equal(X, X).?-
equal(foo(Y), Y).
that is, they will allow you to match a term against an uninstantiated
subterm of itself. In this example, foo(Y) is matched against Y, which
appears within it. As a result, Y will stand for foo(Y), which is
foo(foo(Y)) (because of what Y stands for), which is foo(foo(foo(Y))),
and so on. So Y ends up standing for some kind of infinite structure.
END:(Clocksin & Mellish 2003:254)
foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))))))
Right. but some infinite structures might actually have meaning.
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é
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
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
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
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.
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
On 4/30/2022 10:11 PM, Richard Damon wrote:
On 4/30/22 10:56 PM, olcott wrote: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.
On 4/30/2022 9:38 PM, Richard Damon wrote:
On 4/30/22 10:21 PM, olcott wrote:In this case it does. I have spent thousands of hours on the semantic
On 4/30/2022 9:00 PM, Richard Damon wrote:
On 4/30/22 9:42 PM, olcott wrote:
On 4/30/2022 8:08 PM, Richard Damon wrote:
On 4/30/22 3:02 AM, olcott wrote:
LP := ~True(LP) is translated to Prolog:
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
(SWI-Prolog (threaded, 64 bits, version 7.6.4)
https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
Since it isn't giving you a "syntax error", it is probably
correct Prolog. Not sure if your interpretation of the results >>>>>>>> is correct.
All that false means is that the statement
LP = not(true(LP))
is recursive and that Prolog can't actually evaluate it due to >>>>>>>> its limited logic rules.
That is not what Clocksin & Mellish says. They say it is an
erroneous "infinite term" meaning that it specifies infinitely
nested definition like this:
No, that IS what they say, that this sort of recursion fails the
test of Unification, not that it is has no possible logical meaning. >>>>>>
Prolog represents a somewhat basic form of logic, useful for many
cases, but not encompassing all possible reasoning systems.
Maybe it can handle every one that YOU can understand, but it
can't handle many higher order logical structures.
Note, for instance, at least some ways of writing factorial for an >>>>>> unknown value can lead to an infinite expansion, but the factorial >>>>>> is well defined for all positive integers. The fact that a "prolog >>>>>> like" expansion operator might not be able to handle the
definition, doesn't mean it doesn't have meaning.
It is really dumb that you continue to take wild guesses again the
verified facts.
Please read the Clocksin & Mellish (on page 3 of my paper) text and
eliminate your ignorance.
I did. You just don't seem to understand what I am saying because it
is above your head.
Prolog is NOT the defining authority for what is a valid logical
statement, but a system of programming to handle a subset of those
statements (a useful subset, but a subset).
The fact that Prolog doesn't allow something doesn't mean it doesn't
have a logical meaning, only that it doesn't have a logical meaning
in Prolog.
error of infinitely recursive definition and written a dozen papers
on it. Glancing at one of two of the words of Clocksin & Mellish does
not count as reading it.
And it appears that you don't understand it, because you still make
category errors when trying to talk about it.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs from the
unification used in Resolution. Most Prolog systems will allow you to
satisfy goals like:
equal(X, X).?-
equal(foo(Y), Y).
that is, they will allow you to match a term against an
uninstantiated subterm of itself. In this example, foo(Y) is matched
against Y, which appears within it. As a result, Y will stand for
foo(Y), which is foo(foo(Y)) (because of what Y stands for), which is
foo(foo(foo(Y))), and so on. So Y ends up standing for some kind of
infinite structure.
END:(Clocksin & Mellish 2003:254)
foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))))))
Right. but some infinite structures might actually have meaning.
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.
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
On 4/30/2022 9:15 PM, olcott wrote:
On 4/30/2022 10:11 PM, Richard Damon wrote:
On 4/30/22 10:56 PM, olcott wrote:Not in this case, it is very obvious that no theorem prover can
On 4/30/2022 9:38 PM, Richard Damon wrote:
On 4/30/22 10:21 PM, olcott wrote:In this case it does. I have spent thousands of hours on the
On 4/30/2022 9:00 PM, Richard Damon wrote:
On 4/30/22 9:42 PM, olcott wrote:
On 4/30/2022 8:08 PM, Richard Damon wrote:
On 4/30/22 3:02 AM, olcott wrote:
LP := ~True(LP) is translated to Prolog:
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
(SWI-Prolog (threaded, 64 bits, version 7.6.4)
https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
Since it isn't giving you a "syntax error", it is probably
correct Prolog. Not sure if your interpretation of the results >>>>>>>>> is correct.
All that false means is that the statement
LP = not(true(LP))
is recursive and that Prolog can't actually evaluate it due to >>>>>>>>> its limited logic rules.
That is not what Clocksin & Mellish says. They say it is an
erroneous "infinite term" meaning that it specifies infinitely >>>>>>>> nested definition like this:
No, that IS what they say, that this sort of recursion fails the >>>>>>> test of Unification, not that it is has no possible logical meaning. >>>>>>>
Prolog represents a somewhat basic form of logic, useful for many >>>>>>> cases, but not encompassing all possible reasoning systems.
Maybe it can handle every one that YOU can understand, but it
can't handle many higher order logical structures.
Note, for instance, at least some ways of writing factorial for
an unknown value can lead to an infinite expansion, but the
factorial is well defined for all positive integers. The fact
that a "prolog like" expansion operator might not be able to
handle the definition, doesn't mean it doesn't have meaning.
It is really dumb that you continue to take wild guesses again the >>>>>> verified facts.
Please read the Clocksin & Mellish (on page 3 of my paper) text
and eliminate your ignorance.
I did. You just don't seem to understand what I am saying because
it is above your head.
Prolog is NOT the defining authority for what is a valid logical
statement, but a system of programming to handle a subset of those
statements (a useful subset, but a subset).
The fact that Prolog doesn't allow something doesn't mean it
doesn't have a logical meaning, only that it doesn't have a logical
meaning in Prolog.
semantic error of infinitely recursive definition and written a
dozen papers on it. Glancing at one of two of the words of Clocksin
& Mellish does not count as reading it.
And it appears that you don't understand it, because you still make
category errors when trying to talk about it.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs from the
unification used in Resolution. Most Prolog systems will allow you
to satisfy goals like:
equal(X, X).?-
equal(foo(Y), Y).
that is, they will allow you to match a term against an
uninstantiated subterm of itself. In this example, foo(Y) is matched
against Y, which appears within it. As a result, Y will stand for
foo(Y), which is foo(foo(Y)) (because of what Y stands for), which
is foo(foo(foo(Y))), and so on. So Y ends up standing for some kind
of infinite structure.
END:(Clocksin & Mellish 2003:254)
foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))))))
Right. but some infinite structures might actually have meaning.
possibly prove any infinite expression. It is the same thing as a
program that is stuck in an infinite loop.
Richard wrote and the asshole (PO) snipped ------------------------------------------
Right. but some infinite structures might actually have meaning. The
fact that Prolog uses certain limited method to figure out meaning
doesn't mean that other methods can't find the meaning.
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.
On 5/1/22 6:58 AM, olcott wrote:
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
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.
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.
On 5/1/2022 6:12 AM, Richard Damon wrote:
On 5/1/22 6:58 AM, olcott wrote:
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
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.
Prolog has a better model in that it can detect semantic paradoxes.
LP ↔ ¬True(LP) is correctly assessed as neither true nor false.
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.
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.
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.
On 5/1/2022 6:26 AM, Richard Damon wrote:
On 5/1/22 7:06 AM, olcott wrote:
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.
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.
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. >>>
On 5/1/22 7:45 AM, olcott wrote:
On 5/1/2022 6:12 AM, Richard Damon wrote:
On 5/1/22 6:58 AM, olcott wrote:
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
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.
Prolog has a better model in that it can detect semantic paradoxes.
LP ↔ ¬True(LP) is correctly assessed as neither true nor false.
"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.
On 5/1/22 7:06 AM, olcott wrote:
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.
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.
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. >>
On 4/30/22 11:15 PM, olcott wrote:
On 4/30/2022 10:11 PM, Richard Damon wrote:
On 4/30/22 10:56 PM, olcott wrote:Not in this case, it is very obvious that no theorem prover can
On 4/30/2022 9:38 PM, Richard Damon wrote:
On 4/30/22 10:21 PM, olcott wrote:In this case it does. I have spent thousands of hours on the
On 4/30/2022 9:00 PM, Richard Damon wrote:
On 4/30/22 9:42 PM, olcott wrote:
On 4/30/2022 8:08 PM, Richard Damon wrote:
On 4/30/22 3:02 AM, olcott wrote:
LP := ~True(LP) is translated to Prolog:
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
(SWI-Prolog (threaded, 64 bits, version 7.6.4)
https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
Since it isn't giving you a "syntax error", it is probably
correct Prolog. Not sure if your interpretation of the results >>>>>>>>> is correct.
All that false means is that the statement
LP = not(true(LP))
is recursive and that Prolog can't actually evaluate it due to >>>>>>>>> its limited logic rules.
That is not what Clocksin & Mellish says. They say it is an
erroneous "infinite term" meaning that it specifies infinitely >>>>>>>> nested definition like this:
No, that IS what they say, that this sort of recursion fails the >>>>>>> test of Unification, not that it is has no possible logical meaning. >>>>>>>
Prolog represents a somewhat basic form of logic, useful for many >>>>>>> cases, but not encompassing all possible reasoning systems.
Maybe it can handle every one that YOU can understand, but it
can't handle many higher order logical structures.
Note, for instance, at least some ways of writing factorial for
an unknown value can lead to an infinite expansion, but the
factorial is well defined for all positive integers. The fact
that a "prolog like" expansion operator might not be able to
handle the definition, doesn't mean it doesn't have meaning.
It is really dumb that you continue to take wild guesses again the >>>>>> verified facts.
Please read the Clocksin & Mellish (on page 3 of my paper) text
and eliminate your ignorance.
I did. You just don't seem to understand what I am saying because
it is above your head.
Prolog is NOT the defining authority for what is a valid logical
statement, but a system of programming to handle a subset of those
statements (a useful subset, but a subset).
The fact that Prolog doesn't allow something doesn't mean it
doesn't have a logical meaning, only that it doesn't have a logical
meaning in Prolog.
semantic error of infinitely recursive definition and written a
dozen papers on it. Glancing at one of two of the words of Clocksin
& Mellish does not count as reading it.
And it appears that you don't understand it, because you still make
category errors when trying to talk about it.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs from the
unification used in Resolution. Most Prolog systems will allow you
to satisfy goals like:
equal(X, X).?-
equal(foo(Y), Y).
that is, they will allow you to match a term against an
uninstantiated subterm of itself. In this example, foo(Y) is matched
against Y, which appears within it. As a result, Y will stand for
foo(Y), which is foo(foo(Y)) (because of what Y stands for), which
is foo(foo(foo(Y))), and so on. So Y ends up standing for some kind
of infinite structure.
END:(Clocksin & Mellish 2003:254)
foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))))))
Right. but some infinite structures might actually have meaning.
possibly prove any infinite expression. It is the same thing as a
program that is stuck in an infinite loop.
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.
On 5/1/22 7:54 AM, olcott wrote:
On 5/1/2022 6:26 AM, Richard Damon wrote:
On 5/1/22 7:06 AM, olcott wrote:
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.
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.
That is counter-factual. unify_with_occurs_check determines that it
would require infinite memory and then aborts its evaluation.
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.
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.
On 5/1/2022 7:01 AM, Richard Damon wrote:
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.
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. >>>
So all Clocksin & Melish is saying is that such an expression fails in
PROLOG, not that it doesn't have a valid logical meaning.
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.
On 4/30/2022 9:15 PM, olcott wrote:
On 4/30/2022 10:11 PM, Richard Damon wrote:
On 4/30/22 10:56 PM, olcott wrote:Not in this case, it is very obvious that no theorem prover can
On 4/30/2022 9:38 PM, Richard Damon wrote:
On 4/30/22 10:21 PM, olcott wrote:In this case it does. I have spent thousands of hours on the
On 4/30/2022 9:00 PM, Richard Damon wrote:
On 4/30/22 9:42 PM, olcott wrote:
On 4/30/2022 8:08 PM, Richard Damon wrote:
On 4/30/22 3:02 AM, olcott wrote:
LP := ~True(LP) is translated to Prolog:
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
(SWI-Prolog (threaded, 64 bits, version 7.6.4)
https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
Since it isn't giving you a "syntax error", it is probably
correct Prolog. Not sure if your interpretation of the
results is correct.
All that false means is that the statement
LP = not(true(LP))
is recursive and that Prolog can't actually evaluate it due
to its limited logic rules.
That is not what Clocksin & Mellish says. They say it is an
erroneous "infinite term" meaning that it specifies
infinitely nested definition like this:
No, that IS what they say, that this sort of recursion fails
the test of Unification, not that it is has no possible
logical meaning.
Prolog represents a somewhat basic form of logic, useful for
many cases, but not encompassing all possible reasoning
systems.
Maybe it can handle every one that YOU can understand, but it
can't handle many higher order logical structures.
Note, for instance, at least some ways of writing factorial
for an unknown value can lead to an infinite expansion, but
the factorial is well defined for all positive integers. The
fact that a "prolog like" expansion operator might not be able
to handle the definition, doesn't mean it doesn't have meaning.
It is really dumb that you continue to take wild guesses again
the verified facts.
Please read the Clocksin & Mellish (on page 3 of my paper) text
and eliminate your ignorance.
I did. You just don't seem to understand what I am saying
because it is above your head.
Prolog is NOT the defining authority for what is a valid logical
statement, but a system of programming to handle a subset of
those statements (a useful subset, but a subset).
The fact that Prolog doesn't allow something doesn't mean it
doesn't have a logical meaning, only that it doesn't have a
logical meaning in Prolog.
semantic error of infinitely recursive definition and written a
dozen papers on it. Glancing at one of two of the words of
Clocksin & Mellish does not count as reading it.
And it appears that you don't understand it, because you still
make category errors when trying to talk about it.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs from
the unification used in Resolution. Most Prolog systems will
allow you to satisfy goals like:
equal(X, X).?-
equal(foo(Y), Y).
that is, they will allow you to match a term against an
uninstantiated subterm of itself. In this example, foo(Y) is
matched against Y, which appears within it. As a result, Y will
stand for foo(Y), which is foo(foo(Y)) (because of what Y stands
for), which is foo(foo(foo(Y))), and so on. So Y ends up standing
for some kind of infinite structure.
END:(Clocksin & Mellish 2003:254)
foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))))))
Right. but some infinite structures might actually have meaning.
possibly prove any infinite expression. It is the same thing as a
program that is stuck in an infinite loop.
Richard wrote and the asshole (PO) snipped ------------------------------------------
Right. but some infinite structures might actually have meaning. The
fact that Prolog uses certain limited method to figure out meaning
doesn't mean that other methods can't find the meaning.
Just like:
Fact(n) := (N == 1) ? 1 : N*Fact(n-1);
On Sat, 30 Apr 2022 23:24:05 -0600
Jeff Barnett <jbb@notatt.com> wrote:
On 4/30/2022 9:15 PM, olcott wrote:
On 4/30/2022 10:11 PM, Richard Damon wrote:
On 4/30/22 10:56 PM, olcott wrote:Not in this case, it is very obvious that no theorem prover can
On 4/30/2022 9:38 PM, Richard Damon wrote:
On 4/30/22 10:21 PM, olcott wrote:In this case it does. I have spent thousands of hours on the
On 4/30/2022 9:00 PM, Richard Damon wrote:
On 4/30/22 9:42 PM, olcott wrote:
On 4/30/2022 8:08 PM, Richard Damon wrote:
On 4/30/22 3:02 AM, olcott wrote:
LP := ~True(LP) is translated to Prolog:
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
(SWI-Prolog (threaded, 64 bits, version 7.6.4)
https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
Since it isn't giving you a "syntax error", it is probably >>>>>>>>>> correct Prolog. Not sure if your interpretation of the
results is correct.
All that false means is that the statement
LP = not(true(LP))
is recursive and that Prolog can't actually evaluate it due >>>>>>>>>> to its limited logic rules.
That is not what Clocksin & Mellish says. They say it is an
erroneous "infinite term" meaning that it specifies
infinitely nested definition like this:
No, that IS what they say, that this sort of recursion fails
the test of Unification, not that it is has no possible
logical meaning.
Prolog represents a somewhat basic form of logic, useful for
many cases, but not encompassing all possible reasoning
systems.
Maybe it can handle every one that YOU can understand, but it
can't handle many higher order logical structures.
Note, for instance, at least some ways of writing factorial
for an unknown value can lead to an infinite expansion, but
the factorial is well defined for all positive integers. The
fact that a "prolog like" expansion operator might not be able >>>>>>>> to handle the definition, doesn't mean it doesn't have meaning. >>>>>>>>
It is really dumb that you continue to take wild guesses again
the verified facts.
Please read the Clocksin & Mellish (on page 3 of my paper) text
and eliminate your ignorance.
I did. You just don't seem to understand what I am saying
because it is above your head.
Prolog is NOT the defining authority for what is a valid logical
statement, but a system of programming to handle a subset of
those statements (a useful subset, but a subset).
The fact that Prolog doesn't allow something doesn't mean it
doesn't have a logical meaning, only that it doesn't have a
logical meaning in Prolog.
semantic error of infinitely recursive definition and written a
dozen papers on it. Glancing at one of two of the words of
Clocksin & Mellish does not count as reading it.
And it appears that you don't understand it, because you still
make category errors when trying to talk about it.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs from
the unification used in Resolution. Most Prolog systems will
allow you to satisfy goals like:
equal(X, X).?-
equal(foo(Y), Y).
that is, they will allow you to match a term against an
uninstantiated subterm of itself. In this example, foo(Y) is
matched against Y, which appears within it. As a result, Y will
stand for foo(Y), which is foo(foo(Y)) (because of what Y stands
for), which is foo(foo(foo(Y))), and so on. So Y ends up standing
for some kind of infinite structure.
END:(Clocksin & Mellish 2003:254)
foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))))))
Right. but some infinite structures might actually have meaning.
possibly prove any infinite expression. It is the same thing as a
program that is stuck in an infinite loop.
Richard wrote and the asshole (PO) snipped
------------------------------------------
Right. but some infinite structures might actually have meaning. The
fact that Prolog uses certain limited method to figure out meaning
doesn't mean that other methods can't find the meaning.
Just like:
Fact(n) := (N == 1) ? 1 : N*Fact(n-1);
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
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é
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.
G ↔ ¬Provable(F, G) is an epistemological antinomy therefore it is
necessarily sufficient.
There is no antinomy involved in that formula, epistemological or
otherwise.
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.
The reason I keep asking you to define your 'True' predicate is simply
that it seems utterly unnecessary and pointless.
If you believe
otherwise, then please explain what the difference between the following formulae might possibly be:
(1) LP ↔ ¬True(LP)
(2) True(LP) ↔ ¬True(LP)
(3) LP ↔ ¬LP
(4) True(LP) ↔ ¬LP
André
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"
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.
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
On Sat, 30 Apr 2022 23:24:05 -0600
Jeff Barnett <jbb@notatt.com> wrote:
On 4/30/2022 9:15 PM, olcott wrote:
On 4/30/2022 10:11 PM, Richard Damon wrote:
On 4/30/22 10:56 PM, olcott wrote:Not in this case, it is very obvious that no theorem prover can
On 4/30/2022 9:38 PM, Richard Damon wrote:
On 4/30/22 10:21 PM, olcott wrote:In this case it does. I have spent thousands of hours on the
On 4/30/2022 9:00 PM, Richard Damon wrote:
On 4/30/22 9:42 PM, olcott wrote:
On 4/30/2022 8:08 PM, Richard Damon wrote:
On 4/30/22 3:02 AM, olcott wrote:
LP := ~True(LP) is translated to Prolog:
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
(SWI-Prolog (threaded, 64 bits, version 7.6.4)
https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
Since it isn't giving you a "syntax error", it is probably >>>>>>>>>> correct Prolog. Not sure if your interpretation of the
results is correct.
All that false means is that the statement
LP = not(true(LP))
is recursive and that Prolog can't actually evaluate it due >>>>>>>>>> to its limited logic rules.
That is not what Clocksin & Mellish says. They say it is an
erroneous "infinite term" meaning that it specifies
infinitely nested definition like this:
No, that IS what they say, that this sort of recursion fails
the test of Unification, not that it is has no possible
logical meaning.
Prolog represents a somewhat basic form of logic, useful for
many cases, but not encompassing all possible reasoning
systems.
Maybe it can handle every one that YOU can understand, but it
can't handle many higher order logical structures.
Note, for instance, at least some ways of writing factorial
for an unknown value can lead to an infinite expansion, but
the factorial is well defined for all positive integers. The
fact that a "prolog like" expansion operator might not be able >>>>>>>> to handle the definition, doesn't mean it doesn't have meaning. >>>>>>>>
It is really dumb that you continue to take wild guesses again
the verified facts.
Please read the Clocksin & Mellish (on page 3 of my paper) text
and eliminate your ignorance.
I did. You just don't seem to understand what I am saying
because it is above your head.
Prolog is NOT the defining authority for what is a valid logical
statement, but a system of programming to handle a subset of
those statements (a useful subset, but a subset).
The fact that Prolog doesn't allow something doesn't mean it
doesn't have a logical meaning, only that it doesn't have a
logical meaning in Prolog.
semantic error of infinitely recursive definition and written a
dozen papers on it. Glancing at one of two of the words of
Clocksin & Mellish does not count as reading it.
And it appears that you don't understand it, because you still
make category errors when trying to talk about it.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs from
the unification used in Resolution. Most Prolog systems will
allow you to satisfy goals like:
equal(X, X).?-
equal(foo(Y), Y).
that is, they will allow you to match a term against an
uninstantiated subterm of itself. In this example, foo(Y) is
matched against Y, which appears within it. As a result, Y will
stand for foo(Y), which is foo(foo(Y)) (because of what Y stands
for), which is foo(foo(foo(Y))), and so on. So Y ends up standing
for some kind of infinite structure.
END:(Clocksin & Mellish 2003:254)
foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))))))
Right. but some infinite structures might actually have meaning.
possibly prove any infinite expression. It is the same thing as a
program that is stuck in an infinite loop.
Richard wrote and the asshole (PO) snipped
------------------------------------------
Right. but some infinite structures might actually have meaning. The
fact that Prolog uses certain limited method to figure out meaning
doesn't mean that other methods can't find the meaning.
Just like:
Fact(n) := (N == 1) ? 1 : N*Fact(n-1);
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
On 5/1/2022 12:24 AM, Jeff Barnett wrote:
On 4/30/2022 9:15 PM, olcott wrote:
On 4/30/2022 10:11 PM, Richard Damon wrote:
On 4/30/22 10:56 PM, olcott wrote:Not in this case, it is very obvious that no theorem prover can
On 4/30/2022 9:38 PM, Richard Damon wrote:
On 4/30/22 10:21 PM, olcott wrote:In this case it does. I have spent thousands of hours on the
On 4/30/2022 9:00 PM, Richard Damon wrote:
On 4/30/22 9:42 PM, olcott wrote:
On 4/30/2022 8:08 PM, Richard Damon wrote:
On 4/30/22 3:02 AM, olcott wrote:
LP := ~True(LP) is translated to Prolog:
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
(SWI-Prolog (threaded, 64 bits, version 7.6.4)
https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
Since it isn't giving you a "syntax error", it is probably >>>>>>>>>> correct Prolog. Not sure if your interpretation of the results >>>>>>>>>> is correct.
All that false means is that the statement
LP = not(true(LP))
is recursive and that Prolog can't actually evaluate it due to >>>>>>>>>> its limited logic rules.
That is not what Clocksin & Mellish says. They say it is an
erroneous "infinite term" meaning that it specifies infinitely >>>>>>>>> nested definition like this:
No, that IS what they say, that this sort of recursion fails the >>>>>>>> test of Unification, not that it is has no possible logical
meaning.
Prolog represents a somewhat basic form of logic, useful for
many cases, but not encompassing all possible reasoning systems. >>>>>>>>
Maybe it can handle every one that YOU can understand, but it
can't handle many higher order logical structures.
Note, for instance, at least some ways of writing factorial for >>>>>>>> an unknown value can lead to an infinite expansion, but the
factorial is well defined for all positive integers. The fact
that a "prolog like" expansion operator might not be able to
handle the definition, doesn't mean it doesn't have meaning.
It is really dumb that you continue to take wild guesses again
the verified facts.
Please read the Clocksin & Mellish (on page 3 of my paper) text
and eliminate your ignorance.
I did. You just don't seem to understand what I am saying because
it is above your head.
Prolog is NOT the defining authority for what is a valid logical
statement, but a system of programming to handle a subset of those >>>>>> statements (a useful subset, but a subset).
The fact that Prolog doesn't allow something doesn't mean it
doesn't have a logical meaning, only that it doesn't have a
logical meaning in Prolog.
semantic error of infinitely recursive definition and written a
dozen papers on it. Glancing at one of two of the words of Clocksin
& Mellish does not count as reading it.
And it appears that you don't understand it, because you still make
category errors when trying to talk about it.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs from
the unification used in Resolution. Most Prolog systems will allow
you to satisfy goals like:
equal(X, X).?-
equal(foo(Y), Y).
that is, they will allow you to match a term against an
uninstantiated subterm of itself. In this example, foo(Y) is
matched against Y, which appears within it. As a result, Y will
stand for foo(Y), which is foo(foo(Y)) (because of what Y stands
for), which is foo(foo(foo(Y))), and so on. So Y ends up standing
for some kind of infinite structure.
END:(Clocksin & Mellish 2003:254)
foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))))))
Right. but some infinite structures might actually have meaning.
possibly prove any infinite expression. It is the same thing as a
program that is stuck in an infinite loop.
Richard wrote and the asshole (PO) snipped
------------------------------------------
Right. but some infinite structures might actually have meaning. The
fact that Prolog uses certain limited method to figure out meaning
doesn't mean that other methods can't find the meaning.
The question is not whether some infinite structures have meaning that
is the dishonest dodge of the strawman error.
The question is whether on not the expression at hand has meaning or is simply semantically incoherent. I just posted all of the Clocksin &
Mellish text in my prior post to make this more clear.
This example expanded from Clocksin & Mellish conclusively proves that
some expressions of language are incorrect:
foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))
Just like:
Fact(n) := (N == 1) ? 1 : N*Fact(n-1);
if naively expanded has an infinite expansion.
But, based on mathematical knowledge, and can actually be proven from
the definition, something like Fact(n+1)/fact(n), even for an unknown
n, can be reduced without the need to actually expend infinite
operations.
Note, this is actual shown in your case of H(H^,H^). Yes, if H doesn't
abort its simulation, then for THAT H^, we have that H^(H^) is
non-halting, but so is H(H^,H^), and thus THAT H / H^ pair fails to be
a counter example
When you program H to abort its simulation of H^ at some point, and
build your H^ on that H, then H(H^,H^), will return the non-halting
answer, and H^(H^) when PROPERLY run or simulated halts, because H has
the same "cut off" logic at the factorial above.
The naive expansion thinks it is infinite, but the correct expansion
sees the cut off and sees that it is actually finite.
----------------------------------------------------------------------
A good symbolic manipulation system or a theorem prover with
appropriate axioms and rules of inference could surely handle forms
such as Fact(n+1)/fact(n) without breathing hard. It is only you, an
ignorant fool, who seems to think that the unthinking infinite
unrolling of a form must occur. Only you would think that a solver
system would completely unroll a form before analyzing it and applying
transformations to it.
Son, it don't work that way (unless you are defining and making a mess
trying to write the system yourself). Systems usually have rules that
make small incremental transformations and usually search breadth
first with perhaps a limited amount of depth first interludes. If they
don't use a breadth first strategy, they will not be able to claim the
completeness property. (See resolution theorem prover literature for
some explanation. You wont understand it but you can cite as if you did!)
Richard was trying to explain this to you in the snipped portion I
recited just above. Question for Peter holding his pecker: How do you
always and I mean always manage to delete the part of a message you
respond too that addresses the point you now try to make?
A typically subsequence you might see in the trace: would include in
order but not necessarily consecutively:
Fact(n+1)/Fact(n)
(n+1)*Fact(n)/Fact(n)
(n+1)
Some interspersed terms such as Fact(n+1)/(n*Fact(n-1)) would be found
too. In some circumstances, these other terms might be helpful. A
theorem prover or manipulator does all of this, breadth first, hoping
to blindly stumble on a solution. You can provide heuristics that
might speed up the process but no advice short of an oracle will get
you even one more result. (Another manifestation of HP.) It's the slow
grinding through the possibilities that guarantees that if a result
can be found, it will be found. And all the theory that you don't
understand says that's the best you can do.
Ben and I disagree on reasons for your type of total dishonesty. He
thinks that you are so self deluded that you actual believe what you
are saying; that you are so self deluded that the dishonest utterances
are just your subconscious protecting your already damaged ego. To
that, I say phooey; you are just a long term troll who lies a lot
about math, about your history and health, and about your
accomplishments.
I don't believe that you will read this before you start to respond
but that's okay. Understanding is not required. Neither is respect in
either direction.
On 5/1/2022 6:18 AM, Richard Damon wrote:
On 4/30/22 11:15 PM, olcott wrote:
On 4/30/2022 10:11 PM, Richard Damon wrote:
On 4/30/22 10:56 PM, olcott wrote:Not in this case, it is very obvious that no theorem prover can
On 4/30/2022 9:38 PM, Richard Damon wrote:
On 4/30/22 10:21 PM, olcott wrote:In this case it does. I have spent thousands of hours on the
On 4/30/2022 9:00 PM, Richard Damon wrote:
On 4/30/22 9:42 PM, olcott wrote:
On 4/30/2022 8:08 PM, Richard Damon wrote:
On 4/30/22 3:02 AM, olcott wrote:
LP := ~True(LP) is translated to Prolog:
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
(SWI-Prolog (threaded, 64 bits, version 7.6.4)
https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
Since it isn't giving you a "syntax error", it is probably >>>>>>>>>> correct Prolog. Not sure if your interpretation of the results >>>>>>>>>> is correct.
All that false means is that the statement
LP = not(true(LP))
is recursive and that Prolog can't actually evaluate it due to >>>>>>>>>> its limited logic rules.
That is not what Clocksin & Mellish says. They say it is an
erroneous "infinite term" meaning that it specifies infinitely >>>>>>>>> nested definition like this:
No, that IS what they say, that this sort of recursion fails the >>>>>>>> test of Unification, not that it is has no possible logical
meaning.
Prolog represents a somewhat basic form of logic, useful for
many cases, but not encompassing all possible reasoning systems. >>>>>>>>
Maybe it can handle every one that YOU can understand, but it
can't handle many higher order logical structures.
Note, for instance, at least some ways of writing factorial for >>>>>>>> an unknown value can lead to an infinite expansion, but the
factorial is well defined for all positive integers. The fact
that a "prolog like" expansion operator might not be able to
handle the definition, doesn't mean it doesn't have meaning.
It is really dumb that you continue to take wild guesses again
the verified facts.
Please read the Clocksin & Mellish (on page 3 of my paper) text
and eliminate your ignorance.
I did. You just don't seem to understand what I am saying because
it is above your head.
Prolog is NOT the defining authority for what is a valid logical
statement, but a system of programming to handle a subset of those >>>>>> statements (a useful subset, but a subset).
The fact that Prolog doesn't allow something doesn't mean it
doesn't have a logical meaning, only that it doesn't have a
logical meaning in Prolog.
semantic error of infinitely recursive definition and written a
dozen papers on it. Glancing at one of two of the words of Clocksin
& Mellish does not count as reading it.
And it appears that you don't understand it, because you still make
category errors when trying to talk about it.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs from
the unification used in Resolution. Most Prolog systems will allow
you to satisfy goals like:
equal(X, X).?-
equal(foo(Y), Y).
that is, they will allow you to match a term against an
uninstantiated subterm of itself. In this example, foo(Y) is
matched against Y, which appears within it. As a result, Y will
stand for foo(Y), which is foo(foo(Y)) (because of what Y stands
for), which is foo(foo(foo(Y))), and so on. So Y ends up standing
for some kind of infinite structure.
END:(Clocksin & Mellish 2003:254)
foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))))))
Right. but some infinite structures might actually have meaning.
possibly prove any infinite expression. It is the same thing as a
program that is stuck in an infinite loop.
As Jeff pointed out, your claim is shown false, that some statements
with infinite expansions can be worked with by some automatic solvers.
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.
On 5/1/2022 7:07 AM, Richard Damon wrote:
On 5/1/22 7:45 AM, olcott wrote:
On 5/1/2022 6:12 AM, Richard Damon wrote:
On 5/1/22 6:58 AM, olcott wrote:
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
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.
Prolog has a better model in that it can detect semantic paradoxes.
LP ↔ ¬True(LP) is correctly assessed as neither true nor false.
"Better" is as subjective word unless you define an objective criteria.
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.
On 5/1/2022 7:11 AM, Richard Damon wrote:
On 5/1/22 7:54 AM, olcott wrote:
On 5/1/2022 6:26 AM, Richard Damon wrote:
On 5/1/22 7:06 AM, olcott wrote:
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.
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.
That is counter-factual. unify_with_occurs_check determines that it
would require infinite memory and then aborts its evaluation.
You misunderstand what it says. It says that it can't figure how to
express the statement without a cycle.
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.
On Sun, 1 May 2022 12:01:01 -0500
olcott <NoOne@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
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 <NoOne@NoWhere.com> wrote:
On 5/1/2022 11:21 AM, André G. Isaak wrote:You are not in my kill file: I don't always reply to what you say
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
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é
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?
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é
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 <NoOne@NoWhere.com> wrote:
On 5/1/2022 11:21 AM, André G. Isaak wrote:You are not in my kill file: I don't always reply to what you say
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
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.
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.
On 2022-05-01 13:32, olcott wrote:14 Every epistemological antinomy can likewise be used for a similar undecidability proof
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.
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.
On 5/1/2022 2:44 PM, André G. Isaak wrote:
On 2022-05-01 13:32, olcott wrote:14 Every epistemological antinomy can likewise be used for a similar undecidability proof
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.
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.
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.
On 2022-05-01 14:03, olcott wrote:
On 5/1/2022 2:54 PM, André G. Isaak wrote:
On 2022-05-01 13:48, olcott wrote:
On 5/1/2022 2:44 PM, André G. Isaak wrote:
On 2022-05-01 13:32, olcott wrote:14 Every epistemological antinomy can likewise be used for a similar
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.
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.
undecidability proof
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.
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'?
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:
On 2022-05-01 13:48, olcott wrote:
On 5/1/2022 2:44 PM, André G. Isaak wrote:
On 2022-05-01 13:32, olcott wrote:14 Every epistemological antinomy can likewise be used for a similar >>>>> undecidability proof
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.
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.
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.
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
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:
On 2022-05-01 13:48, olcott wrote:
On 5/1/2022 2:44 PM, André G. Isaak wrote:
On 2022-05-01 13:32, olcott wrote:14 Every epistemological antinomy can likewise be used for a similar >>>>> undecidability proof
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.
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.
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.
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
On 2022-05-01 14:42, olcott wrote:
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:
On 2022-05-01 13:48, olcott wrote:
On 5/1/2022 2:44 PM, André G. Isaak wrote:
On 2022-05-01 13:32, olcott wrote:14 Every epistemological antinomy can likewise be used for a similar >>>>>> undecidability proof
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:And how can you possibly justify your claim that Gödel's G is >>>>>>>>> not a truth bearer?
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) >>>>>>>>>
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.
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.
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.
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
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.
André
On 2022-05-01 14:42, olcott wrote:
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:
On 2022-05-01 13:48, olcott wrote:
On 5/1/2022 2:44 PM, André G. Isaak wrote:
On 2022-05-01 13:32, olcott wrote:14 Every epistemological antinomy can likewise be used for a similar >>>>>> undecidability proof
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:And how can you possibly justify your claim that Gödel's G is >>>>>>>>> not a truth bearer?
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) >>>>>>>>>
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.
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.
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.
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
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.
André
On 5/1/2022 3:51 PM, André G. Isaak wrote:
On 2022-05-01 14:42, olcott wrote:
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:
On 2022-05-01 13:48, olcott wrote:
On 5/1/2022 2:44 PM, André G. Isaak wrote:
On 2022-05-01 13:32, olcott wrote:14 Every epistemological antinomy can likewise be used for a similar >>>>>>> undecidability proof
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:And how can you possibly justify your claim that Gödel's G is >>>>>>>>>> not a truth bearer?
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) >>>>>>>>>>
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.
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.
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.
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
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.
André
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.
On 2022-05-01 16:04, olcott wrote:
On 5/1/2022 3:51 PM, André G. Isaak wrote:
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.
André
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.
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.
André
On 5/1/22 6:04 PM, olcott wrote:
On 5/1/2022 3:51 PM, André G. Isaak wrote:
On 2022-05-01 14:42, olcott wrote:
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:
On 2022-05-01 13:48, olcott wrote:
On 5/1/2022 2:44 PM, André G. Isaak wrote:
On 2022-05-01 13:32, olcott wrote:14 Every epistemological antinomy can likewise be used for a
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:And how can you possibly justify your claim that Gödel's G is >>>>>>>>>>> not a truth bearer?
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) >>>>>>>>>>>
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.
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.
similar
undecidability proof
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.
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
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.
André
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.
On 5/1/2022 3:51 PM, André G. Isaak wrote:
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.
André
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.
On 5/1/2022 5:37 PM, André G. Isaak wrote:
On 2022-05-01 16:04, olcott wrote:
On 5/1/2022 3:51 PM, André G. Isaak wrote:
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.
André
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.
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.
André
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.
On 5/1/2022 5:08 PM, Richard Damon wrote:
On 5/1/22 6:04 PM, olcott wrote:
On 5/1/2022 3:51 PM, André G. Isaak wrote:
On 2022-05-01 14:42, olcott wrote:
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:
On 2022-05-01 13:48, olcott wrote:
On 5/1/2022 2:44 PM, André G. Isaak wrote:
On 2022-05-01 13:32, olcott wrote:14 Every epistemological antinomy can likewise be used for a >>>>>>>>> similar
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:And how can you possibly justify your claim that Gödel's G >>>>>>>>>>>> is not a truth bearer?
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) >>>>>>>>>>>>
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.
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.
undecidability proof
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.
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
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.
André
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
On 5/1/22 6:39 PM, olcott wrote:
sufficiently equivalent
You can PROVE it?
On 5/1/22 6:39 PM, olcott wrote:
On 5/1/2022 5:08 PM, Richard Damon wrote:
On 5/1/22 6:04 PM, olcott wrote:
On 5/1/2022 3:51 PM, André G. Isaak wrote:
On 2022-05-01 14:42, olcott wrote:
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:
On 2022-05-01 13:48, olcott wrote:
On 5/1/2022 2:44 PM, André G. Isaak wrote:
On 2022-05-01 13:32, olcott wrote:14 Every epistemological antinomy can likewise be used for a >>>>>>>>>> similar
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:And how can you possibly justify your claim that Gödel's G >>>>>>>>>>>>> is not a truth bearer?
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) >>>>>>>>>>>>>
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.
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.
undecidability proof
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.
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
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.
André
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?
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.
On 5/1/22 8:58 PM, olcott wrote:
On 5/1/2022 6:18 PM, Richard Damon wrote:
On 5/1/22 6:39 PM, olcott wrote:
On 5/1/2022 5:08 PM, Richard Damon wrote:
On 5/1/22 6:04 PM, olcott wrote:sufficiently equivalent
On 5/1/2022 3:51 PM, André G. Isaak wrote:
On 2022-05-01 14:42, olcott wrote:
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:
On 2022-05-01 13:48, olcott wrote:
On 5/1/2022 2:44 PM, André G. Isaak wrote:
On 2022-05-01 13:32, olcott wrote:14 Every epistemological antinomy can likewise be used for a >>>>>>>>>>>> similar
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:And how can you possibly justify your claim that Gödel's >>>>>>>>>>>>>>> G is not a truth bearer?
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) >>>>>>>>>>>>>>>
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.
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.
undecidability proof
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.
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
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.
André
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. >>>>
You can PROVE it?
I backed André into a corner and forced him to quit lying
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.
On 5/1/2022 6:18 PM, Richard Damon wrote:
On 5/1/22 6:39 PM, olcott wrote:
On 5/1/2022 5:08 PM, Richard Damon wrote:
On 5/1/22 6:04 PM, olcott wrote:
On 5/1/2022 3:51 PM, André G. Isaak wrote:
On 2022-05-01 14:42, olcott wrote:
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:
On 2022-05-01 13:48, olcott wrote:
On 5/1/2022 2:44 PM, André G. Isaak wrote:
On 2022-05-01 13:32, olcott wrote:14 Every epistemological antinomy can likewise be used for a >>>>>>>>>>> similar
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:And how can you possibly justify your claim that Gödel's G >>>>>>>>>>>>>> is not a truth bearer?
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) >>>>>>>>>>>>>>
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.
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.
undecidability proof
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.
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
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.
André
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?
I backed André into a corner and forced him to quit lying
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?
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.
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.
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.
On 5/1/2022 8:32 PM, Richard Damon wrote:
On 5/1/22 8:58 PM, olcott wrote:
On 5/1/2022 6:18 PM, Richard Damon wrote:
On 5/1/22 6:39 PM, olcott wrote:
On 5/1/2022 5:08 PM, Richard Damon wrote:
On 5/1/22 6:04 PM, olcott wrote:sufficiently equivalent
On 5/1/2022 3:51 PM, André G. Isaak wrote:
On 2022-05-01 14:42, olcott wrote:
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:
On 2022-05-01 13:48, olcott wrote:
On 5/1/2022 2:44 PM, André G. Isaak wrote:
On 2022-05-01 13:32, olcott wrote:14 Every epistemological antinomy can likewise be used for >>>>>>>>>>>>> a similar
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.
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.
undecidability proof
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.
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
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.
André
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. >>>>>
You can PROVE it?
I backed André into a corner and forced him to quit lying
So, No. Note a trimming to change meaning, the original was:
sufficiently equivalent
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. >>>>
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 undecidabilityfor a
proofs. I have no idea what it is you hope to achieve by arguing
truism.
Nice out of context quoting, showing again you are the deciver.
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.
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.
On 5/1/22 10:18 PM, olcott wrote:
On 5/1/2022 9:14 PM, Richard Damon wrote:
On 5/1/22 9:53 PM, olcott wrote:
On 5/1/2022 8:32 PM, Richard Damon wrote:
On 5/1/22 8:58 PM, olcott wrote:
On 5/1/2022 6:18 PM, Richard Damon wrote:
On 5/1/22 6:39 PM, olcott wrote:
On 5/1/2022 5:08 PM, Richard Damon wrote:
On 5/1/22 6:04 PM, olcott wrote:
On 5/1/2022 3:51 PM, André G. Isaak wrote:
On 2022-05-01 14:42, olcott wrote:
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:
On 2022-05-01 13:48, olcott wrote:
On 5/1/2022 2:44 PM, André G. Isaak wrote:And again, you snipped all of the
On 2022-05-01 13:32, olcott wrote:undecidability proof
On 5/1/2022 2:22 PM, André G. Isaak wrote: >>>>>>>>>>>>>>>>>>> On 2022-05-01 13:00, olcott wrote: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. >>>>>>>>>>>>>>>> 14 Every epistemological antinomy can likewise be used >>>>>>>>>>>>>>>> for a similar
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. >>>>>>>>>>>>>>>>>
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. >>>>>>>>>>>>>>>
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
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.
André
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?
I backed André into a corner and forced him to quit lying
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 byarguing for a
truism.
Nice out of context quoting, showing again you are the deciver.
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.
If you make sure to knowingly contradict the verified facts then
Revelations 21:8 may eventually apply to you.
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.
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.
On 5/1/22 9:53 PM, olcott wrote:
On 5/1/2022 8:32 PM, Richard Damon wrote:
On 5/1/22 8:58 PM, olcott wrote:
On 5/1/2022 6:18 PM, Richard Damon wrote:
On 5/1/22 6:39 PM, olcott wrote:
On 5/1/2022 5:08 PM, Richard Damon wrote:
On 5/1/22 6:04 PM, olcott wrote:
On 5/1/2022 3:51 PM, André G. Isaak wrote:
On 2022-05-01 14:42, olcott wrote:
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:
On 2022-05-01 13:48, olcott wrote:
On 5/1/2022 2:44 PM, André G. Isaak wrote:And again, you snipped all of the
On 2022-05-01 13:32, olcott wrote:14 Every epistemological antinomy can likewise be used for >>>>>>>>>>>>>> a similar
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.
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.
undecidability proof
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. >>>>>>>>>>>>>
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
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.
André
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?
I backed André into a corner and forced him to quit lying
So, No. Note a trimming to change meaning, the original was:
sufficiently equivalent
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. >>>>>
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 undecidabilityfor a
proofs. I have no idea what it is you hope to achieve by arguing
truism.
Nice out of context quoting, showing again you are the deciver.
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.
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.
On 5/1/2022 9:14 PM, Richard Damon wrote:
On 5/1/22 9:53 PM, olcott wrote:
On 5/1/2022 8:32 PM, Richard Damon wrote:
On 5/1/22 8:58 PM, olcott wrote:
On 5/1/2022 6:18 PM, Richard Damon wrote:
On 5/1/22 6:39 PM, olcott wrote:
On 5/1/2022 5:08 PM, Richard Damon wrote:
On 5/1/22 6:04 PM, olcott wrote:
On 5/1/2022 3:51 PM, André G. Isaak wrote:
On 2022-05-01 14:42, olcott wrote:
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:
On 2022-05-01 13:48, olcott wrote:
On 5/1/2022 2:44 PM, André G. Isaak wrote:And again, you snipped all of the
On 2022-05-01 13:32, olcott wrote:14 Every epistemological antinomy can likewise be used >>>>>>>>>>>>>>> for a similar
On 5/1/2022 2:22 PM, André G. Isaak wrote: >>>>>>>>>>>>>>>>>> On 2022-05-01 13:00, olcott wrote: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.
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. >>>>>>>>>>>>>>>>
undecidability proof
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. >>>>>>>>>>>>>>
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
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.
André
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?
I backed André into a corner and forced him to quit lying
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.
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.
If you make sure to knowingly contradict the verified facts then
Revelations 21:8 may eventually apply to you.
The only one being dishonest here is you as you keep snipping the substance of my post.it is The Liar which is under discussion).
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
There are two crucial differences between G and The Liar:that post. Unless you actually have some comment on that explanation, there's no point repeating yourself.
(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
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.
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.
On 5/1/2022 9:47 PM, Richard Damon wrote:
On 5/1/22 10:18 PM, olcott wrote:
On 5/1/2022 9:14 PM, Richard Damon wrote:
On 5/1/22 9:53 PM, olcott wrote:
On 5/1/2022 8:32 PM, Richard Damon wrote:
On 5/1/22 8:58 PM, olcott wrote:
On 5/1/2022 6:18 PM, Richard Damon wrote:
On 5/1/22 6:39 PM, olcott wrote:
On 5/1/2022 5:08 PM, Richard Damon wrote:
On 5/1/22 6:04 PM, olcott wrote:
On 5/1/2022 3:51 PM, André G. Isaak wrote:
On 2022-05-01 14:42, olcott wrote:
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:
On 2022-05-01 13:48, olcott wrote:
On 5/1/2022 2:44 PM, André G. Isaak wrote: >>>>>>>>>>>>>>>>>> On 2022-05-01 13:32, olcott wrote:And again, you snipped all of the
undecidability proofOn 5/1/2022 2:22 PM, André G. Isaak wrote: >>>>>>>>>>>>>>>>>>>> On 2022-05-01 13:00, olcott wrote: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. >>>>>>>>>>>>>>>>> 14 Every epistemological antinomy can likewise be used >>>>>>>>>>>>>>>>> for a similar
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. >>>>>>>>>>>>>>>>>>
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. >>>>>>>>>>>>>>>>
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
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.
André
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?
I backed André into a corner and forced him to quit lying
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 byarguing for a
truism.
Nice out of context quoting, showing again you are the deciver.
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.
If you make sure to knowingly contradict the verified facts then
Revelations 21:8 may eventually apply to you.
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 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.
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 \+.
LP := ~True(LP) is translated to Prolog:None (!) of the predicates where executed in both unifications (with and without occurs check).
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false
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:None (!) of the predicates where executed in both unifications (with and without occurs check).
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false
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
On 5/1/22 11:04 PM, olcott wrote:
On 5/1/2022 9:47 PM, Richard Damon wrote:
On 5/1/22 10:18 PM, olcott wrote:
On 5/1/2022 9:14 PM, Richard Damon wrote:
On 5/1/22 9:53 PM, olcott wrote:
On 5/1/2022 8:32 PM, Richard Damon wrote:
On 5/1/22 8:58 PM, olcott wrote:
On 5/1/2022 6:18 PM, Richard Damon wrote:
On 5/1/22 6:39 PM, olcott wrote:
On 5/1/2022 5:08 PM, Richard Damon wrote:
On 5/1/22 6:04 PM, olcott wrote:
On 5/1/2022 3:51 PM, André G. Isaak wrote:
On 2022-05-01 14:42, olcott wrote:
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:
On 2022-05-01 13:48, olcott wrote:
On 5/1/2022 2:44 PM, André G. Isaak wrote: >>>>>>>>>>>>>>>>>>> On 2022-05-01 13:32, olcott wrote:And again, you snipped all of the
undecidability proofOn 5/1/2022 2:22 PM, André G. Isaak wrote: >>>>>>>>>>>>>>>>>>>>> On 2022-05-01 13:00, olcott wrote: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. >>>>>>>>>>>>>>>>>> 14 Every epistemological antinomy can likewise be used >>>>>>>>>>>>>>>>>> for a similar
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. >>>>>>>>>>>>>>>>>>>
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. >>>>>>>>>>>>>>>>>
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
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.
André
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?
I backed André into a corner and forced him to quit lying
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 similarundecidability
proofs. I have no idea what it is you hope to achieve byarguing for a
truism.
Nice out of context quoting, showing again you are the deciver.
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.
If you make sure to knowingly contradict the verified facts then
Revelations 21:8 may eventually apply to you.
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 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?
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.
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.
Here is what I understand of the relationship between logic and Prolog. Prolog corrects all of the errors of classical and symbolic logic byProlog by itself is a very bad theorem prover and it is very limited
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
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.
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 ?
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.
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).
On 5/2/2022 9:28 AM, Aleksy Grabowski wrote:
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.
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?
On 5/2/22 17:24, olcott wrote:
On 5/2/2022 9:28 AM, Aleksy Grabowski wrote:
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.
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?
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.
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?
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.
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(...))))))))))))
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.
On Mon, 2 May 2022 11:28:23 -0600
Jeff Barnett <jbb@notatt.com> wrote:
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.
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
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.
On 5/2/2022 12:28 PM, Jeff Barnett wrote:
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.
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.
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.
On 5/2/2022 6:10 AM, Richard Damon wrote:
On 5/1/22 11:04 PM, olcott wrote:
On 5/1/2022 9:47 PM, Richard Damon wrote:
On 5/1/22 10:18 PM, olcott wrote:
On 5/1/2022 9:14 PM, Richard Damon wrote:
On 5/1/22 9:53 PM, olcott wrote:
On 5/1/2022 8:32 PM, Richard Damon wrote:
On 5/1/22 8:58 PM, olcott wrote:If you look at the full context of many messages you will see
On 5/1/2022 6:18 PM, Richard Damon wrote:
On 5/1/22 6:39 PM, olcott wrote:
On 5/1/2022 5:08 PM, Richard Damon wrote:
On 5/1/22 6:04 PM, olcott wrote:
On 5/1/2022 3:51 PM, André G. Isaak wrote:
On 2022-05-01 14:42, olcott wrote:
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: >>>>>>>>>>>>>>>>>> On 2022-05-01 13:48, olcott wrote:
On 5/1/2022 2:44 PM, André G. Isaak wrote: >>>>>>>>>>>>>>>>>>>> On 2022-05-01 13:32, olcott wrote:And again, you snipped all of the
14 Every epistemological antinomy can likewise be >>>>>>>>>>>>>>>>>>> used for a similarOn 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: >>>>>>>>>>>>>>>>>>>>>>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.
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. >>>>>>>>>>>>>>>>>>>>
undecidability proof
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. >>>>>>>>>>>>>>>>>>
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
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.
André
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?
I backed André into a corner and forced him to quit lying
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 similarundecidability
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. >>>>>>>
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.
If you make sure to knowingly contradict the verified facts then
Revelations 21:8 may eventually apply to you.
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 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?
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.
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.
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.
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.
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.
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.
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. 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.
Aleksy Grabowski <hurufu@gmail.com> writes:
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.
And indeed there is a fully formalised proof of GIT in Coq (though I
think it's the slightly tighter Gödel-Rosser version).
On 5/2/2022 6:43 PM, Ben wrote:
Aleksy Grabowski <hurufu@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.
olcott <polcott2@gmail.com> writes:
On 5/2/2022 6:43 PM, Ben wrote:
Aleksy Grabowski <hurufu@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.
On 5/2/2022 9:21 PM, Ben wrote:
olcott <polcott2@gmail.com> writes:
On 5/2/2022 6:43 PM, Ben wrote:
Aleksy Grabowski <hurufu@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.
It is OK that you are not a math guy.
If you were a math guy you would understand that if G is provable then
that makes Gödel totally wrong. G is not Gödel's theorem, it is a key element of his theorem.
Incomplete T means that there exists a φ such that φ is not provable or refutable in formal system T.
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
On 5/2/2022 9:21 PM, Ben wrote:
olcott <polcott2@gmail.com> writes:
On 5/2/2022 6:43 PM, Ben wrote:G is provable. Proofs abound. I was pointing out one in a proper proof
Aleksy Grabowski <hurufu@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.
assistant, Coq.
It is OK that you are not a math guy.
If you were a math guy you would understand that if G is provable then
that makes Gödel totally wrong. G is not Gödel's theorem, it is a key element of his theorem.
On 5/2/2022 6:43 PM, Ben wrote:
Aleksy Grabowski <hurufu@gmail.com> writes:
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.
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 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.
On 2022-05-02 18:57, olcott wrote:
On 5/2/2022 6:43 PM, Ben wrote:
Aleksy Grabowski <hurufu@gmail.com> writes:
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.
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 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.
No.
The Liar can be used to construct an *identical* proof.
Other
antinomies could be used for similar proofs. He's already talking about
The Liar.
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.
You have some serious reading comprehension problems. I never denied the things Gödel wrote. I denied your conclusion because it does not follow.
Gödel starts by claiming there is a close relationship (*not*
equivalence) between one particular antinomy, The Liar, and his G.
He then states that similar proofs could be constructed using any antinomy.
That entails that other antinomies could be used to construct similar
proofs involving a similar close relation (again, *not* equivalence).
Gödel never claims *any* antinomy is equivalent to his G. Merely that a close relationship holds.
And all my comments concerned exactly what that relationship is.
André
On 5/3/2022 10:18 AM, André G. Isaak wrote:
On 2022-05-02 18:57, olcott wrote:
On 5/2/2022 6:43 PM, Ben wrote:
Aleksy Grabowski <hurufu@gmail.com> writes:
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.
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 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.
No. The Liar can be used to construct an *identical* proof.
Really?
Other antinomies could be used for similar proofs. He's already
talking about The Liar.
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.
You have some serious reading comprehension problems. I never denied
the things Gödel wrote. I denied your conclusion because it does not
follow.
Gödel starts by claiming there is a close relationship (*not*
equivalence) between one particular antinomy, The Liar, and his G.
He then states that similar proofs could be constructed using any
antinomy.
That entails that other antinomies could be used to construct similar
proofs involving a similar close relation (again, *not* equivalence).
That you persisted (six times) on claiming that Gödel's statement about
the Liar Paradox overrode and superseded his statement about the entire category that the Liar Paradox belongs to was despicably deceitful,
unless you believe that "close relationship" is stronger than "similar undecidability proof". In that case you never lied about this. I really
only want an honest dialogue so I am happy to admit my mistakes.
Gödel never claims *any* antinomy is equivalent to his G. Merely that
a close relationship holds.
I take "similar undecidability proof" to mean isomorphic.
https://en.wikipedia.org/wiki/Isomorphism
Without carefully studying the philosophical underpinnings of the
concept if incompleteness:
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
Incomplete T means that there exists a φ such that φ is not provable or refutable in formal system T.
The above is the precise measure of isomorphism. Anything meeting the
above specification is isomorphic to Gödel's G.
One might not feel comfortable that isomorphic is what Gödel by "similar undecidability proof". When we examine the above definition of
Incompleteness applied to the entire set of epistemological antinomies,
then we realize that all of them are making the category mistake (thanks Flibble) of presuming that φ is a logic sentence / truth bearer.
On 2022-05-03 10:08, olcott wrote:
On 5/3/2022 10:18 AM, André G. Isaak wrote:
On 2022-05-02 18:57, olcott wrote:
On 5/2/2022 6:43 PM, Ben wrote:
Aleksy Grabowski <hurufu@gmail.com> writes:
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.
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 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.
No. The Liar can be used to construct an *identical* proof.
Really?
Of course really.
His original proof drew on The Liar for inspiration. So a proof which
draws on The Liar would be the same proof.
He is saying that he could have used ANY antinomy.
IOW, he could have chosen a *different* antinomy from The Liar, call it Antinomy X, and constructed a *similar* proof around that. It would not
be the same proof, but it would involve constructing some sentence
G-Prime which held the same relation to Antinomy X as G hold to The Liar.
But there would not be an equivalence between G-Prime and X anymore than there is an equivalence between G and The Liar.
This is the point I keep trying to drive home. There is NO EQUIVALENCE between G and the The Liar. Only a close relationship.
Other antinomies could be used for similar proofs. He's already
talking about The Liar.
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.
You have some serious reading comprehension problems. I never denied
the things Gödel wrote. I denied your conclusion because it does not
follow.
Gödel starts by claiming there is a close relationship (*not*
equivalence) between one particular antinomy, The Liar, and his G.
He then states that similar proofs could be constructed using any
antinomy.
That entails that other antinomies could be used to construct similar
proofs involving a similar close relation (again, *not* equivalence).
That you persisted (six times) on claiming that Gödel's statement
about the Liar Paradox overrode and superseded his statement about the
entire category that the Liar Paradox belongs to was despicably
deceitful,
Except I made no such claim. Not even once. You persisted (six times) in misreading my claim.
unless you believe that "close relationship" is stronger than "similar
undecidability proof". In that case you never lied about this. I
really only want an honest dialogue so I am happy to admit my mistakes.
Gödel never claims *any* antinomy is equivalent to his G. Merely that
a close relationship holds.
I take "similar undecidability proof" to mean isomorphic.
Fine. That would mean the proof involving the Liar and G would be
isomorphic to the proof involving antinomy X and G-Prime.
That does *NOT* get you to the claim you were making which was that G in
some sense equivalent to The Liar. It is not.
And your claim that G is not a truth bearer rests on your false claim
that G and The Liar are somehow equivalent (though you refuse to say
with respect to what).
G is very clearly a truth-bearer. Go back and
reread my original explanation.
https://en.wikipedia.org/wiki/Isomorphism
Without carefully studying the philosophical underpinnings of the
concept if incompleteness:
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
Incomplete T means that there exists a φ such that φ is not provable
or refutable in formal system T.
The above is the precise measure of isomorphism. Anything meeting the
above specification is isomorphic to Gödel's G.
One might not feel comfortable that isomorphic is what Gödel by
"similar undecidability proof". When we examine the above definition
of Incompleteness applied to the entire set of epistemological
antinomies, then we realize that all of them are making the category
mistake (thanks Flibble) of presuming that φ is a logic sentence /
truth bearer.
Gödel's G is most definitely a truth bearer. It asserts that a specific polynomial equation has an integer solution. That claim must either be
true or false.
André
On 2022-05-03 11:05, olcott wrote:
On 5/3/2022 11:52 AM, André G. Isaak wrote:
On 2022-05-03 10:08, olcott wrote:
On 5/3/2022 10:18 AM, André G. Isaak wrote:
On 2022-05-02 18:57, olcott wrote:
On 5/2/2022 6:43 PM, Ben wrote:
Aleksy Grabowski <hurufu@gmail.com> writes:
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.
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 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.
No. The Liar can be used to construct an *identical* proof.
Really?
Of course really.
His original proof drew on The Liar for inspiration. So a proof which
draws on The Liar would be the same proof.
He is saying that he could have used ANY antinomy.
IOW, he could have chosen a *different* antinomy from The Liar, call
it Antinomy X, and constructed a *similar* proof around that. It
would not be the same proof, but it would involve constructing some
sentence G-Prime which held the same relation to Antinomy X as G hold
to The Liar.
But there would not be an equivalence between G-Prime and X anymore
than there is an equivalence between G and The Liar.
This is the point I keep trying to drive home. There is NO
EQUIVALENCE between G and the The Liar. Only a close relationship.
Other antinomies could be used for similar proofs. He's already
talking about The Liar.
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.
You have some serious reading comprehension problems. I never
denied the things Gödel wrote. I denied your conclusion because it
does not follow.
Gödel starts by claiming there is a close relationship (*not*
equivalence) between one particular antinomy, The Liar, and his G.
He then states that similar proofs could be constructed using any
antinomy.
That entails that other antinomies could be used to construct
similar proofs involving a similar close relation (again, *not*
equivalence).
That you persisted (six times) on claiming that Gödel's statement
about the Liar Paradox overrode and superseded his statement about
the entire category that the Liar Paradox belongs to was despicably
deceitful,
Except I made no such claim. Not even once. You persisted (six times)
in misreading my claim.
unless you believe that "close relationship" is stronger than
"similar undecidability proof". In that case you never lied about
this. I really only want an honest dialogue so I am happy to admit
my mistakes.
Gödel never claims *any* antinomy is equivalent to his G. Merely
that a close relationship holds.
I take "similar undecidability proof" to mean isomorphic.
Fine. That would mean the proof involving the Liar and G would be
isomorphic to the proof involving antinomy X and G-Prime.
I have no idea what you mean by G-Prime.
It is defined directly above. Trying reading more carefully.
That does *NOT* get you to the claim you were making which was that G
in some sense equivalent to The Liar. It is not.
And your claim that G is not a truth bearer rests on your false claim
that G and The Liar are somehow equivalent (though you refuse to say
with respect to what).
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
It is the fact that the mathematical definition of Incompleteness
simply assumes that φ is semantically correct that is the core mistake
of the mathematical definition of Incompleteness.
G is very clearly a truth-bearer. Go back and reread my original
explanation.
When G is not provable in PA, how is it shown to be true?
If it is not shown to be true in PA then we have the strawman error.
Here you're simply begging the question by assuming your own conclusion:
that being true and being provable are the same.
The whole point of
Gödel's proof is that they cannot be the same (at least not for
non-trivial systems).
The question is not whether it is true but whether it is a truth *bearer*.
You make the claim that The Liar is not a truth bearer (a plausible
claim depending on one's definitions).
You then jump to the conclusion that G is not a truth bearer based on
your assertion that it is "equivalent" to The Liar. But it is *NOT* equivalent. It merely bears a close relationship. But you refuse to
actually consider what the nature of that relationship; there are both similiarites and differences.
Whereas the Liar has no content other than to assert its own falsity, Gödel's G has definite content. It does not assert its own
unprovability, it asserts a very specific mathematical claim, one which
must by its nature be either true or false. Therefore G *is* a truth
bearer.
The formulation that G asserts its own unprovability is the Cliff-Notes version of the proof. It's not the substance of the actual proof.
André
On 5/3/2022 11:52 AM, André G. Isaak wrote:
On 2022-05-03 10:08, olcott wrote:
On 5/3/2022 10:18 AM, André G. Isaak wrote:
On 2022-05-02 18:57, olcott wrote:
On 5/2/2022 6:43 PM, Ben wrote:
Aleksy Grabowski <hurufu@gmail.com> writes:
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.
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 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.
No. The Liar can be used to construct an *identical* proof.
Really?
Of course really.
His original proof drew on The Liar for inspiration. So a proof which
draws on The Liar would be the same proof.
He is saying that he could have used ANY antinomy.
IOW, he could have chosen a *different* antinomy from The Liar, call
it Antinomy X, and constructed a *similar* proof around that. It would
not be the same proof, but it would involve constructing some sentence
G-Prime which held the same relation to Antinomy X as G hold to The Liar.
But there would not be an equivalence between G-Prime and X anymore
than there is an equivalence between G and The Liar.
This is the point I keep trying to drive home. There is NO EQUIVALENCE
between G and the The Liar. Only a close relationship.
Other antinomies could be used for similar proofs. He's already
talking about The Liar.
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.
You have some serious reading comprehension problems. I never denied
the things Gödel wrote. I denied your conclusion because it does not
follow.
Gödel starts by claiming there is a close relationship (*not*
equivalence) between one particular antinomy, The Liar, and his G.
He then states that similar proofs could be constructed using any
antinomy.
That entails that other antinomies could be used to construct
similar proofs involving a similar close relation (again, *not*
equivalence).
That you persisted (six times) on claiming that Gödel's statement
about the Liar Paradox overrode and superseded his statement about
the entire category that the Liar Paradox belongs to was despicably
deceitful,
Except I made no such claim. Not even once. You persisted (six times)
in misreading my claim.
unless you believe that "close relationship" is stronger than
"similar undecidability proof". In that case you never lied about
this. I really only want an honest dialogue so I am happy to admit my
mistakes.
Gödel never claims *any* antinomy is equivalent to his G. Merely
that a close relationship holds.
I take "similar undecidability proof" to mean isomorphic.
Fine. That would mean the proof involving the Liar and G would be
isomorphic to the proof involving antinomy X and G-Prime.
I have no idea what you mean by G-Prime.
That does *NOT* get you to the claim you were making which was that G
in some sense equivalent to The Liar. It is not.
And your claim that G is not a truth bearer rests on your false claim
that G and The Liar are somehow equivalent (though you refuse to say
with respect to what).
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
It is the fact that the mathematical definition of Incompleteness simply assumes that φ is semantically correct that is the core mistake of the mathematical definition of Incompleteness.
G is very clearly a truth-bearer. Go back and reread my original
explanation.
When G is not provable in PA, how is it shown to be true?
If it is not shown to be true in PA then we have the strawman error.
On 5/3/2022 12:17 PM, André G. Isaak wrote:
On 2022-05-03 11:05, olcott wrote:
On 5/3/2022 11:52 AM, André G. Isaak wrote:
G is very clearly a truth-bearer. Go back and reread my original
explanation.
When G is not provable in PA, how is it shown to be true?
If it is not shown to be true in PA then we have the strawman error.
Here you're simply begging the question by assuming your own
conclusion: that being true and being provable are the same.
This is not any mere assumption.
The only way that any analytic expressions of language are correctly determined to be true is:
(a) They are defined to be true.
(b) They are derived from applying truth preserving operations to (a) or
(b). Prolog knows this on the basis of its facts and rules. Facts are
(a) and rules are (b). This is also known as sound deductive inference.
The whole point of Gödel's proof is that they cannot be the same (at
least not for non-trivial systems).
When G is not provable in PA, how is it shown to be true (wild guess)?
What is the precise basis for assessing that G is true? please provide
ALL the steps.
The question is not whether it is true but whether it is a truth
*bearer*.
You make the claim that The Liar is not a truth bearer (a plausible
claim depending on one's definitions).
You then jump to the conclusion that G is not a truth bearer based on
your assertion that it is "equivalent" to The Liar. But it is *NOT*
equivalent. It merely bears a close relationship. But you refuse to
actually consider what the nature of that relationship; there are both
similiarites and differences.
Precise equivalence is defined by this:
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
The Liar Paradox can be neither proven nor refuted where T is the entire
body of analytic knowledge and φ is LP.
Whereas the Liar has no content other than to assert its own falsity,
Gödel's G has definite content. It does not assert its own
unprovability, it asserts a very specific mathematical claim, one
which must by its nature be either true or false. Therefore G *is* a
truth bearer.
The formulation that G asserts its own unprovability is the
Cliff-Notes version of the proof. It's not the substance of the actual
proof.
André
It is isomorphic to the substance of the actual proof.
Gödel says:
since the undecidable proposition [R(q); q] states precisely that q
belongs to K, i.e. according to (1), that [R(q); q] is not provable. We
are therefore confronted with a proposition which asserts its own unprovability.
On 2022-05-03 11:33, olcott wrote:
On 5/3/2022 12:17 PM, André G. Isaak wrote:
On 2022-05-03 11:05, olcott wrote:
On 5/3/2022 11:52 AM, André G. Isaak wrote:
<snippage>
G is very clearly a truth-bearer. Go back and reread my original
explanation.
When G is not provable in PA, how is it shown to be true?
If it is not shown to be true in PA then we have the strawman error.
Here you're simply begging the question by assuming your own
conclusion: that being true and being provable are the same.
This is not any mere assumption.
The only way that any analytic expressions of language are correctly
determined to be true is:
'True' and 'Correctly determined to be true' mean different things.
(a) They are defined to be true.
(b) They are derived from applying truth preserving operations to (a)
or (b). Prolog knows this on the basis of its facts and rules. Facts
are (a) and rules are (b). This is also known as sound deductive
inference.
These are YOUR assumptions. They have not been demonstrated. And they
are not consistent with the way in which the rest of the world talks
about truth. You are talking about provability, not truth.
The whole point of Gödel's proof is that they cannot be the same (at
least not for non-trivial systems).
When G is not provable in PA, how is it shown to be true (wild guess)?
What is the precise basis for assessing that G is true? please provide
ALL the steps.
"True" and "Known to be true" are entirely different things.
Consider the equation Srt((2748 + 87)^3) = 150,948.776 (to 3 decimal
places)
That equation is true but it is unlikely anyone knew this to be true
until now since I very much doubt anyone had previously considered that specific equation. That's doesn't mean it wasn't true all along. Just
that no one knew it was true.
There are all sorts of cases where we know one thing without knowing all things. I can know with certainty that (A ∨ B) is true meaning that I
know that *at least* one of A or B must be true while still not knowing
the truth value of either. These sorts of things occur all the time.
And not being provable in PA and not being provable are also two
different things.
The question is not whether it is true but whether it is a truth
*bearer*.
You make the claim that The Liar is not a truth bearer (a plausible
claim depending on one's definitions).
You then jump to the conclusion that G is not a truth bearer based on
your assertion that it is "equivalent" to The Liar. But it is *NOT*
equivalent. It merely bears a close relationship. But you refuse to
actually consider what the nature of that relationship; there are
both similiarites and differences.
Precise equivalence is defined by this:
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
The Liar Paradox can be neither proven nor refuted where T is the
entire body of analytic knowledge and φ is LP.
The Liar Paradox is a self-contradiction. The Gödel sentence is not.
Whereas the Liar has no content other than to assert its own falsity,
Gödel's G has definite content. It does not assert its own
unprovability, it asserts a very specific mathematical claim, one
which must by its nature be either true or false. Therefore G *is* a
truth bearer.
The formulation that G asserts its own unprovability is the
Cliff-Notes version of the proof. It's not the substance of the
actual proof.
André
It is isomorphic to the substance of the actual proof.
No. It is not. G asserts a claim about mathematics. It does not assert anything about itself. However, within the metalanguage we can prove
that G can only be true if it is not provable within the system under consideration.
Gödel says:
since the undecidable proposition [R(q); q] states precisely that q
belongs to K, i.e. according to (1), that [R(q); q] is not provable.
We are therefore confronted with a proposition which asserts its own
unprovability.
We are confronted *in our analysis* with such a situation. But there is
no proposition which directly asserts such a thing.
The problem is you refuse to look at the actual math and instead look
only at the text commentary which is merely a guide to, not the actual substance of, the proof.
André
On 5/3/2022 9:18 AM, André G. Isaak wrote:
On 2022-05-02 18:57, olcott wrote:
IDIOT SNIPPED
No. The Liar can be used to construct an *identical* proof. OtherI think that you have provided the troll a similar explanation over 100 times. I admire your tenacity but I must ask you a question: Why do you
antinomies could be used for similar proofs. He's already talking
about The Liar.
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.
You have some serious reading comprehension problems. I never denied
the things Gödel wrote. I denied your conclusion because it does not
follow.
Gödel starts by claiming there is a close relationship (*not*
equivalence) between one particular antinomy, The Liar, and his G.
He then states that similar proofs could be constructed using any
antinomy.
That entails that other antinomies could be used to construct similar
proofs involving a similar close relation (again, *not* equivalence).
Gödel never claims *any* antinomy is equivalent to his G. Merely that
a close relationship holds.
And all my comments concerned exactly what that relationship is.
think one more time will do either him or you any good? It's not like
this is an educational or soul-improving opportunity for either of you;
for you this must be frustrating no matter your intentions and for him
he is what he is and this is his only amusement. Whether troll or
buffoon, he's proud of his appearance as wasted space.
When T is the entire body of analytic knowledge and φ is the liar
paradox, the official mathematical definition of incompleteness
determines that the entire body of analytic knowledge is incomplete.
On 5/3/2022 1:23 PM, André G. Isaak wrote:
On 2022-05-03 11:33, olcott wrote:
On 5/3/2022 12:17 PM, André G. Isaak wrote:
On 2022-05-03 11:05, olcott wrote:
On 5/3/2022 11:52 AM, André G. Isaak wrote:
<snippage>
G is very clearly a truth-bearer. Go back and reread my original
explanation.
When G is not provable in PA, how is it shown to be true?
If it is not shown to be true in PA then we have the strawman error.
Here you're simply begging the question by assuming your own
conclusion: that being true and being provable are the same.
This is not any mere assumption.
The only way that any analytic expressions of language are correctly
determined to be true is:
'True' and 'Correctly determined to be true' mean different things.
Yes that seems to be correct.
On the other hand calling an expression of language true that has not be 'Correctly determined to be true' is an error.
If G is claimed to be true then this assertion must be supported by: 'Correctly determined to be true' otherwise the assessment of its truth
is no more than a wild guess.
(a) They are defined to be true.
(b) They are derived from applying truth preserving operations to (a)
or (b). Prolog knows this on the basis of its facts and rules. Facts
are (a) and rules are (b). This is also known as sound deductive
inference.
These are YOUR assumptions. They have not been demonstrated. And they
are not consistent with the way in which the rest of the world talks
about truth. You are talking about provability, not truth.
If G is claimed to be true then this assertion must be supported by: 'Correctly determined to be true' otherwise the assessment of its truth
is no more than a wild guess.
The whole point of Gödel's proof is that they cannot be the same (at
least not for non-trivial systems).
When G is not provable in PA, how is it shown to be true (wild guess)?
What is the precise basis for assessing that G is true? please
provide ALL the steps.
"True" and "Known to be true" are entirely different things.
Yes, however:
If G is claimed to be true then this assertion must be supported by: 'Correctly determined to be true' otherwise the assessment of its truth
is no more than a wild guess.
Consider the equation Srt((2748 + 87)^3) = 150,948.776 (to 3 decimal
places)
(2748 + 87)^3 = 22,785,532,875
What are you sorting with Srt()?
That equation is true but it is unlikely anyone knew this to be true
until now since I very much doubt anyone had previously considered
that specific equation. That's doesn't mean it wasn't true all along.
Just that no one knew it was true.
There are all sorts of cases where we know one thing without knowing
all things. I can know with certainty that (A ∨ B) is true meaning
that I know that *at least* one of A or B must be true while still not
knowing the truth value of either. These sorts of things occur all the
time.
That is not true. If A and B are syntactically correct expressions of a formal language yet neither one is semantically correct then we have the
same case as the Liar Paradox not being a truth bearer, thus (A ∨ B) is neither true nor false.
And not being provable in PA and not being provable are also two
different things.
I know that. Yet not being provable in PA also means that G cannot be
derived in PA by applying truth preserving operations to the axioms Z of
PA or other expressions Y derived from Z or Y.
If G is correctly determined to be true then there must be some process detailing the steps of how it is 'Correctly determined to be true'.
Lacking these steps one cannot correctly assert that G is true, only
that G might possibly be true.
The question is not whether it is true but whether it is a truth
*bearer*.
You make the claim that The Liar is not a truth bearer (a plausible
claim depending on one's definitions).
You then jump to the conclusion that G is not a truth bearer based
on your assertion that it is "equivalent" to The Liar. But it is
*NOT* equivalent. It merely bears a close relationship. But you
refuse to actually consider what the nature of that relationship;
there are both similiarites and differences.
Precise equivalence is defined by this:
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
The Liar Paradox can be neither proven nor refuted where T is the
entire body of analytic knowledge and φ is LP.
The Liar Paradox is a self-contradiction. The Gödel sentence is not.
Until you understand that G can only be correctly asserted to be true in
X if G is provable in X. G may be true in X without a proof in X, yet it cannot be correctly asserted to be true in X without such a proof.
Whereas the Liar has no content other than to assert its own
falsity, Gödel's G has definite content. It does not assert its own
unprovability, it asserts a very specific mathematical claim, one
which must by its nature be either true or false. Therefore G *is* a
truth bearer.
The formulation that G asserts its own unprovability is the
Cliff-Notes version of the proof. It's not the substance of the
actual proof.
André
It is isomorphic to the substance of the actual proof.
No. It is not. G asserts a claim about mathematics. It does not assert
anything about itself. However, within the metalanguage we can prove
that G can only be true if it is not provable within the system under
consideration.
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
When both G and the LP exactly meet the official mathematical definition
of incompleteness then G and LP are proven to be isomorphic.
Gödel says:
since the undecidable proposition [R(q); q] states precisely that q
belongs to K, i.e. according to (1), that [R(q); q] is not provable.
We are therefore confronted with a proposition which asserts its own
unprovability.
We are confronted *in our analysis* with such a situation. But there
is no proposition which directly asserts such a thing.
You are letting weasel words leak semantic meaning.
My analysis pertaining to the official mathematical definition of incompleteness cuts through these weasel words.
This proves that G the LP and the following sentence are all isomorphic: "This sentence is unprovable".
The problem is you refuse to look at the actual math and instead look
only at the text commentary which is merely a guide to, not the actual
substance of, the proof.
André
On 5/3/2022 1:12 PM, olcott wrote:
On 5/3/2022 1:33 PM, Jeff Barnett wrote:Polly want a cracker?
On 5/3/2022 9:18 AM, André G. Isaak wrote:
On 2022-05-02 18:57, olcott wrote:
IDIOT SNIPPED
No. The Liar can be used to construct an *identical* proof. OtherI think that you have provided the troll a similar explanation over
antinomies could be used for similar proofs. He's already talking
about The Liar.
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.
You have some serious reading comprehension problems. I never denied
the things Gödel wrote. I denied your conclusion because it does not
follow.
Gödel starts by claiming there is a close relationship (*not*
equivalence) between one particular antinomy, The Liar, and his G.
He then states that similar proofs could be constructed using any
antinomy.
That entails that other antinomies could be used to construct
similar proofs involving a similar close relation (again, *not*
equivalence).
Gödel never claims *any* antinomy is equivalent to his G. Merely
that a close relationship holds.
And all my comments concerned exactly what that relationship is.
100 times. I admire your tenacity but I must ask you a question: Why
do you think one more time will do either him or you any good? It's
not like this is an educational or soul-improving opportunity for
either of you; for you this must be frustrating no matter your
intentions and for him he is what he is and this is his only
amusement. Whether troll or buffoon, he's proud of his appearance as
wasted space.
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
I used the above as the precise measure of isomorphism.
The whole error of the incompleteness theorem is entirely anchored in
that the official mathematical definition of incompleteness
incorrectly presumes that syntactically correct expressions of the
language of formal system T are necessarily also semantically incorrect.
When T is the entire body of analytic knowledge and φ is the liar
paradox, the official mathematical definition of incompleteness
determines that the entire body of analytic knowledge is incomplete.
On 2022-05-03 13:12, olcott wrote:
When T is the entire body of analytic knowledge and φ is the liar
paradox, the official mathematical definition of incompleteness
determines that the entire body of analytic knowledge is incomplete.
G is not a formalization of The Liar. There is no such formalization in
the systems Gödel considers.
The Liar results in inconsistency whereas G results in incompleteness.
This is a major difference between G and The Liar which is why you need
to stop conflating the two. The Liar only exists in natural language,
not in mathematics.
André
On 5/3/2022 2:22 PM, André G. Isaak wrote:
On 2022-05-03 13:12, olcott wrote:
When T is the entire body of analytic knowledge and φ is the liar
paradox, the official mathematical definition of incompleteness
determines that the entire body of analytic knowledge is incomplete.
G is not a formalization of The Liar. There is no such formalization
in the systems Gödel considers.
The Liar results in inconsistency whereas G results in incompleteness.
Not according to the mathematical definition of incompleteness
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
Anything and everything that is neither provable nor refutable in some
formal system proves that this formal system IS INCOMPLETE as long as φ
is an expession of language of T.
This is a major difference between G and The Liar which is why you
need to stop conflating the two. The Liar only exists in natural
language,
That is not true, I think Tarski's way of formalizing the Liar Paradox
may be the best. He describes exactly how it would be formalized and
provides the exactly syntax for formalizing it. I will derive this and
post it sometime soon. I will keep working on this until I am sure that
I have it correctly.
not in mathematics.
André
On 5/3/22 10:53 PM, olcott wrote:
On 5/3/2022 2:22 PM, André G. Isaak wrote:
On 2022-05-03 13:12, olcott wrote:
When T is the entire body of analytic knowledge and φ is the liar
paradox, the official mathematical definition of incompleteness
determines that the entire body of analytic knowledge is incomplete.
G is not a formalization of The Liar. There is no such formalization
in the systems Gödel considers.
The Liar results in inconsistency whereas G results in incompleteness.
Not according to the mathematical definition of incompleteness
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
Anything and everything that is neither provable nor refutable in some
formal system proves that this formal system IS INCOMPLETE as long as
φ is an expession of language of T.
Your missing that he is meaning that if the Liar is TRUE, it shows the
logic system to be inconsistent.
While G being true just proves that the system is Incomplete.
(G not being False in a system shows that the system is Inconsistent, as
it says we can prove a false statement in the system)
This is a major difference between G and The Liar which is why you
need to stop conflating the two. The Liar only exists in natural
language,
That is not true, I think Tarski's way of formalizing the Liar Paradox
may be the best. He describes exactly how it would be formalized and
provides the exactly syntax for formalizing it. I will derive this and
post it sometime soon. I will keep working on this until I am sure
that I have it correctly.
not in mathematics.
André
On 2022-05-03 12:59, olcott wrote:
On 5/3/2022 1:23 PM, André G. Isaak wrote:
On 2022-05-03 11:33, olcott wrote:
On 5/3/2022 12:17 PM, André G. Isaak wrote:
On 2022-05-03 11:05, olcott wrote:
On 5/3/2022 11:52 AM, André G. Isaak wrote:
<snippage>
Here you're simply begging the question by assuming your ownG is very clearly a truth-bearer. Go back and reread my original >>>>>>> explanation.
When G is not provable in PA, how is it shown to be true?
If it is not shown to be true in PA then we have the strawman error. >>>>>
conclusion: that being true and being provable are the same.
This is not any mere assumption.
The only way that any analytic expressions of language are correctly
determined to be true is:
'True' and 'Correctly determined to be true' mean different things.
Yes that seems to be correct.
On the other hand calling an expression of language true that has not
be 'Correctly determined to be true' is an error.
But calling it a "non-truth bearer" simply because it has not been
determined to be true would equally be an error.
And it can be shown (i.e. correctly determined) that G is true, just not within the system for which it was constructed.
If G is claimed to be true then this assertion must be supported by:
'Correctly determined to be true' otherwise the assessment of its
truth is no more than a wild guess.
(a) They are defined to be true.
(b) They are derived from applying truth preserving operations to
(a) or (b). Prolog knows this on the basis of its facts and rules.
Facts are (a) and rules are (b). This is also known as sound
deductive inference.
These are YOUR assumptions. They have not been demonstrated. And they
are not consistent with the way in which the rest of the world talks
about truth. You are talking about provability, not truth.
If G is claimed to be true then this assertion must be supported by:
'Correctly determined to be true' otherwise the assessment of its
truth is no more than a wild guess.
The whole point of Gödel's proof is that they cannot be the same
(at least not for non-trivial systems).
When G is not provable in PA, how is it shown to be true (wild guess)? >>>> What is the precise basis for assessing that G is true? please
provide ALL the steps.
"True" and "Known to be true" are entirely different things.
Yes, however:
If G is claimed to be true then this assertion must be supported by:
'Correctly determined to be true' otherwise the assessment of its
truth is no more than a wild guess.
As I said, it can be shown in a higher order system.
But even if it could not be, if we can show that G can only be true in
cases where it is not provable in T, then there are only two possible conclusions:
Either G is true and unprovable in T, in which case T is incomplete.
Or G is false and provable in T, in which case T is inconsistent.
Which is exactly what Gödel's theorem states: A system can be consistent
or it can be complete but it cannot be both. An incomplete system is
still useful. An inconsistent system is not. Ergo he phrases this as an consistent system must be incomplete [with the usual caveats about
meeting some minimum threshold of expressive power].
Consider the equation Srt((2748 + 87)^3) = 150,948.776 (to 3 decimal
places)
(2748 + 87)^3 = 22,785,532,875
What are you sorting with Srt()?
That was obviously a type. Sqrt().
That equation is true but it is unlikely anyone knew this to be true
until now since I very much doubt anyone had previously considered
that specific equation. That's doesn't mean it wasn't true all along.
Just that no one knew it was true.
There are all sorts of cases where we know one thing without knowing
all things. I can know with certainty that (A ∨ B) is true meaning
that I know that *at least* one of A or B must be true while still
not knowing the truth value of either. These sorts of things occur
all the time.
That is not true. If A and B are syntactically correct expressions of
a formal language yet neither one is semantically correct then we have
the same case as the Liar Paradox not being a truth bearer, thus (A ∨
B) is neither true nor false.
But your whole notion of 'semantically correct' is recognized by no one
but you and is antithetical to the entire notion of a formal system. And
what I describe above is a situation which *very* commonly arises in
proofs. They're called proofs by dilemma and take the form:
A → C
B → C
(A ∨ B)
Therefore C
We draw a conclusion from A or B without knowing the truth value of
either. This strategy, for example, was used by Euclid in his proof that
no largest prime exists.
If you declare A and B to be 'non-truth bearers' simply because you
don't know whether they are true or false, then this and many other
proofs completely fall apart.
And not being provable in PA and not being provable are also two
different things.
I know that. Yet not being provable in PA also means that G cannot be
derived in PA by applying truth preserving operations to the axioms Z
of PA or other expressions Y derived from Z or Y.
If G is correctly determined to be true then there must be some
process detailing the steps of how it is 'Correctly determined to be
true'.
Just not in PA.
Lacking these steps one cannot correctly assert that G is true, only
that G might possibly be true.
The question is not whether it is true but whether it is a truth
*bearer*.
You make the claim that The Liar is not a truth bearer (a plausible
claim depending on one's definitions).
You then jump to the conclusion that G is not a truth bearer based
on your assertion that it is "equivalent" to The Liar. But it is
*NOT* equivalent. It merely bears a close relationship. But you
refuse to actually consider what the nature of that relationship;
there are both similiarites and differences.
Precise equivalence is defined by this:
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
The Liar Paradox can be neither proven nor refuted where T is the
entire body of analytic knowledge and φ is LP.
The Liar Paradox is a self-contradiction. The Gödel sentence is not.
Until you understand that G can only be correctly asserted to be true
in X if G is provable in X. G may be true in X without a proof in X,
yet it cannot be correctly asserted to be true in X without such a proof.
This is your confusion, not mine. We can assert that G is not provable
and that ¬G is also not provable without asserting anything at all about whether G is true and still conclude that X is incomplete.
Whereas the Liar has no content other than to assert its own
falsity, Gödel's G has definite content. It does not assert its own >>>>> unprovability, it asserts a very specific mathematical claim, one
which must by its nature be either true or false. Therefore G *is*
a truth bearer.
The formulation that G asserts its own unprovability is the
Cliff-Notes version of the proof. It's not the substance of the
actual proof.
André
It is isomorphic to the substance of the actual proof.
No. It is not. G asserts a claim about mathematics. It does not
assert anything about itself. However, within the metalanguage we can
prove that G can only be true if it is not provable within the system
under consideration.
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
When both G and the LP exactly meet the official mathematical
definition of incompleteness then G and LP are proven to be isomorphic.
LP doesn't meet said definition. LP is a paradox of natural language.
There is no 'isomorphism' between G and LP. And if you claim there is,
you must state what that isomorphism actually is.
Gödel says:
since the undecidable proposition [R(q); q] states precisely that q
belongs to K, i.e. according to (1), that [R(q); q] is not provable.
We are therefore confronted with a proposition which asserts its own
unprovability.
We are confronted *in our analysis* with such a situation. But there
is no proposition which directly asserts such a thing.
You are letting weasel words leak semantic meaning.
What does 'leak semantic meaning' even mean?
André
My analysis pertaining to the official mathematical definition of
incompleteness cuts through these weasel words.
This proves that G the LP and the following sentence are all isomorphic:
"This sentence is unprovable".
The problem is you refuse to look at the actual math and instead look
only at the text commentary which is merely a guide to, not the
actual substance of, the proof.
André
On 5/3/22 10:53 PM, olcott wrote:
On 5/3/2022 2:22 PM, André G. Isaak wrote:
On 2022-05-03 13:12, olcott wrote:
When T is the entire body of analytic knowledge and φ is the liar
paradox, the official mathematical definition of incompleteness
determines that the entire body of analytic knowledge is incomplete.
G is not a formalization of The Liar. There is no such formalization
in the systems Gödel considers.
The Liar results in inconsistency whereas G results in incompleteness.
Not according to the mathematical definition of incompleteness
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
Anything and everything that is neither provable nor refutable in some
formal system proves that this formal system IS INCOMPLETE as long as
φ is an expession of language of T.
Your missing that he is meaning that if the Liar is TRUE, it shows the
logic system to be inconsistent.
On 5/3/2022 3:03 PM, André G. Isaak wrote:
On 2022-05-03 12:59, olcott wrote:
On 5/3/2022 1:23 PM, André G. Isaak wrote:
On 2022-05-03 11:33, olcott wrote:
On 5/3/2022 12:17 PM, André G. Isaak wrote:
On 2022-05-03 11:05, olcott wrote:
On 5/3/2022 11:52 AM, André G. Isaak wrote:
<snippage>
Here you're simply begging the question by assuming your ownG is very clearly a truth-bearer. Go back and reread my original >>>>>>>> explanation.
When G is not provable in PA, how is it shown to be true?
If it is not shown to be true in PA then we have the strawman error. >>>>>>
conclusion: that being true and being provable are the same.
This is not any mere assumption.
The only way that any analytic expressions of language are
correctly determined to be true is:
'True' and 'Correctly determined to be true' mean different things.
Yes that seems to be correct.
On the other hand calling an expression of language true that has not
be 'Correctly determined to be true' is an error.
But calling it a "non-truth bearer" simply because it has not been
determined to be true would equally be an error.
That if correct. If is is impossibly true or false then it is not a
truth bearer.
And it can be shown (i.e. correctly determined) that G is true, just
not within the system for which it was constructed.
unprovable in the system entails untrue in the system.
If G is claimed to be true then this assertion must be supported by:
'Correctly determined to be true' otherwise the assessment of its
truth is no more than a wild guess.
(a) They are defined to be true.
(b) They are derived from applying truth preserving operations to
(a) or (b). Prolog knows this on the basis of its facts and rules.
Facts are (a) and rules are (b). This is also known as sound
deductive inference.
These are YOUR assumptions. They have not been demonstrated. And
they are not consistent with the way in which the rest of the world
talks about truth. You are talking about provability, not truth.
If G is claimed to be true then this assertion must be supported by:
'Correctly determined to be true' otherwise the assessment of its
truth is no more than a wild guess.
The whole point of Gödel's proof is that they cannot be the same
(at least not for non-trivial systems).
When G is not provable in PA, how is it shown to be true (wild guess)? >>>>> What is the precise basis for assessing that G is true? please
provide ALL the steps.
"True" and "Known to be true" are entirely different things.
Yes, however:
If G is claimed to be true then this assertion must be supported by:
'Correctly determined to be true' otherwise the assessment of its
truth is no more than a wild guess.
As I said, it can be shown in a higher order system.
Sure, yet it is only true in this system which also makes it provable in
that system.
But even if it could not be, if we can show that G can only be true in
cases where it is not provable in T, then there are only two possible
conclusions:
It can't be true in T and unprovable in T.
Either G is true and unprovable in T, in which case T is incomplete.
Or G is false and provable in T, in which case T is inconsistent.
If G is provable in U then it is true in U.
If G is unprovable in T then it is untrue in T.
G is unprovable in T because it is semantically incorrect.
Which is exactly what Gödel's theorem states: A system can be
consistent or it can be complete but it cannot be both. An incomplete
system is still useful. An inconsistent system is not. Ergo he phrases
this as an consistent system must be incomplete [with the usual
caveats about meeting some minimum threshold of expressive power].
Consider the equation Srt((2748 + 87)^3) = 150,948.776 (to 3 decimal
places)
(2748 + 87)^3 = 22,785,532,875
What are you sorting with Srt()?
That was obviously a type. Sqrt().
That equation is true but it is unlikely anyone knew this to be true
until now since I very much doubt anyone had previously considered
that specific equation. That's doesn't mean it wasn't true all
along. Just that no one knew it was true.
There are all sorts of cases where we know one thing without knowing
all things. I can know with certainty that (A ∨ B) is true meaning
that I know that *at least* one of A or B must be true while still
not knowing the truth value of either. These sorts of things occur
all the time.
That is not true. If A and B are syntactically correct expressions of
a formal language yet neither one is semantically correct then we
have the same case as the Liar Paradox not being a truth bearer, thus
(A ∨ B) is neither true nor false.
But your whole notion of 'semantically correct' is recognized by no
one but you and is antithetical to the entire notion of a formal
system. And what I describe above is a situation which *very* commonly
arises in proofs. They're called proofs by dilemma and take the form:
A → C
B → C
(A ∨ B)
Therefore C
We draw a conclusion from A or B without knowing the truth value of
either. This strategy, for example, was used by Euclid in his proof
that no largest prime exists.
If you declare A and B to be 'non-truth bearers' simply because you
don't know whether they are true or false, then this and many other
proofs completely fall apart.
It is not because they have unknown truth values.
And not being provable in PA and not being provable are also two
different things.
I know that. Yet not being provable in PA also means that G cannot be
derived in PA by applying truth preserving operations to the axioms Z
of PA or other expressions Y derived from Z or Y.
If G is correctly determined to be true then there must be some
process detailing the steps of how it is 'Correctly determined to be
true'.
Just not in PA.
OK great this is great progress!
Lacking these steps one cannot correctly assert that G is true, only
that G might possibly be true.
The question is not whether it is true but whether it is a truth
*bearer*.
You make the claim that The Liar is not a truth bearer (a
plausible claim depending on one's definitions).
You then jump to the conclusion that G is not a truth bearer based >>>>>> on your assertion that it is "equivalent" to The Liar. But it is
*NOT* equivalent. It merely bears a close relationship. But you
refuse to actually consider what the nature of that relationship;
there are both similiarites and differences.
Precise equivalence is defined by this:
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
The Liar Paradox can be neither proven nor refuted where T is the
entire body of analytic knowledge and φ is LP.
The Liar Paradox is a self-contradiction. The Gödel sentence is not.
Until you understand that G can only be correctly asserted to be true
in X if G is provable in X. G may be true in X without a proof in X,
yet it cannot be correctly asserted to be true in X without such a
proof.
This is your confusion, not mine. We can assert that G is not provable
and that ¬G is also not provable without asserting anything at all
about whether G is true and still conclude that X is incomplete.
Yes, but, only because the mathematical definition of Incomplete does
not screen out semantically erroneous expression of the language of X: Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
Whereas the Liar has no content other than to assert its own
falsity, Gödel's G has definite content. It does not assert its
own unprovability, it asserts a very specific mathematical claim,
one which must by its nature be either true or false. Therefore G
*is* a truth bearer.
The formulation that G asserts its own unprovability is the
Cliff-Notes version of the proof. It's not the substance of the
actual proof.
André
It is isomorphic to the substance of the actual proof.
No. It is not. G asserts a claim about mathematics. It does not
assert anything about itself. However, within the metalanguage we
can prove that G can only be true if it is not provable within the
system under consideration.
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
When both G and the LP exactly meet the official mathematical
definition of incompleteness then G and LP are proven to be isomorphic.
LP doesn't meet said definition. LP is a paradox of natural language.
There is no 'isomorphism' between G and LP. And if you claim there is,
you must state what that isomorphism actually is.
It is a little iffy to say that the LP fits into the above formula
making it isomorphic to Gödel's G unless we can at least specify the
formal system that LP is a member of. Tarski seemed to have provided a
very clean basis to formalize the Liar Paradox. I am working on deriving
it.
Gödel says:
since the undecidable proposition [R(q); q] states precisely that q
belongs to K, i.e. according to (1), that [R(q); q] is not
provable. We are therefore confronted with a proposition which
asserts its own unprovability.
We are confronted *in our analysis* with such a situation. But there
is no proposition which directly asserts such a thing.
You have to pay attention to this
since the undecidable proposition [R(q); q] states precisely that q
belongs to K, i.e. according to (1), that [R(q); q] is not provable.
It is the English language version of a formal logic sentence.
You are letting weasel words leak semantic meaning.
What does 'leak semantic meaning' even mean?
You were simply looking at the wrong lines of the Gödel quote.
On 2022-05-03 21:12, Richard Damon wrote:
On 5/3/22 10:53 PM, olcott wrote:
On 5/3/2022 2:22 PM, André G. Isaak wrote:
On 2022-05-03 13:12, olcott wrote:
When T is the entire body of analytic knowledge and φ is the liar
paradox, the official mathematical definition of incompleteness
determines that the entire body of analytic knowledge is incomplete.
G is not a formalization of The Liar. There is no such formalization
in the systems Gödel considers.
The Liar results in inconsistency whereas G results in incompleteness.
Not according to the mathematical definition of incompleteness
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
Anything and everything that is neither provable nor refutable in
some formal system proves that this formal system IS INCOMPLETE as
long as φ is an expession of language of T.
Your missing that he is meaning that if the Liar is TRUE, it shows the
logic system to be inconsistent.
Actually, it doesn't matter whether it is true or false.
What's relevant here is that it is trivially easy to prove The Liar
using a simple reductio ad absurdum. Unfortunately, it is equally
trivially easy to prove ¬(The Liar) using a reductio of the same form.
That's very different from G, where no proof exists of either G or of ¬G.
The Liar leads to inconsistency.
The sentence 'This sentence is true' would be a natural language example which leads to incompleteness.
André
unprovable in the system entails untrue in the system.
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
The Liar Paradox plugs right in to this
On 2022-05-04 00:17, olcott wrote:
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
The Liar Paradox plugs right in to this
How exactly does it 'plug right into the above'? As I just said, LP *is* provable. ¬LP is also provable.
That's what it means to be a contradiction.
André
On 5/4/2022 9:02 AM, André G. Isaak wrote:
On 2022-05-04 00:17, olcott wrote:
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
The Liar Paradox plugs right in to this
How exactly does it 'plug right into the above'? As I just said, LP
*is* provable. ¬LP is also provable.
That's what it means to be a contradiction.
André
LP exactly meets the mathematical definition of incompleteness, this
will not be clear until after I correctly formalize it and specify the
formal system to which it belongs. Tarski seems to provide the best head start on formalizing the LP.
| Sysop: | Keyop |
|---|---|
| Location: | Huddersfield, West Yorkshire, UK |
| Users: | 297 |
| Nodes: | 16 (0 / 16) |
| Uptime: | 124:36:41 |
| Calls: | 6,662 |
| Files: | 12,212 |
| Messages: | 5,334,763 |