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.
ZFC is the universally, unequivocally best definition of a set
Worse. You are being tricked into believing that ZFC is at all a definition of a set at all, while it is just a set of restrictions on what we would tolerate.
In some sense, if you believe that there is only one second-order model of natural numbers, you have to make decisions what are the properties of natural numbers that you can range over; as Cohen has taught us, this involves making a lot of set-theoretical decisions with continuum hypothesis being only one of them.
What I got out of this post is that second-order logic is a lie.
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!
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.
Worse. You are being tricked into believing that ZFC is at all a definition of a set at all, while it is just a set of restrictions on what we would tolerate.
In some sense, if you believe that there is only one second-order model of natural numbers, you have to make decisions what are the properties of natural numbers that you can range over; as Cohen has taught us, this involves making a lot of set-theoretical decisions with continuum hypothesis being only one of them.