home bbs files messages ]

Forums before death by AOL, social media and spammers... "We can't have nice things"

   sci.logic      Logic -- math, philosophy & computationa      262,912 messages   

[   << oldest   |   < older   |   list   |   newer >   |   newest >>   ]

   Message 262,440 of 262,912   
   olcott to Mikko   
   =?UTF-8?Q?Re=3A_Boiling_G=C3=B6del=27s_1   
   10 Jan 26 10:19:51   
   
   XPost: sci.math, comp.theory, sci.math.symbolic   
   From: polcott333@gmail.com   
      
   On 1/10/2026 3:25 AM, Mikko wrote:   
   > On 08/01/2026 16:18, olcott wrote:   
   >> On 1/8/2026 4:21 AM, Mikko wrote:   
   >>> On 07/01/2026 15:06, olcott wrote:   
   >>>> On 1/7/2026 6:10 AM, Mikko wrote:   
   >>>>> On 06/01/2026 16:02, olcott wrote:   
   >>>>>> On 1/6/2026 7:23 AM, Mikko wrote:   
   >>>>>>> On 06/01/2026 02:24, Oleksiy Gapotchenko wrote:   
   >>>>>>>> Just an external observation:   
   >>>>>>>>   
   >>>>>>>> A lot of tech innovations in software optimization area get   
   >>>>>>>> discarded from the very beginning because people who work on   
   >>>>>>>> them perceive the halting problem as a dogma.   
   >>>>>>>   
   >>>>>>> It is a dogma in the same sense as 2 * 3 = 6 is a dogma: a provably   
   >>>>>>> true sentence of a certain theory.   
   >>>>>>>   
   >>>>>>   
   >>>>>> ...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   
   >>>>>>   
   >>>>>> F ⊢ G_F ↔ ¬Prov_F (⌜G_F⌝)   
   >>>>>> "F proves that: G_F is equivalent to   
   >>>>>> Gödel_Number(G_F) is not provable in F"   
   >>>>>> https://plato.stanford.edu/entries/goedel-incompleteness/   
   >>>>>> #FirIncTheCom   
   >>>>>>   
   >>>>>> Stripping away the inessential baggage using a formal   
   >>>>>> language with its own self-reference operator and   
   >>>>>> provability operator (thus outside of arithmetic)   
   >>>>>>   
   >>>>>> G := (F ⊬ G)   // G asserts its own unprovability in F   
   >>>>>>   
   >>>>>> A proof of G in F would be a sequence of inference   
   >>>>>> steps in F that prove that they themselves do not exist.   
   >>>>>   
   >>>>>  From the way G is constructed it can be meta-proven that either   
   >>>>   
   >>>> Did you hear me stutter ?   
   >>>> A proof of G in F would be a sequence of inference   
   >>>> steps in F that prove that they themselves do not exist.   
   >>>   
   >>> An F where such sequence really exists then in that F both G and   
   >>> the negation of G are provable.   
   >>>   
   >> G := (F ⊬ G)   // G asserts its own unprovability in F   
   >>   
   >> A proof of G in F would be a sequence of inference   
   >> steps in F that prove that they themselves do not exist.   
   >> Does not exist because is contradicts itself.   
   >   
   > That conclusion needs the additional assumption that F is consistent,   
   > which requires that the first order Peano arithmetic is consistent.   
      
   It remains true for any proof system that does not   
   contradict itself.   
      
   > If F is not consistent then both G and its negation are provable in F.   
   > The first order Peano arithmetic is believed to be sonsistent but its   
   > consistency is not proven.   
   >   
      
   The point is that after all these years no one ever   
   bothered to notice WHY G is unprovable in F. When   
   we do that then Gödel Incompleteness falls apart.   
      
   *G is unprovable in F because its proof would contradict itself*   
   *G is unprovable in F because its proof would contradict itself*   
   *G is unprovable in F because its proof would contradict itself*   
      
      
   --   
   Copyright 2026 Olcott

              My 28 year goal has been to make
       "true on the basis of meaning expressed in language"
       reliably computable.

              This required establishing a new foundation
              --- SoupGate-Win32 v1.05        * Origin: you cannot sedate... all the things you hate (1:229/2)   

[   << oldest   |   < older   |   list   |   newer >   |   newest >>   ]


(c) 1994,  bbs@darkrealms.ca