Polynomial time uniformization and non-standard methods

This paper presents the contents of a talk given in December 1990, during the second Journées sur les Arithmétiques Faibles held at the LITP, Paris; the talk was repeated during the 1991 Ecole de Printemps of Méjannes le Clap. The paper proves a polynomial time computability result for a class of NP inter co-NP problems, for which only the obvious exponential time algorithm was known. The result is proved by a striking use of non-standard methods, and it is not clear at all how to obtain it by standard methods.