XPost: comp.theory   
   From: polcott333@gmail.com   
      
   On 11/29/2025 4:31 AM, Mikko wrote:   
   > olcott kirjoitti 28.11.2025 klo 17.21:   
   >> On 11/28/2025 2:40 AM, Mikko wrote:   
   >>> olcott kirjoitti 27.11.2025 klo 17.48:   
   >>>> On 11/27/2025 2:17 AM, Mikko wrote:   
   >>>>> olcott kirjoitti 26.11.2025 klo 17.20:   
   >>>>>> On 11/26/2025 4:17 AM, Mikko wrote:   
   >>>>>>> olcott kirjoitti 14.11.2025 klo 16.49:   
   >>>>>>>> On 11/14/2025 3:09 AM, Mikko wrote:   
   >>>>>>>>> On 2025-11-14 00:56:17 +0000, Tristan Wibberley said:   
   >>>>>>>>>   
   >>>>>>>>>> On 13/11/2025 09:05, Mikko wrote:   
   >>>>>>>>>>> On 2025-11-12 14:45:34 +0000, olcott said:   
   >>>>>>>>>>>   
   >>>>>>>>>>>> ... formalized in Minimal   
   >>>>>>>>>>>> Type Theory as LP := ~True(LP).   
   >>>>>>>>>>>> (where A := B means A is defined as B).   
   >>>>>>>>>>>>   
   >>>>>>>>>>>> https://philpapers.org/rec/OLCREO   
   >>>>>>>>>>>>   
   >>>>>>>>>>>> Can someone review my actual reasoning   
   >>>>>>>>>>>> elaborated in the paper?   
   >>>>>>>>>>>   
   >>>>>>>>>>> If you want to use the term "formal language" you must prove   
   >>>>>>>>>>> that   
   >>>>>>>>>>> there is a Turing machine that can determine whether a string   
   >>>>>>>>>>> is a   
   >>>>>>>>>>> valid sentence of your language. If no such Turing machine   
   >>>>>>>>>>> exists   
   >>>>>>>>>>> you have no justifiction for the use of the word "formal".   
   >>>>>>>>>>   
   >>>>>>>>>> It looks, at a glance, like his system has no theorems with   
   >>>>>>>>>> loops in   
   >>>>>>>>>> them. The system is "safe" and very small.   
   >>>>>>>>>   
   >>>>>>>>> It does not look small. It seems to have very many postulates,   
   >>>>>>>>> perhaps   
   >>>>>>>>> infinitely many. The intent is that it be complete so it   
   >>>>>>>>> probably is   
   >>>>>>>>> only paraconsistent or perhaps even inconsistent.   
   >>>>>>>>>   
   >>>>>>>>   
   >>>>>>>> My system rejects expressions of language that cannot   
   >>>>>>>> possibly be resolved to a truth value because they have   
   >>>>>>>> pathological self-reference(Olcott 2004)   
   >>>>>>>>   
   >>>>>>>> G ↔ ¬Prov(⌜G⌝)   
   >>>>>>>   
   >>>>>>> That can be evaluated ir sufficient defitions are given. In   
   >>>>>>> particular,   
   >>>>>>   
   >>>>>> Directed Graph of evaluation sequence   
   >>>>>> 00 ↔               01 02   
   >>>>>> 01 G   
   >>>>>> 02 ¬               03   
   >>>>>> 03 Prov            04   
   >>>>>> 04 Gödel_Number_of 01  // cycle   
   >>>>>>   
   >>>>>> ?- G = not(provable(F, G)).   
   >>>>>> G = not(provable(F, G)).   
   >>>>>> ?- unify_with_occurs_check(G, not(provable(F, G))).   
   >>>>>> false.   
   >>>>>>   
   >>>>>> You do not understand the deep meaning of   
   >>>>>> unify_with_occurs_check()   
   >>>>>   
   >>>>> That you need to lie about other people indicates that you are not   
   >>>>> sure   
   >>>>> whether what you say is true but you want anyway that others   
   >>>>> believe it.   
   >>>>>   
   >>>>> Of course I do understand the meaning of unify_with_occurs_check/2. It   
   >>>>   
   >>>>   
   >>>> That is not what I said. I said the deep meaning   
   >>>   
   >>> There is no deep meaning that is not a part of the meaning.   
   >>>   
   >>   
   >> That the directly graph of the evaluation sequence   
   >> of a formal expression contains a cycle   
   >>   
   >> LP := ~True(LP)   
   >> that expands to ~True(~True(~True(~True(~True(~True(...))))))   
   >> means that it is semantically unsound.   
   >   
   > Irrelevant to the fact that there is no deep meaning that is not a part   
   > of the meaning.   
   >   
   > Also irrelevant the meaning and deep meaning of the library predicate   
   > unify_with_occurs_check/2.   
   >   
      
   unify_with_occurs_check() does not mean only the   
   Prolog doesn't like it. It means that Prolog has   
   proved that it is semantically unsound.   
      
   --   
   Copyright 2025 Olcott   
      
   My 28 year goal has been to make   
   "true on the basis of meaning" computable.   
      
   This required establishing a new foundation   
   for correct reasoning.   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)