A *choice function* over a set \(E\) is a function \(f\) that assigns to every
non-empty subset of \(E\) one of its elements (of the subset). If \(E\) is in fact a
$Σ$-structure, we say that \(f\) is *regular* if it can be defined by an
MSO[\(\Sigma\)] formula \(\varphi(X,x)\), where the first variable \(X\) refers to
subsets, and the second variable \(x\) i.e. refers to elements.

Naturally, if a $Σ$-structure admits a well-order which can be defined by
an MSO[\(\Sigma\)] formula \(\psi(x,y)\), then one can define such a choice function
\(\varphi(X,x)\) that says "I take the least element of X with respect to \(\psi\)".

The problem, originally stated in my PhD, asks if the reciprocal is true: if a $Σ$-structure \(E\) admits a regular choice function \(\varphi(X,x)\), does it necessarily also admit a regular well order \(\psi(x,y)\)?

I conjecture that it is the case. Moreover, I have also hope for a strengthened constructive version, stated as follow:

*Conjecture*: Let \(\Sigma\) be a signature. There exists a procedure that
inputs an MSO[\(\Sigma\)] formula \(\varphi(X,x)\) and outputs another one,
\(\psi(x,y)\), such that for every $Σ$-structure \(E\), if \(\varphi(X,x)\) is a
regular choice function over \(E\) then \(\psi(x,y)\) is a regular well order over
\(E\).