Discussion:
This is how I overturn the Tarski Undefinability theorem
(too old to reply)
olcott
2024-08-31 18:48:18 UTC
Permalink
*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
--
Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer
Richard Damon
2024-08-31 19:11:13 UTC
Permalink
Post by olcott
*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.
Right, so when x in L is defined to be !True(L,x) does such a connetion
exist?
Post by olcott
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
Right, he *SHOWS* that in the system, it is possible to create the
statement that

x (in L) is defined to be ~True(L, x)

PERIOD.

Try to show where is proof of such a statement is wrong.
Your problem is you don't understand what Tarski is doing at all, so you
can't point to a statement that is in error, just that you think the
answer must be wrong. THAT is not a "refuation", just proof that it is
likely that the error is in *YOUR* ideas,

So, if you claim that such a statement x can neither be established or
refuted in L, then BY THE DEFINITION of the "True" prediciate, that is
that True is TRUE if the statement is actually true, while FALSE for all
other cases, either being refutable, or being a non-truth bearer, then
True(L, x) must be FALSE, but that means that !True(L, x) must be TRUE,
and thus x *IS* establish as a TRUE statement, derivable from the fact
that True(L, x) was FALSE, and the definition of negation.

This means that there exist a statement (x) which is TRUE, but True(L,x)
is FALSE, and thus the predicate True can not meet its definition.

This shows that no such predicate can meet that definition.

Unless you can resolve THAT contradiciton somehow, you have to accept
the conclusion, or just admit you don't understand how logic works.
Post by olcott
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*
But that is invalid, as Prolog doesn't support the needed degree of logic.
Post by olcott
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
As Prolog admits here. All you have done here is proven that you don't
actually understand how logic works.
Post by olcott
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.
Which is meaningless as Prolog doesn't support the needed level of
logic, and proves that YOU don't support the needed level of logic, and
thus your "arguement" is just invalid, and you claims just lies.
Post by olcott
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
Which was a statement taken from unpublished papers, and was apparently
from before Wittgenstein had even read the actual Godel paper.

We don't know if Wittgenstein even continued to believe this, with the
question, if he did, why did he not publish it?
Mikko
2024-09-01 12:52:47 UTC
Permalink
Post by olcott
*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
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.
Post by olcott
?- 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.
Post by olcott
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.
Post by olcott
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.
Post by olcott
https://www.liarparadox.org/Wittgenstein.pdf
--
Mikko
olcott
2024-09-01 13:47:00 UTC
Permalink
Post by Mikko
Post by olcott
*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
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.
Post by olcott
?- 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.
Post by olcott
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.
Post by Mikko
Post by olcott
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)
Post by Mikko
Post by olcott
https://www.liarparadox.org/Wittgenstein.pdf
--
Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer
Mikko
2024-09-02 07:54:06 UTC
Permalink
Post by olcott
Post by Mikko
Post by olcott
*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
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.
Post by olcott
?- 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.
Post by olcott
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.
Post by olcott
If you do know these things then Prolog proved that LP
has no truth-maker and thus cannot be a truth-bearer.
Prolog does not prove anythng about truth bearers. Certain kind
of Prolog programs can be regarded as proofs in a weak formal
system but that does not include those that end with "false".
Even then the proof is not a proof about anything, just a
formal proof.
Post by olcott
Post by Mikko
Post by olcott
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)
No, you did not.
--
Mikko
olcott
2024-09-02 13:01:23 UTC
Permalink
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
*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
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.
Post by olcott
?- 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.
Post by olcott
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.
Post by Mikko
Post by olcott
If you do know these things then Prolog proved that LP
has no truth-maker and thus cannot be a truth-bearer.
Prolog does not prove anythng about truth bearers.
Sure it does and it does this most directly when x is
unprovable in Prolog this proves that x has no truth-maker
in a set of Facts and Rules within the set of Facts and
Rules (AKA formal system).
Post by Mikko
Certain kind
of Prolog programs can be regarded as proofs in a weak formal
system but that does not include those that end with "false".
Even then the proof is not a proof about anything, just a
formal proof.
False in Prolog simply means that ~x is proved by a set of Facts
and Rules. When neither x nor ~x can be proved withing a set
of facts and Rules then x is not a truth-bearer in this formal
system of facts and Rules.
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
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)
No, you did not.
I just showed that when neither x nor ~x is provable within
a set of Facts and Rules (AKA formal system) that x is simply
not a truth bearer in this formal system.

