I wonder how many minds I can blow by saying that Piano Axioms (described here) isn't the same thing as Piano Arithmetic (PA, first-order axiomatic system that keeps popping up in axioms discussions - e.g. that Goodstein sequence[0] termination is unprovable in it)
Then you might want to read Douglas Hofstadter's famous "Gödel, Escher, Bach" which draws analogies between mathematics and music and in one of its playful dialogues does in fact feature things called "Piano Postulates".
(The conceit is that one of the characters in the dialogue interprets mathematical notation as music, and claims to have an immediate sense of whether any given melody is "beautiful" that in every case seems to correspond to the truth or falsehood of the proposition expressed -- but denies all awareness of any connection between these melodies and anything mathematical. He mentions in particular five short but elegant pieces called the "Piano Postulates", which are of course Peano's axioms[1]. It eventually becomes clear, though it's not stated directly, that the character in question knows perfectly well what the notation really means and is trying to pull a hoax on his interlocutor, but his bluff gets called.)
[1] Though I'm only now realising that the notation they're using isn't actually expressive enough for it to be possible to write down the induction axiom in it.
chamomeal [3 hidden]5 mins ago
I was hoping GEB would pop up in this convo somewhere!
I’ve read halfway through like three times. I wish I had a better math background so I could understand the incompleteness theorem. Seems like it’s pretty central to his ideas, but I can’t quite wrap my head around it.
Someday I’ll get all the way through!
namaria [3 hidden]5 mins ago
Veritassium's video about it helped me a lot with understanding this idea:
This post describes Peano’s Arithmetic, not Peano's axiom, even though it says the latter. Induction is a second order quantification over predicate. Just saying induction is true for all predicate is PA.
Really cool idea. I've been curious about theorem provers but never tried one out. I had a quick look at this on my phone (so, maybe not representative UI).
Some things that I think could be improved:
It tells you to click on "Tutorial world", but there is no such button. You have to click "Start" before you see it.
It doesn't tell you what "rfl" stands for.
It doesn't tell you where the "two_eq_succ_one" etc. come from. Are these axioms? Are there infinitely many of them? Are they always available in Lean or are they part of the tutorial world? Why refer to numbers with names instead of digits?
The thing where you have to type "\l" when you want a unicode arrow feels pointlessly obtuse. Why not make it "<-" or something? If humans are going to type it, it should be made out of characters typically found on keyboards.
And I stopped because I got annoyed with typing on my phone. Might try again when I get to a real computer.
EDIT: I just looked it up. "rfl" stands for "reflexivity". Also "rw" is meant to automatically do "rfl" but I think I found that I had to manually do "rfl" after "rw" in the tutorial. https://lovettsoftware.com/NaturalNumbers/Tactics.lean.html
And "two_eq_succ_one" is part of the tutorial world but there are only a small handful of them. In my opinion it is important to distinguish for newbies what is actually part of the system they're learning to use and what is merely part of their learning environment.
immibis [3 hidden]5 mins ago
Theorem providers should be treated as interactive. I don't know how Lean works but I know how Isabelle works. Reading Isabelle proofs in plain text (e.g. in the seL4 verification repository on GitHub) is completely useless. However, when you open one in Isabelle's IDE, you can click on any point in the proof and show the internal state of the verifier - what the current statement being proved is, so you can see how the last tactic modified it. You can also search for names of theorems and axioms by matching templates (e.g. "?a*(?b+?c)=?d" will match the law of distributivity and maybe some other stuff)
magicalhippo [3 hidden]5 mins ago
This is awesome, thanks for sharing. Reminds me of the NandGame[1], but for math.
Don't know why, but to me there is little that I find more interesting than axiomes in math. ZFC / Peano always fascinated me, especially in the light of Gödels incomplete theorem.
culi [3 hidden]5 mins ago
Gödel's incompleteness theorems have given mathematicians an identity crisis for nearly a century now.
I think it leads to a healthier view of mathematics in the end. Imo, it's healthy to realize that math is just an attempt at abstracting observed patterns in a way that can be extended and studied and not some fundamental principle of the universe itself
Koshkin [3 hidden]5 mins ago
Indeed - whatever the axioms, the natural numbers will forever remain a mystery.
culi [3 hidden]5 mins ago
Not sure where this HN title comes from since it's not the original but I have a gripe with the way it represents Peano's Axioms as THE building blocks of arithmetic. Instead of just one of the many attempts at coming up with a set of axioms that can serve as the building blocks of Arithmetic
dang [3 hidden]5 mins ago
I'm guessing that the submitter was also the author of the post* and decided to use a different title for HN. I've reverted it now.
What would some others be? I usually only see Peano's axioms.
xjm [3 hidden]5 mins ago
Another one is Presburger Arithmetic, which is Peano Arithmetic minus the multiplication. What makes it interesting (and useful) is that this removal makes the theory decidable.
I'm wondering whether there are decidable first-order theories about the natural numbers that are stronger than either Skolem or Presburger arithmetic, that presumably use more powerful number theory. Ask "Deep Research"?
[edit] Found something without AI help: The theory of real-closed fields is decidable, PLUS the theory of p-adically closed fields is also decidable - then combined with Hasse's Principle, this might take you beyond Skolem.
There are no specific extensions mentioned, a bunch of math symbol rendering issues, and what seems like maybe some hallucinations? Thanks for proving once again how useless chatgpt is if you're not already an expert on what you're asking it
Maybe a roundabout answer to your question, but Peano's axioms are equiconsistent with many finite set theories (even ZFC without axiom of infinity), and I do think philosophically it makes more sense to say weak axiomatic set theory + predicate calculus forms building blocks of arithmetic[1]. The idea of "number" as conceived by Frege is an equivalence class on finite sets: A ~ B <-> there is a bijection, which is in fact a good way of explaining "counting with fingers" as an especially primitive building block of arithmetic:
{index, middle, ring} ~
{apple, other apple, other other apple} ~
{1, 2, 3}
as representatives of the class "3" etc etc, predicates would be "don't include overripe apples when you count" etc. Then additions are unions and so on, and the Peano axioms are a consequence.
[1] In my view Peano axioms are the Platonic ideal of arithmetic, after the cruft of bijections and whatnot are tossed away. I agree this is splitting hairs.
There are many axiom systems for natural numbers. My favorites are 1. Heyting Arithmetic, and 2. In category theory, one can characterise the natural numbers and the initial algebra of the X |–> X+1. functor.
Koshkin [3 hidden]5 mins ago
Sure, one can, but does it help with anything? Just curious.
ketralnis [3 hidden]5 mins ago
It's up to you if you think it's "better" but it's answering the question of whether Peano axioms are the only fundamental structure
[0] https://en.wikipedia.org/wiki/Goodstein%27s_theorem
Quite disappointed it's just a typo...
(The conceit is that one of the characters in the dialogue interprets mathematical notation as music, and claims to have an immediate sense of whether any given melody is "beautiful" that in every case seems to correspond to the truth or falsehood of the proposition expressed -- but denies all awareness of any connection between these melodies and anything mathematical. He mentions in particular five short but elegant pieces called the "Piano Postulates", which are of course Peano's axioms[1]. It eventually becomes clear, though it's not stated directly, that the character in question knows perfectly well what the notation really means and is trying to pull a hoax on his interlocutor, but his bluff gets called.)
[1] Though I'm only now realising that the notation they're using isn't actually expressive enough for it to be possible to write down the induction axiom in it.
I’ve read halfway through like three times. I wish I had a better math background so I could understand the incompleteness theorem. Seems like it’s pretty central to his ideas, but I can’t quite wrap my head around it.
Someday I’ll get all the way through!
https://www.youtube.com/watch?v=HeQX2HjkcNo
Some things that I think could be improved:
It tells you to click on "Tutorial world", but there is no such button. You have to click "Start" before you see it.
It doesn't tell you what "rfl" stands for.
It doesn't tell you where the "two_eq_succ_one" etc. come from. Are these axioms? Are there infinitely many of them? Are they always available in Lean or are they part of the tutorial world? Why refer to numbers with names instead of digits?
The thing where you have to type "\l" when you want a unicode arrow feels pointlessly obtuse. Why not make it "<-" or something? If humans are going to type it, it should be made out of characters typically found on keyboards.
And I stopped because I got annoyed with typing on my phone. Might try again when I get to a real computer.
EDIT: I just looked it up. "rfl" stands for "reflexivity". Also "rw" is meant to automatically do "rfl" but I think I found that I had to manually do "rfl" after "rw" in the tutorial. https://lovettsoftware.com/NaturalNumbers/Tactics.lean.html
And "two_eq_succ_one" is part of the tutorial world but there are only a small handful of them. In my opinion it is important to distinguish for newbies what is actually part of the system they're learning to use and what is merely part of their learning environment.
[1]: https://www.nandgame.com/
I think it leads to a healthier view of mathematics in the end. Imo, it's healthy to realize that math is just an attempt at abstracting observed patterns in a way that can be extended and studied and not some fundamental principle of the universe itself
* since they've posted most of https://news.ycombinator.com/from?site=principlesofcryptogra...
https://en.wikipedia.org/wiki/Presburger_arithmetic
I'm wondering whether there are decidable first-order theories about the natural numbers that are stronger than either Skolem or Presburger arithmetic, that presumably use more powerful number theory. Ask "Deep Research"?
[edit] Found something without AI help: The theory of real-closed fields is decidable, PLUS the theory of p-adically closed fields is also decidable - then combined with Hasse's Principle, this might take you beyond Skolem.
[edit] Speculating about something else: Is there a decidable first-order theory of some aspects of analytic number theory, like Dirichlet series? That might also take you beyond Skolem. https://en.wikipedia.org/wiki/Analytic_number_theory#Methods...
[1] In my view Peano axioms are the Platonic ideal of arithmetic, after the cruft of bijections and whatnot are tossed away. I agree this is splitting hairs.