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)
> The axiomatization of arithmetic provided by Peano axioms is commonly called Peano arithmetic.
(Ironically, there is no Wikipedia page for Peano Arithmetic, but presumably it can be derived axiomatically by applying the Peano Axiom Wikipedia page to the Arithmetic Wikipedia page wink emoji)
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.
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.
[0] https://en.wikipedia.org/wiki/Goodstein%27s_theorem