XPost: sci.logic, sci.math, sci.math   
   XPost: comp.software-eng   
   From: mikko.levanto@iki.fi   
      
   On 11/01/2026 16:32, olcott wrote:   
   > On 1/11/2026 4:34 AM, Mikko wrote:   
   >> On 10/01/2026 18:19, olcott wrote:   
   >>> 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.   
   >>   
   >> Only for those where G can be constructed so that G is true if and   
   >> only if it is not provable. Such construction is prosible in Peano   
   >> arithmetic and many other systems but not in every system.   
   >   
   > Any Formal System having an unprovability operator ⊬   
   > and A := B // A [is defined as] B (self-reference operator)   
   > can reject this expression G := (F ⊬ G) as non-well-founded   
   > using Proof Theoretic Semantics.   
      
   That is a very restricted scope. For example, neither operator is in   
   the language of the first order Peano arithmetic. In addition, in   
   langages that have := don't have it as a symbol for a function or a   
   predicate but as sui generis with specific syntax rules, one of which   
   usually is that the symbol on the left side of := must not be used on   
   the right side. Therefore G := (F ⊬ G) is not in typical languages that   
   have := and ⊬.   
      
   --   
   Mikko   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)