5 ms·

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

by btilly 1y ago

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.

ikrima 1y ago
Hey! This is fantastic and actually ties in some very high disparate parts of math. Basically, reorient & reformulate all of math/epistomology around discrete sampling the continuum. Invert our notions of Aleph/Beth/Betti numbers as some sort of triadic Grothendieck topoi that encode our human brain's sensory instruments that nucleate discrete samples of continuum of reality (ontology) Then every modal logic becomes some mapping of 2^(N) to some set of statements. The only thing that matters is how predictive they are with some sort of objective function/metric/measure but you can always induce an "ultra metric" around notions of cognitive complexity classes i.e. your brain is finite and can compute finite thoughts/second. Thus for all cognition models that compute some meta-logic around some objective F, we can motivate that less complex models are "better". There comes the ultra measure to tie disparate logic systems. So I can take your Peano Axioms and induce a ternary logic (True, False, Maybe) or an indefinite-definite logic (True or something else entirely). I can even induce bayesian logics by doing power sets of T/F. So a 2x2 bayesian inference logic: (True Positive, True Negative, False Positive, False Negative) Fun stuff! Edit: The technical tldr that I left out is unification all math imho: algebraic topology + differential geometry + tropical geometry + algebraic analysis. D-modules and Microlocal Calculus from Kashiwara and the Yoneda lemma encode all of epistemology as relational: either between objects or the interaction between objects defined as collision less Planck hyper volumes. basically encodes the particle-wave duality as discrete-continuum and all of epistemology is Grothendieck topoi + derived categories + functorial spaces between isometry of those dual spaces whether algebras/coalgebra (discrete modality) or homologies/cohomologies (continuous actions) Edit 2: The thing that ties everything together is Noether's symmetry/conserved quantities which (my own wild ass hunch) are best encoded as "modular forms", arithmetic's final mystery. The continuous symmetry I think makes it easy to think about diffeomorphisms from different topoi by extracting homeomorphisms from gauge invariant symmetries (in the discrete case it's a lattice, but in the continuous we'd have to formalize some notion of liquid or fluid bases? I think Kashiwara's crystal bases has some utility there but this is so beyond my understanding )
- ricardobeat 1y ago
  > Invert our notions of Aleph/Beth/Betti numbers as some sort of triadic Grothendieck topoi that encode our human brain's sensory instruments that nucleate discrete samples of continuum of reality (ontology) There’s probably ten+ years of math education encoded in this single sentence?
  - ikrima 1y ago
    well, you're in luck because I'm about to make a fool of myself in trying to tease Terence Tao over at https://mathstodon.xyz/@mathemagical https://mathstodon.xyz/@mathemagical Wish me luck!
  - ikrima 1y ago
    you know what, I nerd sniped myself, here's a more fleshed out sketch of the [Discrete Continuum Bridge https://github.com/ikrima/topos.noether/blob/master/discrete-continuum-homoiconic-bridge.md#discrete-continuum-bridge https://github.com/ikrima/topos.noether/blob/master/discrete...
    - bobsh 1y ago
      There are others out here thinking along similar lines (in my case, with massive help from LLMs). Proof: https://claude.ai/share/a8128fde-ea47-4dd8-a284-16a1fd76240c https://claude.ai/share/a8128fde-ea47-4dd8-a284-16a1fd76240c . Also, I have a GitHub too: https://github.com/bobshafer/PITkit/blob/main/Links.md https://github.com/bobshafer/PITkit/blob/main/Links.md
    - gjm11 1y ago
      It seems to be entirely written by an LLM. [EDITED to add:] This is worth noting because today's LLMs really don't seem to understand mathematics very well. (This may be becoming less so with e.g. o3-pro and o4, but I'm pretty sure that document was not written by either of those.) They're not bad at pushing mathematical words around in plausible-looking ways; they can often solve fairly routine mathematical problems, even ones that aren't easy for humans who unlike the LLMs haven't read every bit of mathematical writing produced to date by the human race; but they don't really understand what they're doing, and the nature of the mistakes they make shows that. (For the avoidance of doubt, I am not making the tired argument that of course LLMs don't understand anything, they're just pattern-matching, something something stochastic parrots something. So far as I can tell it's perfectly possible that better LLMs, or other near-future AI systems that have a lot in common with LLMs or are mostly built out of LLMs, will be as good at mathematics as the best humans are. I'm just pretty sure that they're still some way off.) (In particular, if you want to say "humans also don't really understand mathematics, they just push words and symbols around, and some have got very good at it", I don't think that's 100% wrong. Cf. the quotation attributed to John von Neumann: "Young man, in mathematics you don't understand things, you just get used to them." I don't think it's 100% right either, and some of the ways in which some humans are good at mathematics -- e.g., geometric intuition, visualization -- match up with things LLMs aren't currently good at. Anyway, I know of no reason why AI systems couldn't be much better at mathematics than the likes of Terry Tao, never mind e.g. me, but they aren't close enough to that yet for "hey, ChatGPT, please evaluate my speculation that we should be unifying continuous and discrete mathematics via topoi in a way that links aleph, beth and Betti numbers and shows how our brains nucleate discrete samples of continuum reality" to produce output that has value for anything other than inspiration.)
Cheyana 1y ago
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!
- burnt-resistor 1y ago
  I suspect in the near future (if not already) ChatGPT data will be sold to data brokers and bough by Amazon such that writing a prompt will end up polluting Alexa product recommendations within a few minutes to hours.
  - lmpdev 1y ago
    Oh for fuck sake Can we not ruin every technology we develop with ads?
    - ccppurcell 1y ago
      Watch Adam Curtis Century of the Self. I don't think he set out to explain ads in tech, but to my mind it answers a lot about how ads specifically came to power.
      - blipvert 1y ago
        Might be of interest - new AC series: https://www.theguardian.com/tv-and-radio/2025/jun/14/shifty-review-adam-curtis-new-show-bbc-iplayer https://www.theguardian.com/tv-and-radio/2025/jun/14/shifty-...
    - brookst 1y ago
      Let’s also not ruin every discussion with speculation about how someone will eventually ruin everything with ads.
    - smoyer 1y ago
      We need to make ads cost more than they are worth - here's one small way (what are others?): https://adnauseam.io/ https://adnauseam.io/
deleted 1y ago
[deleted]
deleted 1y ago
[deleted]
anthk 1y ago
Boot sector Lisp bootstraps itself. https://justine.lol/sectorlisp2/ https://justine.lol/sectorlisp2/ Also, lots of Lisp from https://t3x.org https://t3x.org implement numerals (and the rest of stuff) from cons cells and apply/eval: 'John McCarthy discovered an elegant self-defining way to compute the above steps, more commonly known as the metacircular evaluator. Alan Kay once described this code as the "Maxwell's equations of software". Here are those equations as implemented by SectorLISP: ASSOC EVAL EVCON APPLY EVLIS PAIRLIS ' Ditto with some Forths. Back to T3X, he author has Zenlisp where the meta-circular evaluation it's basically how to define eval/apply and how to they ared called between themselves in a recursive way. http://t3x.org/zsp/index.html http://t3x.org/zsp/index.html
- btilly 1y ago
  I knew that this sort of stuff was possible, but it is fun to see it. When it comes to bootstrapping a programming language from nothing, the two best options are Lisp and Forth. Of the two, I find Lisp easier to understand.
doodlebugging 1y ago
After putting on my boots and wading through all of that I think that you have one edit to make. In the "Why Lisp?" section there is a bit of basic logic defined. The first of those functions appears to have unbalanced parentheses. >(defun not (x) > (if x > false > true) I have a compulsion that I can't control when someone starts using parentheses. I have to scan to see who does what with who. You later say in the same section >But it is really easy to program a computer to look for balanced parentheses Okay. This is pretty funny. Thanks for the laugh. I realize that you weren't doing that but it still is funny that you pointed out being able to do it. This later comment in the "Basic Number Theory" section was also funny. >; After a while, you stop noticing that stack of closing parens. I really enjoyed reading this post. Great job. Though it has been a long time since I did anything with Lisp I was able to walk through and get the gist again.
- kazinator 1y ago
  > I have to scan to see who does what with who. Are you saying that parentheses introduce the problem of having to scan to see what goes with what? As in, if we don't have parentheses, but still have recursive/nested structure, we don't have to scan?
  - Retr0id 1y ago
    Python block indentation is an example of nested structure that's at least easier to visually scan. You don't need to count opening/closing parens, just look down a column of text - assuming nobody mixed tabs and spaces. (but I wouldn't go as far as saying you don't need to scan it)
    - User23 1y ago
      Canonically indented Lisp reads an awful lot like Python. You don’t read the braces, you read the indentation.
  - doodlebugging 1y ago
    For myself the issue goes back to my college mathematics courses, especially differential equations. I worked those homework problems by hand on a large format tablet, roughly 24" x 36", carefully laying them out step by step so that I could walk through them in the future and make sense of the solution process. Counting and matching parentheses was pretty critical since a missed parenthesis may not pop out at you like it would in a compiler error or by walking through code. I automatically count and match even today, 40 years later.
Timwi 1y ago
> Corrections and follow-up questions are welcome. There are two places where you accidentally wrote “omega” instead of “\omega”.
- btilly 1y ago
  Thanks! I am away from my computer for the day, but I will fux it later.
  - gjm11 1y ago
    > I will fux it later I think the problem is that it's already fuxed.
- btilly 1y ago
  It is now fixed. :-)
edanm 1y ago
This is fascinating! I haven't read much past the intro yet, but I find the whole premise that you can prove all specific instances of Goodstein sequences terminate at 0 within PA, but not that all sequences terminate (it's a trivial result but still interesting). I also find it super weird that Peano axioms are enough to encode computation. Again, this might be trivial if you think about it, but that's one self-referential layer more than I've thought about before. One question for you btilly - oddly enough, I just recently decided to learn more Set Theory, and actually worked on an Intro to Set Theory textbook up to Goodstein sequences just last week. I'm a bit past that. Do you have a good recommendation for a second, advanced Set Theory textbook? Also, any recommendation for a textbook that digs into Peano arithmetic? (My mini goal since learning the proof for Goodstein sequences is to work up to understanding the proof that Peano isn't strong enough to prove Goodstein's theorem, though I'll happily take other paths instead if they're strongly recommended.)
- btilly 1y ago
  My apologies for having missed this request. I don't have good suggestions for a good set theory textbook. Grad school was 30 years ago, and I didn't specialize in logic. The best set theory book that I read was https://www.amazon.com/Naive-Theory-Undergraduate-Texts-Mathematics/dp/0387900926 https://www.amazon.com/Naive-Theory-Undergraduate-Texts-Math.... But that one is aimed at people who want to go into math but do not wish to specialize in set theory, and not at people who want to actually learn set theory.
  - edanm 1y ago
    Thanks! I read through a bunch of that textbook when I first decided to learn more maths a few years ago, but I relatively quickly started dual-reading a different textbook ("Introduction to Set Theory" by Hrbacek and Jeck), which is a more in-depth, non-naive introduction. That's the book I'm continuing to work through now.
    - btilly 1y ago
      Then you likely know more set theory than I do!

