Re: This is how I overturn the Tarski Undefinability theorem

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. 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