What I got out of this post is that second-order logic is a lie.

"The mathematicians who deny second-order logic would see that reasoning as invoking an implicit background universe of set theory. Everything you're saying makes sense relative to some particular model of set theory, which would contain possible models of Peano arithmetic as sets, and could look over those sets and pick out the smallest in that model. Similarly, that set theory could look over a proposed model for a many-sorted logic, and say whether there were any subsets within the larger universe which were missing from the many-sorted model. Basically, your brain is insisting that it lives inside some particular model of set theory. And then, from that standpoint, you could look over some other set theory and see how it was missing subsets that your theory had."

Second-order logic is how first-order set theory feels from the inside.

And now I understand (and agree with) Johnicholas' comment from the last post. ZFC is a hack, but it is a very good hack which fits with our intuitions. However, after reading this post, I think that to use second-order logic is to decieve yourself into thinking that ZFC is the universally, unequivocally best definition of a set. I'm not anywhere close to 100% confident (though I'm still well over 50%) that ZFC is even consistent!

Good question. One obvious answer is that the AI would be able to induct what you would call an infinite axiom schema, as a single axiom - a simple, finite hypothesis.

That can easily be worked around. One answer (the one I'm intimately familiar with, not necessarily the best one) is to use first-order metalogic, which proves theorem schema rather than theorems (note that most theorem schema end up isomorphic to theorems, as well). This is the approach Metamath takes, and they have created a metalogically complete axiomatization of first-order metalogic with equality, which ends up allowing ZFC to be finitely axiomatized.