| Sysop: | Amessyroom |
|---|---|
| Location: | Fayetteville, NC |
| Users: | 23 |
| Nodes: | 6 (0 / 6) |
| Uptime: | 54:44:40 |
| Calls: | 583 |
| Files: | 1,139 |
| D/L today: |
179 files (27,921K bytes) |
| Messages: | 111,801 |
All that we must do to defeat the Tarski Undefinability Theorem:
We define the notion of formal system as an extended
version of Prolog's Facts and Rules. This new system
can handle arbitrary orders of logic. Encodes Facts
in formalized natural language.
The Rules only allow semantic logical entailment from
Facts. When we do this Tarski's Liar Paradox basis is
simply rejected as untrue and
Boolean True(Language L, Expression E) becomes definable.
All that we must do to defeat the Tarski Undefinability Theorem:
We define the notion of formal system as an extended
version of Prolog's Facts and Rules. This new system
can handle arbitrary orders of logic.
Encodes Facts
in formalized natural language.
The Rules only allow semantic logical entailment from
Facts.
When we do this Tarski's Liar Paradox basis is
simply rejected as untrue and
Boolean True(Language L, Expression E) becomes definable.
On 2025-08-25 17:54:02 +0000, olcott said:
All that we must do to defeat the Tarski Undefinability Theorem:
Bad luck if you must but can't.
We define the notion of formal system as an extended
version of Prolog's Facts and Rules. This new system
can handle arbitrary orders of logic.
Prolog's system already can. But it cannot handle negations.
Encodes Facts
in formalized natural language.
The Rules only allow semantic logical entailment from
Facts.
You can't encode "semantic logical entailment" in the rules.
Without a formal definition those words are formally nonsense.
When we do this Tarski's Liar Paradox basis is
simply rejected as untrue and
Boolean True(Language L, Expression E) becomes definable.
As Tarski proved, if True(Language L, Expression E) is definable
then Liar Paradox is provably true (therefore not rejectable as
untrue) and provably false, so true is the same as false.
On 8/26/2025 5:11 AM, Mikko wrote:
On 2025-08-25 17:54:02 +0000, olcott said:
All that we must do to defeat the Tarski Undefinability Theorem:
Bad luck if you must but can't.
I create the basic architecture and others implement it.
We define the notion of formal system as an extended
version of Prolog's Facts and Rules. This new system
can handle arbitrary orders of logic.
Prolog's system already can. But it cannot handle negations.
It not that it can't handle negations.
It handles them differently.
https://en.wikipedia.org/wiki/Negation_as_failure
That is the key to avoiding self-referential paradoxes.
They simply are not derived in the system making them
untrue in the system.
LP = "this sentence is not true"
Boolean True("English", LP)==FALSE
Boolean True("English", ~LP)==FALSE
Encodes Facts
in formalized natural language.
The Rules only allow semantic logical entailment from
Facts.
You can't encode "semantic logical entailment" in the rules.
Without a formal definition those words are formally nonsense.
https://plato.stanford.edu/entries/montague-semantics/
Formalizes natural language semantics syntactically.
When we do this Tarski's Liar Paradox basis is
simply rejected as untrue and
Boolean True(Language L, Expression E) becomes definable.
As Tarski proved, if True(Language L, Expression E) is definable
then Liar Paradox is provably true (therefore not rejectable as
untrue) and provably false, so true is the same as false.
Not at all. Tarski got confused by this.
This sentence is not true: "This sentence is not true" is true.
He never noticed that the Liar Paradox is not a bearer of truth
and must be rejected on that basis as not an member of any
logic system. Prolog does notice that:
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
On 2025-08-26 15:16:31 +0000, olcott said:
On 8/26/2025 5:11 AM, Mikko wrote:
On 2025-08-25 17:54:02 +0000, olcott said:
All that we must do to defeat the Tarski Undefinability Theorem:
Bad luck if you must but can't.
I create the basic architecture and others implement it.
Post again when you have the basic architecture on a web site.
We define the notion of formal system as an extended
version of Prolog's Facts and Rules. This new system
can handle arbitrary orders of logic.
Prolog's system already can. But it cannot handle negations.
It not that it can't handle negations.
It is.
It handles them differently.
It handles a different thing.
https://en.wikipedia.org/wiki/Negation_as_failure
That is the key to avoiding self-referential paradoxes.
They simply are not derived in the system making them
untrue in the system.
You can define a self-reference. You cant refer to the
negation of self.
LP =-a "this sentence is not true"
Boolean True("English", LP)==FALSE
Boolean True("English", ~LP)==FALSE
There is nothing in Prolog that means '~'.
Encodes Facts
in formalized natural language.
The Rules only allow semantic logical entailment from
Facts.
You can't encode "semantic logical entailment" in the rules.
Without a formal definition those words are formally nonsense.
https://plato.stanford.edu/entries/montague-semantics/
Formalizes natural language semantics syntactically.
You can't formalize all of natural language semantics.
When we do this Tarski's Liar Paradox basis is
simply rejected as untrue and
Boolean True(Language L, Expression E) becomes definable.
It doesn't be come definable if it isn't already.
As Tarski proved, if True(Language L, Expression E) is definable
then Liar Paradox is provably true (therefore not rejectable as
untrue) and provably false, so true is the same as false.
Not at all. Tarski got confused by this.
This sentence is not true: "This sentence is not true" is true.
No, Tarski got it right when he said that "This sentence is not true"
is not true.
You can't prove that "This sentence is not true" is true.
He never noticed that the Liar Paradox is not a bearer of truth
and must be rejected on that basis as not an member of any
logic system. Prolog does notice that:
What he used in place of the Liar paradox is a valid sentence that
can be used in proofs, either as a sentence or as a part of a larger sentence.
?- LP = not(true(LP)).
LP = not(true(LP)).
Note that the word "not" above does not mean the logical negation.
?- unify_with_occurs_check(LP, not(true(LP))).
false.
Note that the word "not" above does not mean the logical negation.
That unify_with_occurs_check fails does not prove that the two
expressions do not mean the same.
?- unify_with_occurs_check(LP, true(LP)).
false.
On 8/27/2025 3:28 AM, Mikko wrote:
On 2025-08-26 15:16:31 +0000, olcott said:
On 8/26/2025 5:11 AM, Mikko wrote:
On 2025-08-25 17:54:02 +0000, olcott said:
All that we must do to defeat the Tarski Undefinability Theorem:
Bad luck if you must but can't.
I create the basic architecture and others implement it.
Post again when you have the basic architecture on a web site.
No.
On 2025-08-27 15:27:26 +0000, olcott said:
On 8/27/2025 3:28 AM, Mikko wrote:
On 2025-08-26 15:16:31 +0000, olcott said:
On 8/26/2025 5:11 AM, Mikko wrote:
On 2025-08-25 17:54:02 +0000, olcott said:
All that we must do to defeat the Tarski Undefinability Theorem:
Bad luck if you must but can't.
I create the basic architecture and others implement it.
Post again when you have the basic architecture on a web site.
No.
OK, but then we can't discuss it.
On 8/28/2025 2:50 AM, Mikko wrote:
On 2025-08-27 15:27:26 +0000, olcott said:
On 8/27/2025 3:28 AM, Mikko wrote:
On 2025-08-26 15:16:31 +0000, olcott said:
On 8/26/2025 5:11 AM, Mikko wrote:
On 2025-08-25 17:54:02 +0000, olcott said:
All that we must do to defeat the Tarski Undefinability Theorem:
Bad luck if you must but can't.
I create the basic architecture and others implement it.
Post again when you have the basic architecture on a web site.
No.
OK, but then we can't discuss it.
Prolog already knows to reject the Liar Paradox
as not a truth-bearer.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
On 2025-08-28 15:31:28 +0000, olcott said:
On 8/28/2025 2:50 AM, Mikko wrote:
On 2025-08-27 15:27:26 +0000, olcott said:
On 8/27/2025 3:28 AM, Mikko wrote:
On 2025-08-26 15:16:31 +0000, olcott said:
On 8/26/2025 5:11 AM, Mikko wrote:
On 2025-08-25 17:54:02 +0000, olcott said:
All that we must do to defeat the Tarski Undefinability Theorem: >>>>>>>Bad luck if you must but can't.
I create the basic architecture and others implement it.
Post again when you have the basic architecture on a web site.
No.
OK, but then we can't discuss it.
Prolog already knows to reject the Liar Paradox
as not a truth-bearer.
No, it does not. Prolog doesn't identify anything as a "truth-bearer"
or "non-truth-bearer".
?- LP = not(true(LP)).
The Prolog standard allows an implementation to accept or reject that.
Most implementations accept.
LP = not(true(LP)).
This time the implementation accepted and assigned a value to LP.
?- unify_with_occurs_check(LP, not(true(LP))).
In this case an implementation is required to reject as the result
of unification would be an expression that contains itself. Whether
anything is a truth-bearer or not is not checked.
false.
Implementation rejected as required.
On 8/29/2025 1:42 AM, Mikko wrote:
On 2025-08-28 15:31:28 +0000, olcott said:
On 8/28/2025 2:50 AM, Mikko wrote:
On 2025-08-27 15:27:26 +0000, olcott said:
On 8/27/2025 3:28 AM, Mikko wrote:
On 2025-08-26 15:16:31 +0000, olcott said:
On 8/26/2025 5:11 AM, Mikko wrote:
On 2025-08-25 17:54:02 +0000, olcott said:
All that we must do to defeat the Tarski Undefinability Theorem: >>>>>>>>Bad luck if you must but can't.
I create the basic architecture and others implement it.
Post again when you have the basic architecture on a web site.
No.
OK, but then we can't discuss it.
Prolog already knows to reject the Liar Paradox
as not a truth-bearer.
No, it does not. Prolog doesn't identify anything as a "truth-bearer"
or "non-truth-bearer".
The code below proves that LP is not a truth
bearer even if Prolog were to call it an ice
cream sundae with a cherry on top.
LP cannot be resolved to a truth value because
it specifies infinite recursion.
?- LP = not(true(LP)).
The Prolog standard allows an implementation to accept or reject that.
Most implementations accept.
LP = not(true(LP)).
This time the implementation accepted and assigned a value to LP.
?- unify_with_occurs_check(LP, not(true(LP))).
In this case an implementation is required to reject as the result
of unification would be an expression that contains itself. Whether
anything is a truth-bearer or not is not checked.
false.
Implementation rejected as required.
Because it specifies infinite recursion.
Other systems might just get stuck in infinite recursion.
On 2025-08-29 13:56:47 +0000, olcott said:
LP cannot be resolved to a truth value because
it specifies infinite recursion.
Prolog does not even try to resolve LP to a truth value.
Because it specifies infinite recursion.
Yes, but the cause is not reported. The result is the same as it would
be if the two arguments were bound to incompatible values.
Other systems might just get stuck in infinite recursion.
That is possible. In such systems a program that produces a recursive structure is often defiend as erroneous even if the system is not
required to detect the error.
On 8/30/2025 2:51 AM, Mikko wrote:
On 2025-08-29 13:56:47 +0000, olcott said:
LP cannot be resolved to a truth value because
it specifies infinite recursion.
Prolog does not even try to resolve LP to a truth value.
Because it specifies infinite recursion.
Yes, but the cause is not reported. The result is the same as it would
be if the two arguments were bound to incompatible values.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
Prolog rejects LP as specifying infinite recursion
thus rejecting the basis of the Tarski Undefinability Theorem
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
On 2025-08-30 15:31:20 +0000, olcott said:
On 8/30/2025 2:51 AM, Mikko wrote:
On 2025-08-29 13:56:47 +0000, olcott said:
LP cannot be resolved to a truth value because
it specifies infinite recursion.
Prolog does not even try to resolve LP to a truth value.
Because it specifies infinite recursion.
Yes, but the cause is not reported. The result is the same as it would
be if the two arguments were bound to incompatible values.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
Prolog rejects LP as specifying infinite recursion
thus rejecting the basis of the Tarski Undefinability Theorem
Prolog does not say anyathing about an infinite recursion.
The result is the same for
-a?- unify_with_occurs_check(true(not(LP)), not(true(LP))).
which does not contain any infinite recursion.
-a-a It would then be possible to reconstruct the
-a-a antinomy of the liar in the metalanguage, by
-a-a forming in the language itself a sentence x
-a-a such that the sentence of the metalanguage
-a-a which is correlated with x asserts that x is
-a-a not a true sentence.
-a-a https://liarparadox.org/Tarski_247_248.pdf
Your quote omits essential context. In particular the meanng of "then"
is not clear from the quote. From the omitted context it is clear that
the meaning is 'if a truth predicate could be defined'.
On 8/31/2025 3:24 AM, Mikko wrote:
On 2025-08-30 15:31:20 +0000, olcott said:
On 8/30/2025 2:51 AM, Mikko wrote:
On 2025-08-29 13:56:47 +0000, olcott said:
LP cannot be resolved to a truth value because
it specifies infinite recursion.
Prolog does not even try to resolve LP to a truth value.
Because it specifies infinite recursion.
Yes, but the cause is not reported. The result is the same as it would >>>> be if the two arguments were bound to incompatible values.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
Prolog rejects LP as specifying infinite recursion
thus rejecting the basis of the Tarski Undefinability Theorem
Prolog does not say anyathing about an infinite recursion.
The result is the same for
*Yes it does, you just deleted this*
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)
Clocksin, W.F. and Mellish, C.S.
2003. Programming in Prolog Using the ISO Standard Fifth Edition, 254. Berlin Heidelberg: Springer-Verlag.
https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence