XPost: comp.theory, sci.math, sci.lang   
   From: polcott333@gmail.com   
      
   On 12/1/2025 11:37 AM, Tristan Wibberley wrote:   
   > On 29/11/2025 20:51, olcott wrote:   
   >   
   >> Try and show how Gödel incompleteness can be   
   >> specified in a language that can directly encode   
   >> self-reference and has its own provability operator   
   >> without hiding the actual semantics using Gödel numbers.   
   >   
   > An outline how I'd go about this kind of thing (not complete by far, and   
   > also not checked properly, though I have thought about it a bit). I've   
   > done this about Olcott's paraphrasing of Goedel's outline in PM rather   
   > than the challenge stated above because Goedel's system P is weird and I   
   > don't trust it at all. IMPORTANT! Goedels outline and Olcott's   
   > paraphrase use a self-referential definition rather than universal   
   > quantification! I'll have to cogitate more to waffle about that.   
   >   
   > Note, it involves a formal system /extension/ rather than an /episystem/   
   > and that's how we may interpret the challenge to do our task "in [the]   
   > language".   
   >   
   > Thinking about it a touch more carefully than before, assuming Olcott   
   > very carefully formulated his G definition (I think F is nothing to do   
   > with Goedel's system P, but is more akin to a modernisation of PM  which   
   > goedel used for his similar outline). Note I have this time interpreted   
   > F to refer to a basic system rather than the definition extension that I   
   > previously supposed. This way we have a few points in the space of   
   > systems to reason more clearly with.   
   >   
   > You have to take this all with a pinch of salt, we're using ":=" and it   
   > will take some formalisation which I'm not doing (and so will |/-).   
   >   
   >   
   > Then consider Olcott's paraphrasing   
   >   
   > G := (F |/- G)   
   >   
   > The above must be an axiom of a definition extension I'll call "I" that   
   > also adjoins G and I to the objects of F and we'll assume we've already   
   > formalised extension within F. I'll call the resulting extended system   
   > "I(F)" and suppose that's the form by which statements in F may name a   
   > system "F" extended by I.   
   >   
   > In that case I(F) is consistent: G is not derived of F.   
   >   
   > We'd have a problem if I use a definition extension "J" that adjoins,   
   > instead, objects G and J and an axiom   
   >   
   > G := (J(F) |/- G).   
   >   
   > "J(F)" names what I assumed Olcott had meant "F" to name previously. I   
   > kind-of-conjecture that J(F) is contradictory because it seems obvious   
   > that we can derive both |- G and |/- G which is how we'll recognise   
   > contradiction. I hesitate to use the term "inconsistent" because I don't   
   > trust the concept having found "indiscriminate" to be satisfactory and   
   > more general for simpler systems.   
   >   
   >   
   > Having drawn a very faint line on a block of stone before spending eons   
   > carving and polishing and looking up to see what it took to do so   
   > little, it is obvious why Olcott has not been swayed by the   
   > conversations in these newsgroups.   
   >   
      
   I have not been swayed because there have been no   
   actual rebuttals on the basis of actual correct   
   reasoning. Most all of the rebuttals have been   
   some form of "we really really don't believe you".   
      
   Here is Prolog directly showing how Pathological   
   self-reference(Olcott 2004) make an expression   
   semantically unsound.   
      
   % This sentence is not true.   
   ?- LP = not(true(LP)).   
   LP = not(true(LP)).   
   ?- unify_with_occurs_check(LP, not(true(LP))).   
   false.   
      
   % This sentence cannot be proven in F   
   ?- G = not(provable(F, G)).   
   G = not(provable(F, G)).   
   ?- unify_with_occurs_check(G, not(provable(F, G))).   
   false.   
      
   BEGIN:(Clocksin & Mellish 2003:254)   
   Finally, a note about how Prolog matching sometimes differs from the   
   unification used in Resolution. Most Prolog systems will allow you to   
   satisfy goals like:   
      
   equal(X, X).   
   ?- equal(foo(Y), Y).   
      
   that is, they will allow you to match a term against an uninstantiated   
   subterm of itself. In this example, foo(Y) is matched against Y,   
   which appears within it. As a result, Y will stand for foo(Y), which is   
   foo(foo(Y)) (because of what Y stands for), which is foo(foo(foo(Y))),   
   and so on. So Y ends up standing for some kind of infinite structure.   
   END:(Clocksin & Mellish 2003:254)   
      
   This is the same as Olcott's Minimal Type Theory   
   LP := ~True(LP) // LP is defined as ~True(LP)   
   this expands to ~True(~True(~True(~True(~True(~True(...))))))   
      
   --   
   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)