[HN Gopher] Peano arithmetic is enough, because Peano arithmetic...
       ___________________________________________________________________
        
       Peano arithmetic is enough, because Peano arithmetic  encodes
       computation
        
       Author : btilly
       Score  : 6 points
       Date   : 2025-06-13 16:10 UTC (6 hours ago)
        
 (HTM) web link (math.stackexchange.com)
 (TXT) w3m dump (math.stackexchange.com)
        
       | btilly wrote:
       | This is a stack overflow question that I turned into a blog post.
       | 
       | It covers both the limits of what can be proven in the Peano
       | Axioms, and how one would begin bootstrapping Lisp in the Peano
       | Axioms. All of the bad jokes are in the second section.
       | 
       | Corrections and follow-up questions are welcome.
        
         | Cheyana wrote:
         | Thanks for this. In another strange internet coincidence, I was
         | asking ChatGPT to break down the fundamentals of the Peano
         | axioms just yesterday and now I see this. Thumbs up!
        
         | entaloneralie wrote:
         | What did you refer to when you said Prelude? I'm familiar with
         | the concept of preludes in PL, but anything specifically that
         | related to lisp bootstrapping from PA?
        
       | dooglius wrote:
       | The interesting part to me (I have a background in both
       | math+programming) isn't so much the encoding of computation but
       | that one can work around the independence of goodstein's theorem
       | in this self-referential way. I think this implies that PA+"PA is
       | omega-consistent" can prove goodstein's theorem, and perhaps can
       | more generally do transfinite induction up to epsilon_0?
        
       ___________________________________________________________________
       (page generated 2025-06-13 23:02 UTC)