From:  Mikko <mikko.levanto@iki.fi>
Date:  07 Sep 2024 16:35:00 Hong Kong Time
Newsgroup:  news.alt119.net/sci.logic
Subject:  

Re: This is how I overturn the Tarski Undefinability theorem

NNTP-Posting-Host:  null

On 2024-09-06 12:22:04 +0000, olcott said:

> On 9/6/2024 6:55 AM, Mikko wrote:
>> On 2024-09-03 12:44:00 +0000, olcott said:
>> 
>>> 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
>> 
>> Logic where the infoerence rules are for the most part truth prserving
>> is not useful. They all must be.
>> 
>>>> 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.
>> 
>> Standard Prolog is what the Prolog standard says. Conforming implementations
>> may vary if the standard allows. If you think otherwise you are wrong.
>> There are also non-starndard Prlongs that vary even more.
>> 
> 
> 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.

-- 
Mikko