XPost: comp.theory   
   From: polcott333@gmail.com   
      
   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()   
      
   > the value of Prov('G') must be determinable. The value of G must be   
   > either true or false, so even if it is not given or determinable it is   
   > possible to evaluate the expression for both values. If the result is   
   > the same then that is the value of the expression, otherwise the given   
   > information is insufficient.   
   >   
   >> LP := ~True(LP)   
   >   
   > That is a definition. THe purpose of a definition is not to specify a   
   > truth value. Languages that permit definitions the use of the same LP   
   > on both sides of := is usually a syntax error.   
   >   
      
      
   --   
   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)