Krivine's intuitionistic proof of classical completeness (for countable languages)
The first part of the paper presents Krivine's intuitionistic version of Gödel's completeness theorem for first-order classical predicate logic [see \textit{J. L. Krivine}, Bull. Symb. Log. 2, 405--421 (1996; Zbl 0872.03004)]. The second part makes use of the ideas of Krivine's proof to derive intuitionistically some suitable variants of the two following classical theorems: the Ultrafilter Theorem for countable Boolean algebras and the Maximal Ideal Theorem for countable rings.
scientific article; zbMATH DE number 2117326