Path: ...!2.eu.feeder.erje.net!feeder.erje.net!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Mikko <mikko.levanto@iki.fi>
Newsgroups: sci.logic
Subject: Re: This is how I overturn the Tarski Undefinability theorem
Date: Mon, 2 Sep 2024 10:54:06 +0300
Organization: -
Lines: 80
Message-ID: <vb3quu$1t290$1@dont-email.me>
References: <vavohi$140m1$1@dont-email.me> <vb1o2v$1gbmn$1@dont-email.me> <vb1r8k$1g7lq$3@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 09:54:06 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="4ae33bef920975be84e44326db049334";
	logging-data="2001184"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX19kZdxANnOVo3BCLkGc+vrT"
User-Agent: Unison/2.2
Cancel-Lock: sha1:cWgr/Vj0YtKV8jLAn43VtkJLu3c=
Bytes: 3835

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.

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

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

-- 
Mikko