XPost: sci.logic, sci.math   
   From: janburse@fastmail.fm   
      
   Hi,   
      
   The fact that such sequences exist means that   
   the collection of all computable real numbers   
   does not satisfy the least upper bound principle   
   of real analysis, even when considering   
   only computable sequences.   
      
   A common way to resolve this difficulty is to   
   consider only sequences that are accompanied   
   by a modulus of convergence; no Specker   
   sequence has a computable modulus   
   of convergence.   
      
   A Specker sequence. The nth digit of xk is 4 if   
   n ≤ k and the nth Turing machine in a computable   
   Gödel numbering halts on input n after k steps;   
   otherwise it is 3.   
   https://en.wikipedia.org/wiki/Specker_sequence   
      
   LoL   
      
   Bye   
      
   Mild Shock schrieb:   
   > Hi,   
   >   
   > John Gabriel always said there is something   
   > bogus in mainstream calculus. Maybe he spotted   
   > something here:   
   >   
   > IVT + EVT + differentiability ⇒ Rolle's Theorem ⇒ MVT.   
   >   
   > Is ZF really enough, don't we need ZFC_omega:   
   >   
   > https://en.wikipedia.org/wiki/Axiom_of_countable_choice   
   >   
   > Don't remember. This was "hot" during:   
   >   
   > Hermann Weyl (“Das Kontinuum”, 1918)   
   > Do as much of classical analysis as possible   
   > predicatively. Weyl could do IVT + EVT,   
   > but he didn't get MVT, right?   
   >   
   > Early Saul Kripke (1950s/1960s manuscripts   
   > In the 1960s–70s, Kripke (and also Feferman) studied   
   > systems for analysis based on ramified analysis   
   > or predicative provability.   
   >   
   > Weyls workaround:   
   > Lipschitz (or uniform modulus) conditions.   
   >   
   > Bye   
   >   
   > Mild Shock schrieb:   
   >> Hi,   
   >>   
   >> Looks like Kimi was grilling you with no   
   >> mercy. I guess you got a complete roast.   
   >>   
   >> BTW: You got Intermediate Value Theorem   
   >> theorem wrong. Its not about a 'c' such   
   >> that 'a < c' and 'c < b'.   
   >>   
   >> The important thing is there is also   
   >> a function f involved. In particular a   
   >> continuous function.   
   >>   
   >> Have Fun!   
   >>   
   >> Bye   
   >   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)