Christian Espíndola: The completeness of Kripke semantics in constructive reverse

We will consider in intuitionistic set theory the completeness theorem with respect to Kripke semantics and analyze its strength from the point of view of constructive reverse mathematics.

We will prove that, over intuitionistic Zermelo-Fraenkel set theory IZF, the strong completeness of the negative fragment of intuitionistic first order logic is equivalent, in the sense of interderivability, to (all instances of) the law of the excluded middle, and that the same result holds for the disjunction-free fragment.

On the other hand, we will prove that the strong completeness of full intuitionistic first order logic is equivalent, over IZF, to (all instances of) the law of the excluded middle plus the Boolean prime ideal theorem.

As a consequence, we will see that the generalization to arbitrary theories of Veldman's completeness theorem for modified Kripke semantics cannot be proved in IZF.

Finally, we will mention aspects of a joint work in progress with Henrik Forssell on the categorical analysis of modified Kripke semantics and how it could be used to derive in IZF completeness proofs for the disjunction-free fragment.