XPost: comp.theory, comp.ai.philosophy, comp.software-eng   
   XPost: sci.math   
   From: polcott333@gmail.com   
      
   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.   
      
      
   --   
   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-DOS v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)