Path: ...!weretis.net!feeder9.news.weretis.net!i2pn.org!i2pn2.org!.POSTED!not-for-mail
From: Richard Damon <richard@damon-family.org>
Newsgroups: sci.logic
Subject: Re: This is how I overturn the Tarski Undefinability theorem
Date: Tue, 3 Sep 2024 22:28:07 -0400
Organization: i2pn2 (i2pn.org)
Message-ID: <b2d2364ddfdd70e6e85e6871914bd236ffb528c8@i2pn2.org>
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>
 <vb4cv3$2r7ok$3@dont-email.me> <vb6ouc$3achu$1@dont-email.me>
 <vb70ah$3b4ub$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Wed, 4 Sep 2024 02:28:07 -0000 (UTC)
Injection-Info: i2pn2.org;
	logging-data="771834"; mail-complaints-to="usenet@i2pn2.org";
	posting-account="diqKR1lalukngNWEqoq9/uFtbkm5U+w3w6FQ0yesrXg";
User-Agent: Mozilla Thunderbird
Content-Language: en-US
In-Reply-To: <vb70ah$3b4ub$1@dont-email.me>
X-Spam-Checker-Version: SpamAssassin 4.0.0
Bytes: 4579
Lines: 96

On 9/3/24 8:44 AM, olcott wrote:
> On 9/3/2024 5:38 AM, Mikko wrote:
>> On 2024-09-02 13:01:23 +0000, olcott said:
>>
>>> 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.
>>
>> A Prolog impementation applies Prolog operations. 
> 
> Which are (like logic) for the most part truth preserving.
> If (A & B) then A

But Prolog can not express ALL logical statement.

> 
>> For some cases
>> Prolog offers several operations letting the implementation to
>> choose which one to apply. 
> 
> I don't thing so. Once the Facts and Rules are specified
> Prolog chooses whatever Facts and Rules to prove x or not.
> It is back-chained inference.

But the set of Prolog operations are limited compared to logic.

> 
>> Consequently some goals may evaluate
>> to true in some implementations and false in others, for example
>>
>>   L = [L].
>>
> 
>