Path: ...!weretis.net!feeder9.news.weretis.net!news.quux.org!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!eternal-september.org!.POSTED!not-for-mail From: Mikko Newsgroups: sci.logic Subject: Re: The key undecidable instance that I know about Date: Tue, 11 Mar 2025 13:15:07 +0200 Organization: - Lines: 106 Message-ID: References: MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Tue, 11 Mar 2025 12:15:08 +0100 (CET) Injection-Info: dont-email.me; posting-host="ac66f5fd211d01a7df4319119304e545"; logging-data="2049594"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19E8B3dur89+AMg4NmNleI/" User-Agent: Unison/2.2 Cancel-Lock: sha1:hWsGeTf6dya2HFF4Em1K26BpFgg= Bytes: 4645 On 2025-03-10 15:36:28 +0000, olcott said: > On 3/10/2025 4:48 AM, Mikko wrote: >> On 2025-03-09 17:15:13 +0000, olcott said: >> >>> Is the Liar Paradox True or False? >>> >>> LP := ~True(LP) >> >> In typical languages of formal logic that is not a syntactically valid >> expression. >> > > I created Minimal Type Theory such that self-reference > can be expressed concisely and correctly. Have you pbulished that "Minimal Type Theory" or put it to a web page? Without a pointer to it there is no point to mention it. Of course one can create a language that can express a self reference but why would one? > Apparently this cannot be expressed concisely and correctly in > any formal logic system. A self reference cannot be expressed in an uninterpreted formal language. Sometimes some symbols and expressions are interpreted to represent themselves or other symbols or expressions. For example, the symbol 0 of arthmetic can be interpreted to mean the symbol 0 and the term S0 the sqence of symbols S and 0. > Here is how this is typically done in formal systems > > 2.4 Diagonalization, or, “Self-reference” > https://plato.stanford.edu/entries/goedel-incompleteness/#DiaSelRef Diagonalixation is not what is "typically" done. It is done when it is useful. > LP := ~True(LP) is exactly self-reference without the > convoluted mess of the The Diagonalization Lemma. Only in languages that allow the expression. Typical formal languages either don't have the symbo ":=" or restrict its use so that the symbol on the left side cannot be used on the right side. In those languages the expression LP := ~True(LP) does not mean anything. > The other advantage of Minimal Type Theory is that It does not make sense to say "The other advantage" when you haven't already identified one. And how do you know there is no third advantage? > it outputs a directed graph of the evaluation sequence > explicitly showing any cycles that prove the expression > is invalid in the exact same way that > > ?- unify_with_occurs_check(LP, not(true(LP))). > proves that LP = not(true(LP)). has a cycle in its > evaluation sequence. The library predicate unify_with_occurs_check/2 gives the same result when asked "unify_with_occurs_check(1, 2)". Is there a cycle in the evaluation sequence of "1 = 2"? >>> ?- LP = not(true(LP)). >>> LP = not(true(LP)). >> >> Apparently you were using a Prolog implementation that does not check >> whether a cyclic data structure is produced. > > In other words you can see the infinite structure of: > ?- LP = not(true(LP)). Yes, but the unification algorithm of a typical Prolog implementation creates it without seeing it. > Not checking for cycles This is the default because > checking for cycles is too costly. And rarely useful. >> Another Prolog implementation >> could say false instead. >> >>> ?- unify_with_occurs_check(LP, not(true(LP))). >>> false. >> >> For this quesry the only permitted answer is false. > > Proving a cycle in the evaluation sequence of ?- LP = not(true(LP)). Only if there is a cycle in the evaluation sequence of 1 = 2. >>> Its infinitely recursive structure makes it neither true nor false. >> >> What is that "its" intended to refer to? According to Prolog rules >> unify_with_occurs_check(LP, not(true(LP))) is false. > > Proving that ?- LP = not(true(LP)). is infinitely recursive. There is nothing infinite there. Everything that can be in a computer's memory is finite and everthinng a computer does is done in finite time. -- Mikko