Gödel’s completeness theorem states that a first order formula is derivable if and only if it is valid, where a formula is valid if it is true (ā la Tarksi) in every model. Unfortunately Gödel’s proof and the more commonly presented proof by Henkin are not constructive. I suspected that there was no constructive proof of the completeness of classical first order logic.
Today, I found this wonderful paper, “Krivine Intuitionistic Proof Of Classical Completeness (for countable languages)” which says that Gödel showed that there can be no constructive proof of the completness theorem.
However, there is an out. If we change the definition of validity slightly so that a formula is valid if it holds in all models including the empty model, then the completeness theorem is constructively provable! Since the empty model witnesses all statements this modified definition of validity is classically equivalent to the original definition. I would say that the definition of validity that admits the empty model is more natural anyway.