by btilly 1y ago

ikrima 1y ago

Hey! This is fantastic and actually ties in some very high disparate parts of math. Basically, reorient & reformulate all of math/epistomology around discrete sampling the continuum. Invert our notions of Aleph/Beth/Betti numbers as some sort of triadic Grothendieck topoi that encode our human brain's sensory instruments that nucleate discrete samples of continuum of reality (ontology) Then every modal logic becomes some mapping of 2^(N) to some set of statements. The only thing that matters is how predictive they are with some sort of objective function/metric/measure but you can always induce an "ultra metric" around notions of cognitive complexity classes i.e. your brain is finite and can compute finite thoughts/second. Thus for all cognition models that compute some meta-logic around some objective F, we can motivate that less complex models are "better". There comes the ultra measure to tie disparate logic systems. So I can take your Peano Axioms and induce a ternary logic (True, False, Maybe) or an indefinite-definite logic (True or something else entirely). I can even induce bayesian logics by doing power sets of T/F. So a 2x2 bayesian inference logic: (True Positive, True Negative, False Positive, False Negative) Fun stuff! Edit: The technical tldr that I left out is unification all math imho: algebraic topology + differential geometry + tropical geometry + algebraic analysis. D-modules and Microlocal Calculus from Kashiwara and the Yoneda lemma encode all of epistemology as relational: either between objects or the interaction between objects defined as collision less Planck hyper volumes. basically encodes the particle-wave duality as discrete-continuum and all of epistemology is Grothendieck topoi + derived categories + functorial spaces between isometry of those dual spaces whether algebras/coalgebra (discrete modality) or homologies/cohomologies (continuous actions) Edit 2: The thing that ties everything together is Noether's symmetry/conserved quantities which (my own wild ass hunch) are best encoded as "modular forms", arithmetic's final mystery. The continuous symmetry I think makes it easy to think about diffeomorphisms from different topoi by extracting homeomorphisms from gauge invariant symmetries (in the discrete case it's a lattice, but in the continuous we'd have to formalize some notion of liquid or fluid bases? I think Kashiwara's crystal bases has some utility there but this is so beyond my understanding )

