Deutsch English Français Italiano |
<v325l6$2pkb$3@dont-email.me> View for Bookmarking (what is this?) Look up another Usenet article |
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: Mon, 27 May 2024 09:34:14 -0500 Organization: A noiseless patient Spider Lines: 78 Message-ID: <v325l6$2pkb$3@dont-email.me> References: <v1mljr$1q5ee$4@dont-email.me> <v2b1dr$2u8oi$3@dont-email.me> <v2b9mo$1ecj9$2@i2pn2.org> <v2bb6d$308qd$2@dont-email.me> <v2bc5o$1ecj9$3@i2pn2.org> <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> MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Mon, 27 May 2024 16:34:15 +0200 (CEST) Injection-Info: dont-email.me; posting-host="458305845cd025bf1a433877c96321fe"; logging-data="91787"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+wpkwkKOQ9EOYPUxciol4F" User-Agent: Mozilla Thunderbird Cancel-Lock: sha1:O86/btC5sc5qSzT4YKPtAZ73Br4= In-Reply-To: <v324pa$2rt4$1@dont-email.me> Content-Language: en-US Bytes: 4668 On 5/27/2024 9:19 AM, Mikko wrote: > On 2024-05-27 14:15:57 +0000, olcott said: > >> On 5/27/2024 3:00 AM, Mikko wrote: <snip> >>> Users of your MTT basically need two programs: one that checks whether >>> the input is syntactiaclly correct and identifies at least one error >>> if it is not, and one that checks whether a proof (that may but need >>> not have unproven premises) is valid and identifies at least one error >>> if it is not. >>> >> >> MTT is build with YACC and LEX and outputs the XML of the >> input expression. >> >> LP := ~True(L, LP) >> >> definition_2 token="ASSIGN_ALIAS" >> | definition_2 token="IDENTIFIER" value="LP" >> | sentence_2 token="NOT" >> | | atomic_sentence_1 token="IDENTIFIER" value="True" >> | | | term_list_1 >> | | | | term_2 token="IDENTIFIER" value="L" >> | | | | term_2 token="IDENTIFIER" value="LP" >> >> Directed graph of evaulation sequence of LP >> Nodes on the left edges on the right >> 00 NOT 01 >> 01 True 02, 00 // cycle >> 02 L >> >> <definition_2 token="ASSIGN_ALIAS"> >> <definition_2 token="IDENTIFIER" value="LP"/> >> <sentence_2 token="NOT"> >> <atomic_sentence_1 token="IDENTIFIER" value="True"> >> <term_list_1> >> <term_2 token="IDENTIFIER" value="L"/> >> <term_2 token="IDENTIFIER" value="LP"/> >> </term_list_1> >> </atomic_sentence_1> >> </sentence_2> >> </definition_2> > > That is not far from useful. Much of the code could be reused for > the more useful programs mentioned above. > Minimal Type Theory (YACC BNF) https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF It correctly parses every MTT expression and translates it into XML. The directed graph shown above does the same thing as unify_with_occurs_check/2 in Prolog The SWI-Prolog implementation of unify_with_occurs_check/2 is cycle-safe and only guards against creating cycles, not against cycles that may already be present in one of the arguments. https://www.swi-prolog.org/pldoc/man?predicate=unify_with_occurs_check/2 ?- 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. -- Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius hits a target no one else can see." Arthur Schopenhauer