Path: ...!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 22:54:07 -0500
Organization: A noiseless patient Spider
Lines: 142
Message-ID: <v368su$100kd$4@dont-email.me>
References: <v1mljr$1q5ee$4@dont-email.me> <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>
 <v364hp$vl7m$1@dont-email.me> <v36801$2d368$2@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 05:54:07 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="b7a5feb561e035e50c2e5bc5a99a467f";
	logging-data="1049229"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1+5ygdDJMrkoldZbXXK1VBG"
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:6eakDfe7QG99XcAanmco84Kut2o=
Content-Language: en-US
In-Reply-To: <v36801$2d368$2@i2pn2.org>
Bytes: 7601

On 5/28/2024 10:38 PM, Richard Damon wrote:
> On 5/28/24 10:39 PM, olcott wrote:
>> 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.
> 
> What ignorance?
> 

The fact that you assert that you know the underlying details of
https://www.swi-prolog.org/pldoc/man?predicate=unify_with_occurs_check/2
without even glancing at the documentation and write-up in Clocksin and
Mellish seems to be willful ignorance.

> The fact that I understand the limitation of Prolog and what forms of 
> logic it can do, which seems to be beyond your understanding?
> 
> Claiming that Prolog rejects a statement because it doesn't fit its 
> grammer is meaningless for more complicated logics that don't have that 
> same grammer restricition.
> 
> IF you want to limit the logic you use to what Prolog can handle, go 
> ahead, the rest of the world likes its mathematics.
> 
>>
>>>>
>>>>> 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
> 
> Right, He has SHOWN that the logic system, when given the assumption of 
> the existance of the Truth Predicate, can construct the liar as a 
> truth-bearing statement.
> 

Utterly Ridiculous (and you probably don't know it).

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