  An initial connection between AC and logic emerges by returning to its formulation AC3 in terms of relations, namely: any binary relation contains a function with the same domain. This version of AC is naturally expressible within a second-order language \(L\) with individual variables \(x\), \(y\), \(z\), … and function variables \(f\), \(g\), \(h\), …. In \(L\), binary relations are represented by formulas \(\phi(x, y)\) with two free individual variables \(x\), \(y\). The counterpart in \(L\) of the assertion AC3 is then