Sujet : Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT
De : polcott333 (at) *nospam* gmail.com (olcott)
Groupes : sci.logic comp.theoryDate : 29. May 2024, 14:11:02
Autres entêtes
Organisation : A noiseless patient Spider
Message-ID : <v379h7$159q4$1@dont-email.me>
References : 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32
User-Agent : Mozilla Thunderbird
On 5/29/2024 2:01 AM, Python wrote:
Le 29/05/2024 à 04:39, olcott a écrit :
...
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, Peter Olcott, are actually the one showing one's ignorance here.
Gödel theorems can be handled by more powerful proving systems such
as COQ : http://r6.ca/Goedel/goedel1.html
?- LP = not(true(L, LP)).
LP = not(true(L, LP)).
?- unify_with_occurs_check(LP, not(true(L, LP))).
false.
Richard explained this incorrectly.
let's see if you can do better.
I created Minimal Type Theory that does the same thing as
https://www.swi-prolog.org/pldoc/man?predicate=unify_with_occurs_check/2Minimal Type Theory (YACC BNF)
https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNFLP := ~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"
<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>
Directed graph of evaluation sequence of LP
Nodes on the left edges on the right
00 NOT 01
01 True 02, 00 // cycle
02 L
-- Copyright 2024 Olcott "Talent hits a target no one else can hit; Geniushits a target no one else can see." Arthur Schopenhauer