logic - Who first proved that the second-order theory of real numbers is categorical?

The second-order theory of real numbers is obtained by taking the axioms of ordered fields and adding a (Dedekind) completeness axiom, which states that every set which has an upper bound has a least upper bound. This theory is categorical, meaning that it has a unique model upto isomorphism.

My question is, who first managed to prove this fact? Let me give a proof here, so we can be clear as to what we're talking about. Let us first define the natural numbers in our theory. A hereditary set is a set which contains x+1 whenever it contains x, and a natural number is a real number which is an element of every hereditary set containing 0. Let me show that these natural numbers satisfy the axioms of second-order Peano arithmetic.

1. To prove that 0 is a natural number, we must prove that 0 belongs to every hereditary set containing 0. That's trivial because 0 belongs to every set containing 0.




2. We must prove that whenever x is a natural number, so is x+1. Consider any hereditary set X containing 0. Then by definition of natural number, x must belong to X, and thus by definition of hereditary, x+1 must belong to X. Since X was arbitrary, x+1 belongs to every hereditary set containing 0, and thus x+1 is a natural number.




3. The fact that x+1=y+1 implies x=y follows directly from the field axioms, which are part of the second-order theory of real numbers.




4. We must prove that there exists no natural number x such that x+1=0, which in our case is equivalent to the statement that -1 is not a natural number. Well, just consider the set of all natural numbers greater than or equal to 0 (which is of course all of them, but we don't know that yet). Then this is a hereditary set containing 0, and yet -1 doesn't belong to it, so -1 is not a natural number.




5. The induction axiom says that if X contains 0 and contains x+1 whenever it contains x, then X contains all the natural numbers. But that is just saying that if X is a hereditary set containing 0, all natural numbers belong to it, which is trivial given our definition of natural number.




6. The defining axioms of addition and multiplication in Peano arithmetic follow easily from the field axioms.

Since the axioms of second-order Peano arithmetic are categorical, it follows that the sets of natural numbers in any two models of the second-order theory of real theory must be isomorphic, and thus the sets of rational numbers in the two models must also be isomorphic. (The isomorphism can be extended straightforwardly to the rational numbers.) Let’s say we have two models R and S, with sets of rational numbers Q_R and Q_S, and with the isomorphism g from Q_R to Q_S. Then let us define the map f from R to S as follows: f(x) is the least upper bound of the set g({q in Q_R: q < x}). In other words, f is the least upper bound of the Dedekind cut in Q_S which corresponds to the Dedekind cut of x in Q_R. We can easily check that f is an isomorphism, so any two models of the second-order theory of real numbers are isomorphic.

Who was the first person to write down this proof or something like it?

Any help would be greatly appreciated.

Thank You in Advance.