Path: ...!news.mixmin.net!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: olcott <polcott333@gmail.com>
Newsgroups: sci.logic,comp.theory
Subject: Re: True on the basis of meaning --- Good job Richard ! ---Socratic
 method MTT
Date: Tue, 28 May 2024 21:39:54 -0500
Organization: A noiseless patient Spider
Lines: 119
Message-ID: <v364hp$vl7m$1@dont-email.me>
References: <v1mljr$1q5ee$4@dont-email.me> <v2bsog$36vvc$1@dont-email.me>
 <v2cpb1$1g2n8$1@i2pn2.org> <v2cvj6$3ddo5$1@dont-email.me>
 <v2d0qp$3dlkm$1@dont-email.me> <v2d1io$3dplm$1@dont-email.me>
 <v2evl5$3snmj$1@dont-email.me> <v2g2dp$3ugq$1@dont-email.me>
 <v2hkkl$ggq9$1@dont-email.me> <v2ibhe$ksut$1@dont-email.me>
 <v2k8go$1363g$1@dont-email.me> <v2l4hr$188bi$3@dont-email.me>
 <v2l87m$19619$1@dont-email.me> <v2lies$1b4kp$1@dont-email.me>
 <v2ltgl$1nrfv$2@i2pn2.org> <v2m0m5$1dcof$2@dont-email.me>
 <v2m4lg$1qo0t$1@i2pn2.org> <v2mtkj$1ln2l$1@dont-email.me>
 <v2ngi3$1or9h$8@dont-email.me> <v2pig4$28a91$1@dont-email.me>
 <v2qp30$2f6v4$1@dont-email.me> <v2s5td$2psu4$1@dont-email.me>
 <v2t9ne$2vna0$5@dont-email.me> <v2usea$3be7o$1@dont-email.me>
 <v2veqj$3e8pb$1@dont-email.me> <v31eit$3ugn4$1@dont-email.me>
 <v324iu$2pkb$1@dont-email.me> <v324pa$2rt4$1@dont-email.me>
 <v325l6$2pkb$3@dont-email.me> <v33vc1$g5n4$1@dont-email.me>
 <v34rgj$l2fc$1@dont-email.me> <v362er$2d367$1@i2pn2.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Wed, 29 May 2024 04:39:54 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="b7a5feb561e035e50c2e5bc5a99a467f";
	logging-data="1037558"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1+kDO20kXXOUnpSOoKVCU1y"
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:skzkixENyrzn4juOvW9UxbbORjo=
In-Reply-To: <v362er$2d367$1@i2pn2.org>
Content-Language: en-US
Bytes: 6523

On 5/28/2024 9:04 PM, Richard Damon wrote:
> On 5/28/24 10:59 AM, olcott wrote:
>> On 5/28/2024 1:59 AM, Mikko wrote:
>>> On 2024-05-27 14:34:14 +0000, olcott said:
>>>
>>>> ?- LP = not(true(LP)).
>>>> LP = not(true(LP)).
>>>>
>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>> false.
>>>>
>>>> In other words Prolog has detected a cycle in the directed graph of the
>>>> evaluation sequence of the structure of the Liar Paradox. Experts seem
>>>> to think that Prolog is taking "not" and "true" as meaningless and is
>>>> only evaluating the structure of the expression.
>>>
>>> The words "not" and "true" of Prolog are meaningful in some contexts
>>> but not above. The word "true" is meaningful only when it has no 
>>> arguments.
>>>
>>
>> That Prolog construes any expression having the same structure as the
>> Liar Paradox as having a cycle in the directed graph of its evaluation
>> sequence already completely proves my point. In other words Prolog
>> is saying that there is something wrong with the expression and it must
>> be rejected.
> 
> But Prolog doesn't support powerful enough logic to handle the system 
> like Tarski and Godel are talking about.
> 
> The fact that Prolog just rejects it shows that.
> 

Your ignorance is no excuse.

>>
>>> You could try
>>> ?- LP = not(true(LP), true(LP).
>>>
>>> or
>>> ?- LP = not(true(LP), not(true(LP)).
>>>
>>> The predicate unify_with_occurs_check checks whether the resulting
>>> sructure is acyclic because that is its purpose. Whether a simple
>>
>> Yes exactly. If I knew that Prolog did this then I would not have
>> created Minimal Type Theory that does this same thing. That I did
>> create MTT that does do this same thing makes my understanding much
>> deeper.
>>
>>> unification like LP = not(true(LP)) does same is implementation
>>> dependent as Prolog rules permit but do not require that. In a
>>> typical implementation a simple unification does not check for
>>> cycles.
>>>
>>
>> ISO Prolog implementations have the built-in predicate
>> unify_with_occurs_check/2 for sound unification
>> https://en.wikipedia.org/wiki/Occurs_check#Sound_unification
>>
>> Alternatively such expressions crash or remain stuck in infinite loops.
>>
>>
>>> Anyway, none of this is relevant to the topic of this thread or
>>> topics of sci.logic.
>>>
>>
>>     ...14 Every epistemological antinomy can likewise be used for
>>     a similar undecidability proof...(Gödel 1931:40)
>>
>> Gödel, Kurt 1931.
>> On Formally Undecidable Propositions of Principia Mathematica And 
>> Related Systems
>>
>> https://monoskop.org/images/9/93/Kurt_G%C3%B6del_On_Formally_Undecidable_Propositions_of_Principia_Mathematica_and_Related_Systems_1992.pdf
>>
>>     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.
>>
>> CONCEPT OF TRUTH IN FORMALIZED LANGUAGES, Tarski
>> https://liarparadox.org/Tarski_247_248.pdf
>>
>> The Liar Paradox and other such {epistemological antinomies} must be
>> rejected as type mismatch errors for any system of bivalent logic thus
>> cannot be correctly used for any undecidability or undefinability proof.
>>
> 
> But you just don't don't understand what was done in those proofs.
> 
> Neither of them assumed the Liar's paradox had a truth value. Only 
> statements formed from VALID logical sequences in the field.
> 
> Please try to show what step in Godel's or Tarski's proof where they 
> made a logical error (not just came up with a statement you think can't 
> be valid).
> 

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

adapted to become the first line of his proof
x ∉ Pr if and only if p

-- 
Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer