Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT

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