An intuitionistic completeness theorem for classical predicate logic (Q708927)

The completeness of intuitionistic first-order logic with respect to the corresponding class of structures can be proved via a purely intuitionistic argument establishing a connection between Beth forcing and intuitionistic validity. The author shows that a similar argument leads to an intuitionistic version of Gödel's completeness theorem for classical first-order logic.