From: tristan.wibberley+netnews2@alumni.manchester.ac.uk   
      
   On 05/01/2026 14:20, Mikko wrote:   
   > On 05/01/2026 16:04, olcott wrote:   
   >   
   >> ...there is also a close relationship with the “liar” antinomy,14 ...   
   >> ...14 Every epistemological antinomy can likewise be used for a   
   >> similar undecidability proof...   
   >> ...We are therefore confronted with a proposition which   
   >> asserts its own unprovability. 15 … (Gödel 1931:40-41)   
   >>   
   >> Gödel, Kurt 1931.   
   >> On Formally Undecidable Propositions of   
   >> Principia Mathematica And Related Systems   
   >>   
   >> Even when Gödel directly admits that it is   
   >> as simple as that and people see that he   
   >> admitted it they still deny this.   
   >>   
   >> G := (F ⊬ G) // where A := B means A "is defined as" B   
   >>   
   >> LP := ~True(LP) // "This sentence is not true".   
   >>   
   >> The Liar Paradox is an epistemological antinomy   
   >>   
   >> epistemological antinomy   
   >> An epistemological antinomy is a fundamental,   
   >> unresolvable contradiction within human reason,   
   >> where two opposing conclusions, each supported   
   >> by seemingly valid arguments, appear equally true.   
   >   
   > For most peopple who care at all onlh care about the result and only   
   > to the extent that that they don't try the impossible. Some people   
   > want to understand Gödel's proof or some other proof but for most of   
   > them understanding one proof is enough. Usual alternative proofs are   
   > fairly similar to the original one and only differ on some details.   
   > A significantly simpler proof would be interesting but only if it is   
   > a complete proof.   
      
   I've tried to figure out what is the exact theorem statement.   
      
   I've cited James R Meyer's excellent English translation (except that   
   his excellence is limited by the fact he translated Π to ∀ completely   
   unnecessarily, it /is/ the logical product over the domain of its   
   predicate isn't it? I've cut the citations short because they're long   
   text, but you can find them at   
   https://jamesrmeyer.com/ffgit/godel-original-english   
      
      
   At the end, the end of Part 3:   
      
   "The results will be stated and proved in fuller generality in a   
   forthcoming sequel."   
      
   I have found a name of the sequel via an AI - it's the same name but   
   with II at the end instead of I) and a year (1938) but I haven't found   
   the fabled generalisation. Obviously those could be hallucinations. I   
   also found a citation saying it never got published.   
      
      
   The restricted variant of the theorem for the system P with mere   
   indications of wider applicability is at the end of Part 2 although   
   there is some generality in the theorem statement if not the fuller   
   generality promised in the sequel:   
      
   "In every formal system that satisfies ... undecidable propositions   
   exist of the form x∀ F(x) ..."   
      
   "the systems that satisfy assumptions 1 and 2 include the   
   Zermelo-Fraenkel and the v. Neumann axiom systems of set theory, and ..."   
      
   Assumptions 1 and 2 appear to be:   
      
   "1. The class of axioms and the rules of inference ...   
    2. Every recursive relation ...   
   "   
      
      
   Important footnote at the end of that Part 2:   
      
   "48a: The real reason for the incompleteness inherent in all formal   
   systems of mathematics – as will be shown in Part II of this paper ..."   
      
      
   I can't tell if he means the second of the three parts in the paper or   
   the paper titled the same but for "II" instead of "I". I suspect the   
   later paper because "will be shown in Part II" doesn't make sense when   
   it's at the /end/ of Part II of the paper. I wonder if he has Part I   
   made of 3 parts and Part II was the predicted sequel.   
      
      
   IMPORTANT, the system P doesn't have a deduction rule like "If ⊢ x∀ F(x)   
   Then ⊢ F(x)" as far as I can see and it wouldn't help anyway due to the   
   way transfinitism is present. So I think what is "undecidable" is the ∀   
   quantified statement, not the apparent nonprovability statement! I also   
   deduce therefore that Gödel doesn't have the type system of PM1 (that he   
   references) which restricts forall quantifications to only "meaningful"   
   propositions, he seems to have "unrestricted generality" or "universal   
   generality". That might be an unstated assumption, even though I think   
   type theory was normal at the time due to PM1.   
      
   It's not clear to me yet whether it is the extension of inductively   
   defined theorems on the naturals to x₁∀ that is the cause of the exact   
   conclusion. Gödel mentions transfinite aspects as (I interpret) essential.   
      
    Thanks Jeff Barnet and Mike Terry for the discussion around the meaning   
   of propositions that are forall quantified, I was just pondering that in   
   PM1's introduction at the time. For other readers it's about   
   (imprecisely) "The system generates the statements in the forall   
   quantification" and "If I have a statement from the forall   
   quantification, there is a derivation for it" vs "the forall   
   quantification is derivable in the system but not necessarily the   
   statements that the forall quantification describes".   
      
      
   --   
   Tristan Wibberley   
      
   The message body is Copyright (C) 2026 Tristan Wibberley except   
   citations and quotations noted. All Rights Reserved except that you may,   
   of course, cite it academically giving credit to me, distribute it   
   verbatim as part of a usenet system or its archives, and use it to   
   promote my greatness and general superiority without misrepresentation   
   of my opinions other than my opinion of my greatness and general   
   superiority which you _may_ misrepresent. You definitely MAY NOT train   
   any production AI system with it but you may train experimental AI that   
   will only be used for evaluation of the AI methods it implements.   
      
   --- SoupGate-DOS v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)