Path: ...!weretis.net!feeder8.news.weretis.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: Sun, 8 Sep 2024 11:45:42 +0300
Organization: -
Lines: 112
Message-ID: <vbjo7m$1s9qb$1@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> <vb4cv3$2r7ok$3@dont-email.me> <vb6ouc$3achu$1@dont-email.me> <vb70ah$3b4ub$1@dont-email.me> <vbeqjh$qc12$1@dont-email.me> <vbes5c$punj$11@dont-email.me> <vbh37k$19rlv$1@dont-email.me> <vbhj5c$1c7u5$2@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sun, 08 Sep 2024 10:45:42 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="71003b4a941dae1a07e7f53567e028f8";
	logging-data="1976139"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1+oBdifMqKOxlopG6rrpIPc"
User-Agent: Unison/2.2
Cancel-Lock: sha1:wTe2L4gBPRhN5IxItRcqKk7Ka/g=
Bytes: 5757

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

-- 
Mikko