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.