XPost: comp.theory, sci.math, sci.lang   
   From: polcott333@gmail.com   
      
   On 12/1/2025 7:13 PM, Tristan Wibberley wrote:   
   > On 29/11/2025 23:19, olcott wrote:   
   >   
   >> Gödel, Kurt 1931.   
   >> On Formally Undecidable Propositions of Principia Mathematica And   
   >> Related Systems   
   >   
   > Do you have a reference to the original and also English translation of   
   > his 1938 paper "On Formally Undecidable Propositions of Principia   
   > Mathematica And Related Systems II"?   
   >                                  ^^   
   >   
      
   Gödel, Kurt 1931.   
   On Formally Undecidable Propositions of Principia Mathematica And   
   Related Systems   
      
   https://monoskop.org/images/9/93/Kurt_G%C3%B6del_On_Formally_Und   
   cidable_Propositions_of_Principia_Mathematica_and_Related_Systems_1992.pdf   
      
      
   I never look at things in terms of their complex verbosity.   
   As a software engineer with decades of experience I boil   
   them down to their breast essence.   
      
   > His 1931 paper says he'll followup with a completed proof and   
   > generalisation to more systems - so I think that's what we have to look   
   > at to understand what people refer to as his first incompleteness proof   
   > and theorem. I've been told (albeit by a chatbot) that the title and   
   > year above is what I should look for.   
   >   
   >   
   >> If you think that I am wrong then don't fucking guess   
   >> show exactly what his sentence actually says without   
   >> the ruse of Gödel numbers in a language has its own   
   >> self-reference operator and provability operator.   
   >   
   > You've gone off the deep end there.   
   >   
      
   Maybe with the swearing, these people have proven to   
   be incorrigible, that is why I blocked half of them.   
      
   >   
   >> I say it says this:   
   >> G := (F ⊬ G) // G says of itself that it is unprovable in F   
   >   
   >   
   > It says that G is not a theorem of F, and perhaps it does so   
      
   That is short-hand.   
      
   > epitheoretically because of the use of ":=" which often nominates a   
   > substitution to apply to get an object of F, and that would /almost/   
   > trivially make it true, albeit not for all possible F.   
   >   
      
   *YACC Syntax of Olcott Minimal Type Theory*   
   https://philarchive.org/archive/PETMTT-4v2   
   I used the "defined as" operator to allow   
   direct self-reference.   
      
   > "[fact] in [a system]" conventionally can mean [fact] for all definition   
   > extensions of [a system] when mathematicians are talking because they   
   > add definitions when using the system and examine the consequences "/in/   
   > the system". The prepositions are ambiguous across specialisms, clearly.   
   >   
      
   I mean every fact that can be axiomatized in the   
   the verbal model of the actual world.   
      
   "cats"  "animals" stipulates relations between   
   finite strings Implementing Gödel's "theory of simple types"   
   in a type hierarchy of Rudolf Carnap Meaning Postulates.   
      
   https://lawrencecpaulson.github.io/papers/Russells-mathematical-logic.pdf   
   bottom of page 9   
      
   https://liarparadox.org/Meaning_Postulates_Rudolf_Carnap_1952.pdf   
      
   > There are some more ambiguities so reflecting and responding usefully on   
   > Olcott's expression is difficult and nondeterministic.   
   >   
      
   *YACC Syntax of Olcott Minimal Type Theory*   
   https://philarchive.org/archive/PETMTT-4v2   
      
   Here I show Olcott's Minimal Type Theory and   
   Prolog side-by-side with the Clocksin & Mellish   
   showing the same infinite expansion.   
      
   % This sentence is not true.   
   ?- LP = not(true(LP)).   
   LP = not(true(LP)).   
   ?- unify_with_occurs_check(LP, not(true(LP))).   
   false.   
      
   In Olcott's Minimal Type Theory   
   LP := ~True(LP)   
   that expands to: ~True(~True(~True(~True(~True(LP)))))   
      
   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 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.   
      
      
   --   
   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)