*This is how I overturn the Tarski Undefinability theorem*
An analytic expression of language is any expression of formal or
natural language that can be proven true or false entirely on the basis
of a connection to its semantic meaning in this same language.
This connection must be through a sequence of truth preserving
operations from expression x of language L to meaning M in L. A lack of
such connection from x or ~x in L is construed as x is not a truth
bearer in L.
Tarski's Liar Paradox from page 248
It would then be possible to reconstruct the antinomy of the liar
in the metalanguage, by forming in the language itself a sentence
x such that the sentence of the metalanguage which is correlated
with x asserts that x is not a true sentence.
https://liarparadox.org/Tarski_247_248.pdf
Formalized as:
x ∉ True if and only if p
where the symbol 'p' represents the whole sentence x https://liarparadox.org/Tarski_275_276.pdf
*Formalized as Prolog*
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
When formalized as Prolog unify_with_occurs_check()
detects a cycle in the directed graph of the evaluation
sequence proving the LP is not a truth bearer.
The purpose of this work was to show that algorithmic
undecidability is a misconception providing more details
than Wittgenstein's rebuttal of Gödel.
https://www.liarparadox.org/Wittgenstein.pdf
*This is how I overturn the Tarski Undefinability theorem*
An analytic expression of language is any expression of formal or
natural language that can be proven true or false entirely on the basis
of a connection to its semantic meaning in this same language.
This connection must be through a sequence of truth preserving
operations from expression x of language L to meaning M in L. A lack of
such connection from x or ~x in L is construed as x is not a truth
bearer in L.
Tarski's Liar Paradox from page 248
It would then be possible to reconstruct the antinomy of the liar
in the metalanguage, by forming in the language itself a sentence
x such that the sentence of the metalanguage which is correlated
with x asserts that x is not a true sentence.
https://liarparadox.org/Tarski_247_248.pdf
Formalized as:
x ∉ True if and only if p
where the symbol 'p' represents the whole sentence x https://liarparadox.org/Tarski_275_276.pdf
*Formalized as Prolog*
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
When formalized as Prolog unify_with_occurs_check()
detects a cycle in the directed graph of the evaluation
sequence proving the LP is not a truth bearer.
The purpose of this work was to show that algorithmic
undecidability is a misconception providing more details
than Wittgenstein's rebuttal of Gödel.
https://www.liarparadox.org/Wittgenstein.pdf
On 9/1/2024 7:52 AM, Mikko wrote:
On 2024-08-31 18:48:18 +0000, olcott said:
*This is how I overturn the Tarski Undefinability theorem*
An analytic expression of language is any expression of formal or
natural language that can be proven true or false entirely on the basis
of a connection to its semantic meaning in this same language.
This connection must be through a sequence of truth preserving
operations from expression x of language L to meaning M in L. A lack of
such connection from x or ~x in L is construed as x is not a truth
bearer in L.
Tarski's Liar Paradox from page 248
It would then be possible to reconstruct the antinomy of the liar >>> in the metalanguage, by forming in the language itself a sentence >>> x such that the sentence of the metalanguage which is correlated
with x asserts that x is not a true sentence.
https://liarparadox.org/Tarski_247_248.pdf
Formalized as:
x ∉ True if and only if p
where the symbol 'p' represents the whole sentence x
https://liarparadox.org/Tarski_275_276.pdf
*Formalized as Prolog*
?- LP = not(true(LP)).
LP = not(true(LP)).
According to Prolog semantics "false" would also be a correct
response.
?- unify_with_occurs_check(LP, not(true(LP))).
false.
To the extend Prolog formalizes anything, that only formalizes
the condept of self-reference. I does not say anything about
int.
When formalized as Prolog unify_with_occurs_check()
detects a cycle in the directed graph of the evaluation
sequence proving the LP is not a truth bearer.
Prolog does not say anything about truth-bearers.
It may seem that way if you have no idea what
(a) a directed is
(b) what cycles in a directed graph are
(c) What an evaluation sequence is
If you do know these things then Prolog proved that LP
has no truth-maker and thus cannot be a truth-bearer.
The purpose of this work was to show that algorithmic
undecidability is a misconception providing more details
than Wittgenstein's rebuttal of Gödel.
Which it didn't show.
I showed it to everyone knowing (a)(b)(c)
On 9/2/2024 2:54 AM, Mikko wrote:
On 2024-09-01 13:47:00 +0000, olcott said:
On 9/1/2024 7:52 AM, Mikko wrote:
On 2024-08-31 18:48:18 +0000, olcott said:
*This is how I overturn the Tarski Undefinability theorem*
An analytic expression of language is any expression of formal or
natural language that can be proven true or false entirely on the basis >>>>> of a connection to its semantic meaning in this same language.
This connection must be through a sequence of truth preserving
operations from expression x of language L to meaning M in L. A lack of >>>>> such connection from x or ~x in L is construed as x is not a truth
bearer in L.
Tarski's Liar Paradox from page 248
It would then be possible to reconstruct the antinomy of the liar >>>>> in the metalanguage, by forming in the language itself a sentence >>>>> x such that the sentence of the metalanguage which is correlated >>>>> with x asserts that x is not a true sentence.
https://liarparadox.org/Tarski_247_248.pdf
Formalized as:
x ∉ True if and only if p
where the symbol 'p' represents the whole sentence x
https://liarparadox.org/Tarski_275_276.pdf
*Formalized as Prolog*
?- LP = not(true(LP)).
LP = not(true(LP)).
According to Prolog semantics "false" would also be a correct
response.
?- unify_with_occurs_check(LP, not(true(LP))).
false.
To the extend Prolog formalizes anything, that only formalizes
the condept of self-reference. I does not say anything about
int.
When formalized as Prolog unify_with_occurs_check()
detects a cycle in the directed graph of the evaluation
sequence proving the LP is not a truth bearer.
Prolog does not say anything about truth-bearers.
It may seem that way if you have no idea what
(a) a directed is
(b) what cycles in a directed graph are
(c) What an evaluation sequence is
More relevanto would be what a "truth-maker" is.
Anyway, it seems that Prolog does not say anything about
truth-bearers because Prolog does not say anything about
truth-bearers.
When Prolog derives expression x from Facts and Rules
by applying the truth preserving operations of Rules to
Facts is the truthmaker for truth-bearer x.
On 9/3/2024 5:38 AM, Mikko wrote:
On 2024-09-02 13:01:23 +0000, olcott said:
On 9/2/2024 2:54 AM, Mikko wrote:
On 2024-09-01 13:47:00 +0000, olcott said:
On 9/1/2024 7:52 AM, Mikko wrote:
On 2024-08-31 18:48:18 +0000, olcott said:
*This is how I overturn the Tarski Undefinability theorem*
An analytic expression of language is any expression of formal or >>>>>>> natural language that can be proven true or false entirely on the >>>>>>> basis of a connection to its semantic meaning in this same language. >>>>>>>
This connection must be through a sequence of truth preserving
operations from expression x of language L to meaning M in L. A
lack of such connection from x or ~x in L is construed as x is
not a truth bearer in L.
Tarski's Liar Paradox from page 248
It would then be possible to reconstruct the antinomy of the >>>>>>> liar
in the metalanguage, by forming in the language itself a
sentence
x such that the sentence of the metalanguage which is correlated >>>>>>> with x asserts that x is not a true sentence.
https://liarparadox.org/Tarski_247_248.pdf
Formalized as:
x ∉ True if and only if p
where the symbol 'p' represents the whole sentence x
https://liarparadox.org/Tarski_275_276.pdf
*Formalized as Prolog*
?- LP = not(true(LP)).
LP = not(true(LP)).
According to Prolog semantics "false" would also be a correct
response.
?- unify_with_occurs_check(LP, not(true(LP))).
false.
To the extend Prolog formalizes anything, that only formalizes
the condept of self-reference. I does not say anything about
int.
When formalized as Prolog unify_with_occurs_check()
detects a cycle in the directed graph of the evaluation
sequence proving the LP is not a truth bearer.
Prolog does not say anything about truth-bearers.
It may seem that way if you have no idea what
(a) a directed is
(b) what cycles in a directed graph are
(c) What an evaluation sequence is
More relevanto would be what a "truth-maker" is.
Anyway, it seems that Prolog does not say anything about
truth-bearers because Prolog does not say anything about
truth-bearers.
When Prolog derives expression x from Facts and Rules
by applying the truth preserving operations of Rules to
Facts is the truthmaker for truth-bearer x.
A Prolog impementation applies Prolog operations.
Which are (like logic) for the most part truth preserving.
If (A & B) then A
For some cases
Prolog offers several operations letting the implementation to
choose which one to apply.
I don't thing so. Once the Facts and Rules are specified
Prolog chooses whatever Facts and Rules to prove x or not.
It is back-chained inference.
Consequently some goals may evaluate
to true in some implementations and false in others, for example
L = [L].
On 9/3/2024 5:38 AM, Mikko wrote:
On 2024-09-02 13:01:23 +0000, olcott said:
On 9/2/2024 2:54 AM, Mikko wrote:
On 2024-09-01 13:47:00 +0000, olcott said:
On 9/1/2024 7:52 AM, Mikko wrote:
On 2024-08-31 18:48:18 +0000, olcott said:
*This is how I overturn the Tarski Undefinability theorem*
An analytic expression of language is any expression of formal or >>>>>>> natural language that can be proven true or false entirely on the basis >>>>>>> of a connection to its semantic meaning in this same language.
This connection must be through a sequence of truth preserving
operations from expression x of language L to meaning M in L. A lack of >>>>>>> such connection from x or ~x in L is construed as x is not a truth >>>>>>> bearer in L.
Tarski's Liar Paradox from page 248
It would then be possible to reconstruct the antinomy of the liar
in the metalanguage, by forming in the language itself a sentence
x such that the sentence of the metalanguage which is correlated >>>>>>> with x asserts that x is not a true sentence.
https://liarparadox.org/Tarski_247_248.pdf
Formalized as:
x ∉ True if and only if p
where the symbol 'p' represents the whole sentence x
https://liarparadox.org/Tarski_275_276.pdf
*Formalized as Prolog*
?- LP = not(true(LP)).
LP = not(true(LP)).
According to Prolog semantics "false" would also be a correct
response.
?- unify_with_occurs_check(LP, not(true(LP))).
false.
To the extend Prolog formalizes anything, that only formalizes
the condept of self-reference. I does not say anything about
int.
When formalized as Prolog unify_with_occurs_check()
detects a cycle in the directed graph of the evaluation
sequence proving the LP is not a truth bearer.
Prolog does not say anything about truth-bearers.
It may seem that way if you have no idea what
(a) a directed is
(b) what cycles in a directed graph are
(c) What an evaluation sequence is
More relevanto would be what a "truth-maker" is.
Anyway, it seems that Prolog does not say anything about
truth-bearers because Prolog does not say anything about
truth-bearers.
When Prolog derives expression x from Facts and Rules
by applying the truth preserving operations of Rules to
Facts is the truthmaker for truth-bearer x.
A Prolog impementation applies Prolog operations.
Which are (like logic) for the most part truth preserving.
If (A & B) then A
For some cases
Prolog offers several operations letting the implementation to
choose which one to apply.
I don't thing so. Once the Facts and Rules are specified
Prolog chooses whatever Facts and Rules to prove x or not.
It is back-chained inference.
Consequently some goals may evaluate
to true in some implementations and false in others, for example
L = [L].
On 9/6/2024 6:55 AM, Mikko wrote:
On 2024-09-03 12:44:00 +0000, olcott said:
On 9/3/2024 5:38 AM, Mikko wrote:
On 2024-09-02 13:01:23 +0000, olcott said:
On 9/2/2024 2:54 AM, Mikko wrote:
On 2024-09-01 13:47:00 +0000, olcott said:
On 9/1/2024 7:52 AM, Mikko wrote:
On 2024-08-31 18:48:18 +0000, olcott said:
*This is how I overturn the Tarski Undefinability theorem*
An analytic expression of language is any expression of formal or >>>>>>>>> natural language that can be proven true or false entirely on the basis
of a connection to its semantic meaning in this same language. >>>>>>>>>
This connection must be through a sequence of truth preserving >>>>>>>>> operations from expression x of language L to meaning M in L. A lack of
such connection from x or ~x in L is construed as x is not a truth >>>>>>>>> bearer in L.
Tarski's Liar Paradox from page 248
It would then be possible to reconstruct the antinomy of the liar
in the metalanguage, by forming in the language itself a sentence
x such that the sentence of the metalanguage which is correlated
with x asserts that x is not a true sentence.
https://liarparadox.org/Tarski_247_248.pdf
Formalized as:
x ∉ True if and only if p
where the symbol 'p' represents the whole sentence x
https://liarparadox.org/Tarski_275_276.pdf
*Formalized as Prolog*
?- LP = not(true(LP)).
LP = not(true(LP)).
According to Prolog semantics "false" would also be a correct
response.
?- unify_with_occurs_check(LP, not(true(LP))).
false.
To the extend Prolog formalizes anything, that only formalizes >>>>>>>> the condept of self-reference. I does not say anything about
int.
When formalized as Prolog unify_with_occurs_check()
detects a cycle in the directed graph of the evaluation
sequence proving the LP is not a truth bearer.
Prolog does not say anything about truth-bearers.
It may seem that way if you have no idea what
(a) a directed is
(b) what cycles in a directed graph are
(c) What an evaluation sequence is
More relevanto would be what a "truth-maker" is.
Anyway, it seems that Prolog does not say anything about
truth-bearers because Prolog does not say anything about
truth-bearers.
When Prolog derives expression x from Facts and Rules
by applying the truth preserving operations of Rules to
Facts is the truthmaker for truth-bearer x.
A Prolog impementation applies Prolog operations.
Which are (like logic) for the most part truth preserving.
If (A & B) then A
Logic where the infoerence rules are for the most part truth prserving
is not useful. They all must be.
For some cases
Prolog offers several operations letting the implementation to
choose which one to apply.
I don't thing so. Once the Facts and Rules are specified
Prolog chooses whatever Facts and Rules to prove x or not.
It is back-chained inference.
Standard Prolog is what the Prolog standard says. Conforming implementations >> may vary if the standard allows. If you think otherwise you are wrong.
There are also non-starndard Prlongs that vary even more.
The fundamental architectural overview of all Prolog implementations
is the same True(x) means X is derived by applying Rules (AKA truth preserving operations) to Facts.
On 9/7/2024 3:35 AM, Mikko wrote:
On 2024-09-06 12:22:04 +0000, olcott said:
On 9/6/2024 6:55 AM, Mikko wrote:
On 2024-09-03 12:44:00 +0000, olcott said:
On 9/3/2024 5:38 AM, Mikko wrote:
On 2024-09-02 13:01:23 +0000, olcott said:
On 9/2/2024 2:54 AM, Mikko wrote:
On 2024-09-01 13:47:00 +0000, olcott said:
On 9/1/2024 7:52 AM, Mikko wrote:
On 2024-08-31 18:48:18 +0000, olcott said:
*This is how I overturn the Tarski Undefinability theorem* >>>>>>>>>>> An analytic expression of language is any expression of
formal or natural language that can be proven true or false >>>>>>>>>>> entirely on the basis of a connection to its semantic meaning >>>>>>>>>>> in this same language.
This connection must be through a sequence of truth
preserving operations from expression x of language L to >>>>>>>>>>> meaning M in L. A lack of such connection from x or ~x in L >>>>>>>>>>> is construed as x is not a truth bearer in L.
Tarski's Liar Paradox from page 248
It would then be possible to reconstruct the antinomy of >>>>>>>>>>> the liar
in the metalanguage, by forming in the language itself a >>>>>>>>>>> sentence
x such that the sentence of the metalanguage which is >>>>>>>>>>> correlated
with x asserts that x is not a true sentence.
https://liarparadox.org/Tarski_247_248.pdf
Formalized as:
x ∉ True if and only if p
where the symbol 'p' represents the whole sentence x
https://liarparadox.org/Tarski_275_276.pdf
*Formalized as Prolog*
?- LP = not(true(LP)).
LP = not(true(LP)).
According to Prolog semantics "false" would also be a correct >>>>>>>>>> response.
?- unify_with_occurs_check(LP, not(true(LP))).
false.
To the extend Prolog formalizes anything, that only formalizes >>>>>>>>>> the condept of self-reference. I does not say anything about >>>>>>>>>> int.
When formalized as Prolog unify_with_occurs_check()
detects a cycle in the directed graph of the evaluation
sequence proving the LP is not a truth bearer.
Prolog does not say anything about truth-bearers.
It may seem that way if you have no idea what
(a) a directed is
(b) what cycles in a directed graph are
(c) What an evaluation sequence is
More relevanto would be what a "truth-maker" is.
Anyway, it seems that Prolog does not say anything about
truth-bearers because Prolog does not say anything about
truth-bearers.
When Prolog derives expression x from Facts and Rules
by applying the truth preserving operations of Rules to
Facts is the truthmaker for truth-bearer x.
A Prolog impementation applies Prolog operations.
Which are (like logic) for the most part truth preserving.
If (A & B) then A
Logic where the infoerence rules are for the most part truth prserving >>>> is not useful. They all must be.
For some cases
Prolog offers several operations letting the implementation to
choose which one to apply.
I don't thing so. Once the Facts and Rules are specified
Prolog chooses whatever Facts and Rules to prove x or not.
It is back-chained inference.
Standard Prolog is what the Prolog standard says. Conforming
implementations
may vary if the standard allows. If you think otherwise you are wrong. >>>> There are also non-starndard Prlongs that vary even more.
The fundamental architectural overview of all Prolog implementations
is the same True(x) means X is derived by applying Rules (AKA truth
preserving operations) to Facts.
The details are permitted to differ.
Instead of using any single order of logic we simultaneously
represent an arbitrary number of orders of logic in a type
hierarchy knowledge ontology.
On 9/7/2024 3:35 AM, Mikko wrote:
On 2024-09-06 12:22:04 +0000, olcott said:
On 9/6/2024 6:55 AM, Mikko wrote:
On 2024-09-03 12:44:00 +0000, olcott said:
On 9/3/2024 5:38 AM, Mikko wrote:
On 2024-09-02 13:01:23 +0000, olcott said:
On 9/2/2024 2:54 AM, Mikko wrote:
On 2024-09-01 13:47:00 +0000, olcott said:
On 9/1/2024 7:52 AM, Mikko wrote:
On 2024-08-31 18:48:18 +0000, olcott said:
*This is how I overturn the Tarski Undefinability theorem* >>>>>>>>>>> An analytic expression of language is any expression of formal or >>>>>>>>>>> natural language that can be proven true or false entirely on the basis
of a connection to its semantic meaning in this same language. >>>>>>>>>>>
This connection must be through a sequence of truth preserving >>>>>>>>>>> operations from expression x of language L to meaning M in L. A lack of
such connection from x or ~x in L is construed as x is not a truth >>>>>>>>>>> bearer in L.
Tarski's Liar Paradox from page 248
It would then be possible to reconstruct the antinomy of the liar
in the metalanguage, by forming in the language itself a sentence
x such that the sentence of the metalanguage which is correlated
with x asserts that x is not a true sentence.
https://liarparadox.org/Tarski_247_248.pdf
Formalized as:
x ∉ True if and only if p
where the symbol 'p' represents the whole sentence x
https://liarparadox.org/Tarski_275_276.pdf
*Formalized as Prolog*
?- LP = not(true(LP)).
LP = not(true(LP)).
According to Prolog semantics "false" would also be a correct >>>>>>>>>> response.
?- unify_with_occurs_check(LP, not(true(LP))).
false.
To the extend Prolog formalizes anything, that only formalizes >>>>>>>>>> the condept of self-reference. I does not say anything about >>>>>>>>>> int.
When formalized as Prolog unify_with_occurs_check()
detects a cycle in the directed graph of the evaluation
sequence proving the LP is not a truth bearer.
Prolog does not say anything about truth-bearers.
It may seem that way if you have no idea what
(a) a directed is
(b) what cycles in a directed graph are
(c) What an evaluation sequence is
More relevanto would be what a "truth-maker" is.
Anyway, it seems that Prolog does not say anything about
truth-bearers because Prolog does not say anything about
truth-bearers.
When Prolog derives expression x from Facts and Rules
by applying the truth preserving operations of Rules to
Facts is the truthmaker for truth-bearer x.
A Prolog impementation applies Prolog operations.
Which are (like logic) for the most part truth preserving.
If (A & B) then A
Logic where the infoerence rules are for the most part truth prserving >>>> is not useful. They all must be.
For some cases
Prolog offers several operations letting the implementation to
choose which one to apply.
I don't thing so. Once the Facts and Rules are specified
Prolog chooses whatever Facts and Rules to prove x or not.
It is back-chained inference.
Standard Prolog is what the Prolog standard says. Conforming implementations
may vary if the standard allows. If you think otherwise you are wrong. >>>> There are also non-starndard Prlongs that vary even more.
The fundamental architectural overview of all Prolog implementations
is the same True(x) means X is derived by applying Rules (AKA truth
preserving operations) to Facts.
The details are permitted to differ.
Instead of using any single order of logic we simultaneously
represent an arbitrary number of orders of logic in a type
hierarchy knowledge ontology.
On 9/8/2024 3:45 AM, Mikko wrote:
On 2024-09-07 13:06:52 +0000, olcott said:
On 9/7/2024 3:35 AM, Mikko wrote:
On 2024-09-06 12:22:04 +0000, olcott said:
The fundamental architectural overview of all Prolog implementations >>>>> is the same True(x) means X is derived by applying Rules (AKA truth
preserving operations) to Facts.
The details are permitted to differ.
Instead of using any single order of logic we simultaneously
represent an arbitrary number of orders of logic in a type
hierarchy knowledge ontology.
The type system of Prolog is different.
Yes I know that. The architecture of Prolog is used
the implementation details are scrapped.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false. // LP is rejected as cyclic
Even with Prolog just the way it is it is not as stupid
as Tarski's system that doesn't know to reject the Liar
Paradox.
https://liarparadox.org/Tarski_247_248.pdf
On 9/8/2024 9:31 AM, Mikko wrote:
On 2024-09-08 12:44:56 +0000, olcott said:
On 9/8/2024 3:45 AM, Mikko wrote:
On 2024-09-07 13:06:52 +0000, olcott said:
On 9/7/2024 3:35 AM, Mikko wrote:
On 2024-09-06 12:22:04 +0000, olcott said:
The fundamental architectural overview of all Prolog implementations >>>>>>> is the same True(x) means X is derived by applying Rules (AKA truth >>>>>>> preserving operations) to Facts.
The details are permitted to differ.
Instead of using any single order of logic we simultaneously
represent an arbitrary number of orders of logic in a type
hierarchy knowledge ontology.
The type system of Prolog is different.
Yes I know that. The architecture of Prolog is used
the implementation details are scrapped.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false. // LP is rejected as cyclic
Even with Prolog just the way it is it is not as stupid
as Tarski's system that doesn't know to reject the Liar
Paradox.
https://liarparadox.org/Tarski_247_248.pdf
Most Prolog implementations don't reject L = not(ture(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
Prolog just gets stuck in an infinite loop
when a cyclic term is unified.
On 9/9/2024 4:05 AM, Mikko wrote:
On 2024-09-08 14:38:51 +0000, olcott said:
On 9/8/2024 9:31 AM, Mikko wrote:
On 2024-09-08 12:44:56 +0000, olcott said:
On 9/8/2024 3:45 AM, Mikko wrote:
On 2024-09-07 13:06:52 +0000, olcott said:
On 9/7/2024 3:35 AM, Mikko wrote:
On 2024-09-06 12:22:04 +0000, olcott said:
The fundamental architectural overview of all Prolog implementations >>>>>>>>> is the same True(x) means X is derived by applying Rules (AKA truth >>>>>>>>> preserving operations) to Facts.
The details are permitted to differ.
Instead of using any single order of logic we simultaneously
represent an arbitrary number of orders of logic in a type
hierarchy knowledge ontology.
The type system of Prolog is different.
Yes I know that. The architecture of Prolog is used
the implementation details are scrapped.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false. // LP is rejected as cyclic
Even with Prolog just the way it is it is not as stupid
as Tarski's system that doesn't know to reject the Liar
Paradox.
https://liarparadox.org/Tarski_247_248.pdf
Most Prolog implementations don't reject L = not(ture(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
Prolog just gets stuck in an infinite loop
when a cyclic term is unified.
You can ask "unify_with_occurs_check(LP, not(true(LP)))" but you
needn't. If you don't ask it doen't reject.
It gets stuck in an infinite loop.
You can say that
"LP = not(true(LP))" and most Prolog implementations simply
assign not(true(LP) to LP. Whether your program gets stuck in
an infinite loop depends on what you try to do with LP.
?- LP. % Gets stuck in an infinite loop
On 9/10/2024 4:12 AM, Mikko wrote:
On 2024-09-09 13:12:13 +0000, olcott said:
On 9/9/2024 4:05 AM, Mikko wrote:
On 2024-09-08 14:38:51 +0000, olcott said:
On 9/8/2024 9:31 AM, Mikko wrote:
On 2024-09-08 12:44:56 +0000, olcott said:
On 9/8/2024 3:45 AM, Mikko wrote:
On 2024-09-07 13:06:52 +0000, olcott said:
On 9/7/2024 3:35 AM, Mikko wrote:
On 2024-09-06 12:22:04 +0000, olcott said:
The fundamental architectural overview of all Prolog
implementations
is the same True(x) means X is derived by applying Rules (AKA >>>>>>>>>>> truth preserving operations) to Facts.
The details are permitted to differ.
Instead of using any single order of logic we simultaneously >>>>>>>>> represent an arbitrary number of orders of logic in a type
hierarchy knowledge ontology.
The type system of Prolog is different.
Yes I know that. The architecture of Prolog is used
the implementation details are scrapped.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false. // LP is rejected as cyclic
Even with Prolog just the way it is it is not as stupid
as Tarski's system that doesn't know to reject the Liar
Paradox.
https://liarparadox.org/Tarski_247_248.pdf
Most Prolog implementations don't reject L = not(ture(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
Prolog just gets stuck in an infinite loop
when a cyclic term is unified.
You can ask "unify_with_occurs_check(LP, not(true(LP)))" but you
needn't. If you don't ask it doen't reject.
It gets stuck in an infinite loop.
You can say that
"LP = not(true(LP))" and most Prolog implementations simply
assign not(true(LP) to LP. Whether your program gets stuck in
an infinite loop depends on what you try to do with LP.
?- LP. % Gets stuck in an infinite loop
As I already said, some operations with LP get stuck in an infinite loop.
That does not prevent the use of LP in other operations. For example,
LP = not(LP) does not get stuck but simply evaluates to false.
LP == "this sentence is not true"
True(LP)
"LP is rejected an invalid input"
On 9/10/2024 4:12 AM, Mikko wrote:
On 2024-09-09 13:12:13 +0000, olcott said:
On 9/9/2024 4:05 AM, Mikko wrote:
On 2024-09-08 14:38:51 +0000, olcott said:
On 9/8/2024 9:31 AM, Mikko wrote:
On 2024-09-08 12:44:56 +0000, olcott said:
On 9/8/2024 3:45 AM, Mikko wrote:
On 2024-09-07 13:06:52 +0000, olcott said:
On 9/7/2024 3:35 AM, Mikko wrote:
On 2024-09-06 12:22:04 +0000, olcott said:
The fundamental architectural overview of all Prolog implementations
is the same True(x) means X is derived by applying Rules (AKA truth >>>>>>>>>>> preserving operations) to Facts.
The details are permitted to differ.
Instead of using any single order of logic we simultaneously >>>>>>>>> represent an arbitrary number of orders of logic in a type
hierarchy knowledge ontology.
The type system of Prolog is different.
Yes I know that. The architecture of Prolog is used
the implementation details are scrapped.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false. // LP is rejected as cyclic
Even with Prolog just the way it is it is not as stupid
as Tarski's system that doesn't know to reject the Liar
Paradox.
https://liarparadox.org/Tarski_247_248.pdf
Most Prolog implementations don't reject L = not(ture(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
Prolog just gets stuck in an infinite loop
when a cyclic term is unified.
You can ask "unify_with_occurs_check(LP, not(true(LP)))" but you
needn't. If you don't ask it doen't reject.
It gets stuck in an infinite loop.
You can say that
"LP = not(true(LP))" and most Prolog implementations simply
assign not(true(LP) to LP. Whether your program gets stuck in
an infinite loop depends on what you try to do with LP.
?- LP. % Gets stuck in an infinite loop
As I already said, some operations with LP get stuck in an infinite loop.
That does not prevent the use of LP in other operations. For example,
LP = not(LP) does not get stuck but simply evaluates to false.
LP == "this sentence is not true"
True(LP)
"LP is rejected an invalid input"
| Sysop: | Keyop |
|---|---|
| Location: | Huddersfield, West Yorkshire, UK |
| Users: | 715 |
| Nodes: | 16 (3 / 13) |
| Uptime: | 03:22:16 |
| Calls: | 12,099 |
| Calls today: | 7 |
| Files: | 15,003 |
| Messages: | 6,517,876 |