It turns out this only pushes back the problem. You can write down second-order axioms for arithmetic which have a unique model, but in a model of a second-ord

It turns out this only pushes back the problem. You can write down second-order axioms for arithmetic which have a unique model, but in a model of a second-order theory predicates are interpreted as sets. So, you need to choose a version of set theory, to know what a model actually is. Suppose you choose ZFC (the usual axioms of set theory). Unfortunately this itself has infinitely many models! I explained this in a bit more detail here: https://johncarlosbaez.wordpress.com/2016/04/02/computing-the-uncomputable/#comment-79002 https://johncarlosbaez.wordpress.com/2016/04/02/computing-th...