Hugo Herbelin (INRIA), Computing with Gödel’s completeness theorem: Weak Fan Theorem, Markov’s Principle and Double Negation Shift in action



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:

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.