Sujet : Re: This is how I overturn the Tarski Undefinability theorem
De : mikko.levanto (at) *nospam* iki.fi (Mikko)
Groupes : sci.logicDate : 11. Sep 2024, 09:29:46
Autres entêtes
Organisation : -
Message-ID : <vbrgta$3fs7t$1@dont-email.me>
References : 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
User-Agent : Unison/2.2
On 2024-09-10 13:10:27 +0000, olcott said:
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"
If you can't say anything you needn't babble.
-- Mikko
This is how I overturn the Tarski Undefinability theorem
Re: This is how I overturn the Tarski Undefinability theorem
