Completeness of first-order logic against Tarski semantics, that is Gödel's completeness theorem, has been abundantly studied in the context of classical and intuitionistic reverse mathematics in either second-order arithmetic or set theory, sometimes with inconsistent results (e.g. Krivine asserting it is fully constructive, Kreisel deriving Markov's principle, McCarty asserting it requires excluded-middle, Simpson asserting it is classically Weak Kőnig Lemma, Henkin that it is classically the Ultrafilter Theorem, etc.).

We will survey these results, sorting out the reasons for these apparently inconsistent results, eventually clarifying that completeness with respect to Tarski semantics over recursively enumerable theories intuitionistically requires:

• a purely intuitionistic (unexpected) predicative form of the Weak Fan Theorem for dealing with the underlying logical structure and the negative connectives,
• Markov's Principle for dealing with positive/additive falsity,
• a form of Double Negation Shift for dealing with positive disjunction.

Interestingly, Markov's Principle and Double Negation Shift are weakly classical principles which preserve the witness and disjunction properties, and thus, are in this sense "valid" intuitionistic principles.