XPost: comp.theory, comp.software-eng, sci.logic   
   XPost: sci.math   
   From: mikko.levanto@iki.fi   
      
   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.   
   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.   
      
   --   
   Mikko   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)