By the way, just to note something about the last discussion on topology. It makes me wonder what a 1st-order axiomatization might look like, which one might reasonably believe is robust and not subject to set-theoretic opinion.
Just like ACA is a reasonable axiomatization of ℕ that captures the 2nd-order induction better than PA.