On Skolemization in constructive theories

In this paper a method for the replacement, in formulas, of strong quantifiers
by functions is introduced that can be considered as an alternative
to Skolemization in the setting of constructive theories. A constructive
extension of intuitionistic predicate logic that captures the notions of preorder
and existence is introduced and the method, orderization, is shown
to be sound and complete with respect to this logic. This implies an
analogue of Herbrand’s theorem for intuitionistic logic. The orderization
method is applied to the constructive theories of equality and groups.