If the formal system is about lug-nuts then we cannot say that
it is incomplete for not knowing about birthday cakes.

If x is self-contradictory then x is rejected as invalid input
the same way that Prolog rejects the Liar Paradox.

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

Prolog detects a cycle in the directed graph of the
evaluation sequence of LP meaning that the evaluation
of LP has an infinite loop that would never end.
--
Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer
olcott
2024-09-03 12:44:00 UTC
Permalink
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
*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
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.
Post by olcott
?- 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.
Post by olcott
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].
--
Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer
Mikko
2024-09-06 11:55:29 UTC
Permalink
Post by olcott
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
*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
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.
Post by olcott
?- 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.
Post by olcott
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.
Post by olcott
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.
Post by olcott
Consequently some goals may evaluate
to true in some implementations and false in others, for example
 L = [L].
No matter what you think this is an example. It is outside of the intended
application area but not prohibited.
--
Mikko
olcott
2024-09-06 12:22:04 UTC
Permalink
Post by Mikko
Post by olcott
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
*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
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.
Post by olcott
?- 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.
Post by olcott
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.
Post by olcott
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.

That is the way that all expressions X of language L are determined
to be true in L on the basis of the connection from X in L by truth
preserving operations to the semantic meaning of X in L.

{Linguistic truth} is the philosophical foundation of truth
in math and logic, AKA relations between finite strings.
Post by Mikko
Post by olcott
Consequently some goals may evaluate
to true in some implementations and false in others, for example
 L = [L].
No matter what you think this is an example. It is outside of the intended
application area but not prohibited.
--
Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer
Mikko
2024-09-07 08:35:00 UTC
Permalink
Post by olcott
Post by Mikko
Post by olcott
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
*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
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.
Post by olcott
?- 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.
Post by olcott
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.
Post by olcott
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.
--
Mikko
olcott
2024-09-07 13:06:52 UTC
Permalink
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
*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
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.
Post by olcott
?- 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.
Post by olcott
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.
Post by olcott
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.
--
Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer
Richard Damon
2024-09-07 13:19:10 UTC
Permalink
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
*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
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.
Post by olcott
?- 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.
Post by olcott
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.
Post by olcott
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.
Doesn't work, and just shows that you don't understand what you are
talking about.
olcott
2024-09-09 17:28:50 UTC
Permalink
Post by Richard Damon
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
*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
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.
Post by olcott
?- 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.
Post by olcott
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.
Post by olcott
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.
Doesn't work, and just shows that you don't understand what you are
talking about.
This <is> already implemented in conventional type theory.
Objects of thought at differing orders of logic are different types.
--
Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer
Mikko
2024-09-08 08:45:42 UTC
Permalink
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
*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
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.
Post by olcott
?- 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.
Post by olcott
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.
Post by olcott
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.
The type system of Prolog is different.
--
Mikko
olcott
2024-09-08 12:44:56 UTC
Permalink
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
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
--
Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer
Mikko
2024-09-08 14:31:23 UTC
Permalink
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
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)).
--
Mikko
olcott
2024-09-08 14:38:51 UTC
Permalink
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
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.
--
Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer
Mikko
2024-09-09 09:05:06 UTC
Permalink
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
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. 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.
--
Mikko
olcott
2024-09-09 13:12:13 UTC
Permalink
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
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.
Post by Mikko
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
--
Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer
Mikko
2024-09-10 09:12:48 UTC
Permalink
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
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.
Post by Mikko
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.
--
Mikko
olcott
2024-09-10 13:10:27 UTC
Permalink
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
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.
Post by Mikko
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"
--
Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer
Richard Damon
2024-09-11 01:37:01 UTC
Permalink
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
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.
Post by Mikko
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"
Not a valid answer for a predicate.

Sorry, you are just proving your stupidity.

If you want to make your own system, DO SO, and do it FULLY, not just
your half-ass incorrect method of trying to band-aid onto an existing
system after presuming to pull out the foundation, that just doesn't
work and shows that you just don't have the skills needed to even try
what you are claiming to do.
Mikko
2024-09-11 07:29:46 UTC
Permalink
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
Post by Mikko
Post by olcott
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.
Post by Mikko
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"
If you can't say anything you needn't babble.
--
Mikko
Loading...