Controlling witnesses

This paper presents a translation which allows one to describe constructive provability (in the sense of usual mathematics) within classical first-order logic.