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)

[0] https://en.wikipedia.org/wiki/Goodstein%27s_theorem

> Piano Axioms

Quite disappointed it's just a typo...

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.

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!

Veritassium's video about it helped me a lot with understanding this idea:

https://www.youtube.com/watch?v=HeQX2HjkcNo

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.

to get well acquainted with these axioms, try playing the "natural number game": https://adam.math.hhu.de/#/g/leanprover-community/nng4

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.

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)

This is awesome, thanks for sharing. Reminds me of the NandGame[1], but for math.

[1]: https://www.nandgame.com/

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.

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

Indeed - whatever the axioms, the natural numbers will forever remain a mystery.

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

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.

* since they've posted most of https://news.ycombinator.com/from?site=principlesofcryptogra...

What would some others be? I usually only see Peano's axioms.

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.

https://en.wikipedia.org/wiki/Presburger_arithmetic

Skolem arithmetic is decidable too: https://en.wikipedia.org/wiki/Skolem_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...

I recently learned about https://en.wikipedia.org/wiki/Self-verifying_theories which gives you most of multiplication while still being decidable, which is pretty crazy.

That's cool, but where does it say it's decidable?

Not on that Wikipedia page, but you might want to have a look at the papers?

Some decidable extensions of Skolem and Presburger, searched for and found by ChatGPT: https://chatgpt.com/share/67e1d302-c930-800f-bc2a-85bdc60563...

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.

Conway's Surreal Numbers https://en.wikipedia.org/wiki/Surreal_number#Arithmetic

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.

Sure, one can, but does it help with anything? Just curious.

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