Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: olcott <polcott333@gmail.com>
Newsgroups: sci.logic
Subject: Re: This is how I overturn the Tarski Undefinability theorem
Date: Mon, 2 Sep 2024 08:01:23 -0500
Organization: A noiseless patient Spider
Lines: 119
Message-ID: <vb4cv3$2r7ok$3@dont-email.me>
References: <vavohi$140m1$1@dont-email.me> <vb1o2v$1gbmn$1@dont-email.me>
 <vb1r8k$1g7lq$3@dont-email.me> <vb3quu$1t290$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 02 Sep 2024 15:01:24 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="a2fe8748f6382997edaeece42547d6b5";
	logging-data="2989844"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX188CR956ITuy0EcBWXMl9cB"
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:OSJV2sQg/t+FrTKjwvS57Rs1PVQ=
Content-Language: en-US
In-Reply-To: <vb3quu$1t290$1@dont-email.me>
Bytes: 5441

On 9/2/2024 2:54 AM, Mikko wrote:
> On 2024-09-01 13:47:00 +0000, olcott said:
> 
>> On 9/1/2024 7:52 AM, Mikko wrote:
>>> On 2024-08-31 18:48:18 +0000, olcott said:
>>>
>>>> *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)).
>>>
>>> According to Prolog semantics "false" would also be a correct
>>> response.
>>>
>>>> ?- 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.
>>>
>>>> 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.

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

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

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