[HN Gopher] Orders of Infinity
       ___________________________________________________________________
        
       Orders of Infinity
        
       Author : matt_d
       Score  : 51 points
       Date   : 2025-05-04 17:55 UTC (5 hours ago)
        
 (HTM) web link (terrytao.wordpress.com)
 (TXT) w3m dump (terrytao.wordpress.com)
        
       | singularity2001 wrote:
       | Since we know that these hyper real numbers are well defined we
       | can teach them axiomatically to high school students the way
       | Leibniz used them (and keep the explicit construction via filters
       | to university students just like with a dedekind cut for reals)
       | 
       | Here is the axiomatic approach in Julia and Lean
       | https://github.com/pannous/hyper-lean
        
       | btilly wrote:
       | I'm not a big fan of using nonstandard analysis for this. We're
       | assuming the existence of arbitrary answers that we cannot ever
       | produce.
       | 
       | For example, which function is eventually larger than the other?
       | (1 + sin(x)) * e^x + x         (1 + cos(x)) * e^x + x
       | 
       | In the ultrafilter, one almost certainly will be larger. In fact
       | the ratio of the two will, asymptotically, approach a specific
       | limit. Which one is larger? What is the ratio? That entirely
       | depends on the ultrafilter.
       | 
       | Which means that we can accept the illusionary simplicity of his
       | axiom about every predicate P(N), and it will remain simple right
       | until we try to get a concrete and useful answer out of it.
        
         | JohnKemeny wrote:
         | I don't think that's the case. They can both _not have the
         | property that it is eventually larger than the other_.
        
           | LegionMammal978 wrote:
           | The axioms demand that either one function is eventually
           | dominated by the other, or both functions are of the same
           | order. But which of these is the case will strongly depend on
           | which subsequence you look at.
        
           | btilly wrote:
           | No, it is the case.
           | 
           | Look for the comment in the article, _after passing to a
           | subsequence if necessary_. The ultrafilter produces the
           | necessary subsequence for any question that you ask, and will
           | do so in such a way as to produce logically consistent
           | answers for any combination of questions that you choose.
           | 
           | That is why the ultrafilter axiom is a weak version of
           | choice. Take the set of possible yes/no questions that we can
           | ask as predicates, such that each answer shows up infinitely
           | often. The ultrafilter results in an arbitrary yet consistent
           | set of choices of yes/no for each predicate.
        
       ___________________________________________________________________
       (page generated 2025-05-04 23:00 UTC)