The choice function C on Rⁿ associates each X⊆Rⁿ with a chosen set C(X)⊆X. The function is called ordinal if, for any strictly monotone mapping ψ: Rⁿ→Rⁿ and every X⊆Rⁿ, it satisfies C(ψ(X))=ψ(C(X)).The article proposes and studies the method for formalization of the ordinal functions of choice on Rⁿ by means of first-order logic. All ordinal models of choice based of binary relation described in the scientific literature are researched for formalizability. For the majority of them (22 out of 28), the formalizations are constructed; for the remaining models, nonformalizability is correctly proved. Operations on choice functions (parallel and sequential composition, branching, inversion, limited feedback) are considered, and for each of them the corresponding formalization transformation is found. This allows to formalize complex hierarchical models of ordinal choice. Some problems related to the construction, simplification and minimization of formalizations, are investigated for algorithmic solvability, NP-hardness, and polynomiality, where the complexity of formalization is understood as the number of quantifiers in its prefix form.

choice function, ordinal choice, first-order logic, formalizing of ordinal choice, formalizations transformation, complexity of formalization

Mathematical problems and theory of numerical methods