Re: This is how I overturn the Tarski Undefinability theorem

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.