I had originally found myself very confused by how the second order axiom of induction restricted PA to a single model, leading to this discussion where I thought doing so would violate the incompleteness theorem.
What I misunderstood is that while the axiom schema of induction effectively quantifies over properties definable in PA, the SOL version quantifies over ALL properties, including those you can't even define in PA.
This seems like a really subtle point that wasn't obvious to me from the article, knowing FOL but not SOL. I actually realized my mistake when I saw that Eliezer was representing properties as sets in the visual diagram.
Anyway, I thought others might benefit by learning from my mistake. Also, I'd like to point out that this definition of the natural numbers yields no procedure that lets you produce theorems of PA as second-order logic has no computable complete definition of provability. Just use the axiom schema of induction instead of the second order axiom of induction and you will be able to produce theorems though.
Thanks, can you recommend a textbook for this stuff? I've mostly been learning off Wikipedia.
I can't find a textbook on logic in the lesswrong textbook list.
I'm a fan of Enderton's "A Mathematical Introduction to Logic". It's short and very precisely written, which can make it a little difficult to learn from on its own, but together with a general familiarity with the subject and using wikipedia for additional examples elaboration, it should be perfect.