Krivineʹs intuitionistic proof of classical completeness (for countable languages)

In 1996, Krivine applied Friedmanʹs A-translation in order to get an intuitionistic version of Gِdel completeness result for first-order classical logic and (at most) countable languages and models. Such a result is known to be intuitionistically underivable (see J. Philos. Logic 25 (1996) 559), but Krivine was able to derive intuitionistically a weak form of it, namely, he proved that every consistent classical theory has a model. In this paper, we want to analyze the ideas Krivineʹs remarkable result relies on, ideas which where somehow hidden by the heavy formal machinery used in the original proof. We show that the ideas in Krivineʹs proof can be used to intuitionistically derive some (suitable variants of) crucial mathematical results, which were supposed to be purely classical up to now: the Ultrafilter Theorem for countable Boolean algebras, and the maximal ideal theorem for countable rings.