Gödel’s completeness connects Tarski semantics and provability. It is a key theorem of logic.

Its constructive contents started to be studied in minimal classical logic in the 90’s by Krivine [K] with a concrete presentation of the computational content of Henkin’s proof obtained in [HI].

The reverse mathematics of completeness in constructive logic says that the theoretical strength of the completeness theorem depends on the connective one considers [BV]. For instance, it can be shown that if the logic contains a connective false itself interpreted as falsity in the semantics, then completeness implies Markov’s principle.

It is also folklore that completeness in the presence of disjunction is equivalent to some formulation of Fan theorem.

On another side, McCarty and Espíndola have studied the strength of completeness for arbitrary theories, showing that excluded-middle (EM) can be proved [MC] using non recursive theories or the existence of a boolean prime ideal (BPI) can also be proved [E].

The first objective of the internship is to clarify the existing knowledge into an organised way to eventually produce a synthetic paper on the constructive proof-theoretic strength of Gödel’s theorem in the presence of various connectives, isolating the various ingredients which lead to infer EM or BPI. So to speak, this is about constructive reverse mathematics.

In a second step, a constructive content will be given to Markov’s principle, which is well known, and to Fan theorem, which is less well-known (an approach is to inherit from the constructive contents of the classical axiom of dependent choice, using either realizability as in Berger-Oliva’s [BO], or a direct style proof interpretation as in [H]). From that, an algorithm to extract proofs of provability from proofs of validity will be obtained for the full standard set of connectives.

Bibliography

• [BO] Ulrich Berger and Paolo Oliva, Modified Bar Recursion and Classical Dependent Choice, Logic Colloquium’01, 2005.
• [BV] Stefano Berardi and Silvio Valentini, Krivine’s intuitionistic proof of classical completeness (for countable languages). Ann. Pure Appl. Logic , 129(1-3):93–106, 2004.
• [K] Jean-Louis Krivine, Une preuve formelle et intuitionniste du théorème de complétude de la logique classique. Bulletin of Symbolic Logic , 2(4):405–421, 1996.
• [E] Christian Espíndola, Semantic Completeness of First-Order Theories in Constructive Reverse Mathematics, Notre Dame Journal of Formal Logic, volume 57(2), 2016.
• [H] Hugo Herbelin, A constructive proof of dependent choice, compatible with classical logic, LICS, 2012.
• [HI] Hugo Herbelin, Danko Ilik, An analysis of the constructive content of Henkin’s proof of Gödel’s completeness theorem, 2016.

This document was translated from L^AT_EX by H^EV^EA.