 Then \(\oR\models\theta\) essentially says that if a binary relation \(X\) relates to each \(x\in\oR\) a non-empty set \(\{y\in\oR : X(x,y\}\), then there is a function \(F\) which chooses for each \(x\in\oR\) some \(y=F(x)\) such that \(X(x,y)\). In set theory this is one of many equivalent ways of saying that the Axiom of Choice holds for (continuum size) families of subsets of \(\oR\). The basic tenet of second-order logic is that “all” properties of elements of a fixed domain exist and we can quantify over them. In set-theoretical terms this means that all subsets, definable or not, of a set of any cardinality exists and we can quantify over them. In this spirit the Axiom of Choice seems innocent and is usually accepted in the literature of second-order logic.