When working with a first-order theory, it is customary to use definitions and Skolem functions to clarify the specification of the given theory; this is usual practice, for instance, in first-order theorem proving. The problem arises when trying to eliminate these extra predicates and functions because naive elimination procedures often lead to an exponential increase in the length of the proofs.

The problem of the efficient elimination of definitions in prepositional logic is a major open question in the field of proof complexity. This paper, on the one hand, introduces a procedure that allows one to eliminate definitions in polynomial time, provided that the theory is able to prove the existence of two elements in the universe.

On the other hand, the increase in proof length when eliminating Skolem functions is also an important problem in proof theory of pure first-order logic. This paper shows that Skolem functions can be efficiently eliminated, provided that the theory is strong enough to code finite functions.

The results presented in this paper, although not directed to the most general statement of the problems of elimination of definitions and Skolem functions, show that efficient procedures of elimination exist in many natural (according to the hypotheses stated above) first-order proof systems.