ricardobeat 1y ago
> Invert our notions of Aleph/Beth/Betti numbers as some sort of triadic Grothendieck topoi that encode our human brain's sensory instruments that nucleate discrete samples of continuum of reality (ontology) There’s probably ten+ years of math education encoded in this single sentence?
- ikrima 1y ago
  well, you're in luck because I'm about to make a fool of myself in trying to tease Terence Tao over at https://mathstodon.xyz/@mathemagical https://mathstodon.xyz/@mathemagical Wish me luck!
- ikrima 1y ago
  you know what, I nerd sniped myself, here's a more fleshed out sketch of the [Discrete Continuum Bridge https://github.com/ikrima/topos.noether/blob/master/discrete-continuum-homoiconic-bridge.md#discrete-continuum-bridge https://github.com/ikrima/topos.noether/blob/master/discrete...
  - bobsh 1y ago
    There are others out here thinking along similar lines (in my case, with massive help from LLMs). Proof: https://claude.ai/share/a8128fde-ea47-4dd8-a284-16a1fd76240c https://claude.ai/share/a8128fde-ea47-4dd8-a284-16a1fd76240c . Also, I have a GitHub too: https://github.com/bobshafer/PITkit/blob/main/Links.md https://github.com/bobshafer/PITkit/blob/main/Links.md
  - gjm11 1y ago
    It seems to be entirely written by an LLM. [EDITED to add:] This is worth noting because today's LLMs really don't seem to understand mathematics very well. (This may be becoming less so with e.g. o3-pro and o4, but I'm pretty sure that document was not written by either of those.) They're not bad at pushing mathematical words around in plausible-looking ways; they can often solve fairly routine mathematical problems, even ones that aren't easy for humans who unlike the LLMs haven't read every bit of mathematical writing produced to date by the human race; but they don't really understand what they're doing, and the nature of the mistakes they make shows that. (For the avoidance of doubt, I am not making the tired argument that of course LLMs don't understand anything, they're just pattern-matching, something something stochastic parrots something. So far as I can tell it's perfectly possible that better LLMs, or other near-future AI systems that have a lot in common with LLMs or are mostly built out of LLMs, will be as good at mathematics as the best humans are. I'm just pretty sure that they're still some way off.) (In particular, if you want to say "humans also don't really understand mathematics, they just push words and symbols around, and some have got very good at it", I don't think that's 100% wrong. Cf. the quotation attributed to John von Neumann: "Young man, in mathematics you don't understand things, you just get used to them." I don't think it's 100% right either, and some of the ways in which some humans are good at mathematics -- e.g., geometric intuition, visualization -- match up with things LLMs aren't currently good at. Anyway, I know of no reason why AI systems couldn't be much better at mathematics than the likes of Terry Tao, never mind e.g. me, but they aren't close enough to that yet for "hey, ChatGPT, please evaluate my speculation that we should be unifying continuous and discrete mathematics via topoi in a way that links aleph, beth and Betti numbers and shows how our brains nucleate discrete samples of continuum reality" to produce output that has value for anything other than inspiration.)

Cheyana 1y ago

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!

burnt-resistor 1y ago
I suspect in the near future (if not already) ChatGPT data will be sold to data brokers and bough by Amazon such that writing a prompt will end up polluting Alexa product recommendations within a few minutes to hours.
- lmpdev 1y ago
  Oh for fuck sake Can we not ruin every technology we develop with ads?
  - ccppurcell 1y ago
    Watch Adam Curtis Century of the Self. I don't think he set out to explain ads in tech, but to my mind it answers a lot about how ads specifically came to power.
    - blipvert 1y ago
      Might be of interest - new AC series: https://www.theguardian.com/tv-and-radio/2025/jun/14/shifty-review-adam-curtis-new-show-bbc-iplayer https://www.theguardian.com/tv-and-radio/2025/jun/14/shifty-...
  - brookst 1y ago
    Let’s also not ruin every discussion with speculation about how someone will eventually ruin everything with ads.
  - smoyer 1y ago
    We need to make ads cost more than they are worth - here's one small way (what are others?): https://adnauseam.io/ https://adnauseam.io/

deleted 1y ago

[deleted]

deleted 1y ago

[deleted]

anthk 1y ago

Boot sector Lisp bootstraps itself. https://justine.lol/sectorlisp2/ https://justine.lol/sectorlisp2/ Also, lots of Lisp from https://t3x.org https://t3x.org implement numerals (and the rest of stuff) from cons cells and apply/eval: 'John McCarthy discovered an elegant self-defining way to compute the above steps, more commonly known as the metacircular evaluator. Alan Kay once described this code as the "Maxwell's equations of software". Here are those equations as implemented by SectorLISP: ASSOC EVAL EVCON APPLY EVLIS PAIRLIS ' Ditto with some Forths. Back to T3X, he author has Zenlisp where the meta-circular evaluation it's basically how to define eval/apply and how to they ared called between themselves in a recursive way. http://t3x.org/zsp/index.html http://t3x.org/zsp/index.html

btilly 1y ago
I knew that this sort of stuff was possible, but it is fun to see it. When it comes to bootstrapping a programming language from nothing, the two best options are Lisp and Forth. Of the two, I find Lisp easier to understand.

doodlebugging 1y ago

After putting on my boots and wading through all of that I think that you have one edit to make. In the "Why Lisp?" section there is a bit of basic logic defined. The first of those functions appears to have unbalanced parentheses. >(defun not (x) > (if x > false > true) I have a compulsion that I can't control when someone starts using parentheses. I have to scan to see who does what with who. You later say in the same section >But it is really easy to program a computer to look for balanced parentheses Okay. This is pretty funny. Thanks for the laugh. I realize that you weren't doing that but it still is funny that you pointed out being able to do it. This later comment in the "Basic Number Theory" section was also funny. >; After a while, you stop noticing that stack of closing parens. I really enjoyed reading this post. Great job. Though it has been a long time since I did anything with Lisp I was able to walk through and get the gist again.

kazinator 1y ago
> I have to scan to see who does what with who. Are you saying that parentheses introduce the problem of having to scan to see what goes with what? As in, if we don't have parentheses, but still have recursive/nested structure, we don't have to scan?
- Retr0id 1y ago
  Python block indentation is an example of nested structure that's at least easier to visually scan. You don't need to count opening/closing parens, just look down a column of text - assuming nobody mixed tabs and spaces. (but I wouldn't go as far as saying you don't need to scan it)
  - User23 1y ago
    Canonically indented Lisp reads an awful lot like Python. You don’t read the braces, you read the indentation.
- doodlebugging 1y ago
  For myself the issue goes back to my college mathematics courses, especially differential equations. I worked those homework problems by hand on a large format tablet, roughly 24" x 36", carefully laying them out step by step so that I could walk through them in the future and make sense of the solution process. Counting and matching parentheses was pretty critical since a missed parenthesis may not pop out at you like it would in a compiler error or by walking through code. I automatically count and match even today, 40 years later.

Timwi 1y ago

> Corrections and follow-up questions are welcome. There are two places where you accidentally wrote “omega” instead of “\omega”.

btilly 1y ago
Thanks! I am away from my computer for the day, but I will fux it later.
- gjm11 1y ago
  > I will fux it later I think the problem is that it's already fuxed.
btilly 1y ago
It is now fixed. :-)

edanm 1y ago

This is fascinating! I haven't read much past the intro yet, but I find the whole premise that you can prove all specific instances of Goodstein sequences terminate at 0 within PA, but not that all sequences terminate (it's a trivial result but still interesting). I also find it super weird that Peano axioms are enough to encode computation. Again, this might be trivial if you think about it, but that's one self-referential layer more than I've thought about before. One question for you btilly - oddly enough, I just recently decided to learn more Set Theory, and actually worked on an Intro to Set Theory textbook up to Goodstein sequences just last week. I'm a bit past that. Do you have a good recommendation for a second, advanced Set Theory textbook? Also, any recommendation for a textbook that digs into Peano arithmetic? (My mini goal since learning the proof for Goodstein sequences is to work up to understanding the proof that Peano isn't strong enough to prove Goodstein's theorem, though I'll happily take other paths instead if they're strongly recommended.)

btilly 1y ago
My apologies for having missed this request. I don't have good suggestions for a good set theory textbook. Grad school was 30 years ago, and I didn't specialize in logic. The best set theory book that I read was https://www.amazon.com/Naive-Theory-Undergraduate-Texts-Mathematics/dp/0387900926 https://www.amazon.com/Naive-Theory-Undergraduate-Texts-Math.... But that one is aimed at people who want to go into math but do not wish to specialize in set theory, and not at people who want to actually learn set theory.
- edanm 1y ago
  Thanks! I read through a bunch of that textbook when I first decided to learn more maths a few years ago, but I relatively quickly started dual-reading a different textbook ("Introduction to Set Theory" by Hrbacek and Jeck), which is a more in-depth, non-naive introduction. That's the book I'm continuing to work through now.
  - btilly 1y ago
    Then you likely know more set theory than I do!