Henrik Forssell: Constructive completeness and exploding models

We present a unifying categorical approach, based on Joyal's completeness theorem, that proves constructive completeness theorems for classical and intuitionistic first order logic, as well as for the coherent fragment. We show that the notion of exploding structure introduced by Veldman in 1976 is adequate for certain fragments of first-order logic and that Veldman's modified Kripke semantics arises, as a consequence, as the semantics of a suitable sheaf topos. The proof, as that of Veldman's, makes use of the fan theorem. This raises the question of how far one can get in proving completeness constructively but without using the fan theorem. We show that the disjunction-free fragment is constructively complete without appeal to the fan theorem, and also without placing restrictions on the decidability of the theories and the size of the language. Along the way we show how the completeness of Kripke semantics for the disjunction free fragment is equivalent, over IZF, to the Law of Excluded middle. (This is joint work with Christian Espíndola.)