XPost: comp.theory   
   From: mikko.levanto@iki.fi   
      
   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   
   unifies two data structures if they can be unified without creating a   
   loop that is not already in at least one of the structures to be   
   unified, or fails if a new loop would be created or the structures   
   cannot be unified.   
      
      
   For example,   
      
      unify_with_occurs_check(G, provable(G)).   
      
   fails because it would produce a loop but   
      
      H = provable(H), unify_with_occurs_check(X, H).   
      
   succeeds because the loop in X is already in H.   
      
      
   All of which is of course irrelevant to anything in my previous message.   
      
   --   
   Mikko   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)