# 22.9 Constructive Zermelo's Problem

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$$.