Constructive completeness and exploding models

ABSTRACT. 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 essential use of the Fan theorem, since we show that these completeness theorems are in fact equivalent to it. This raises the question of how far one can get in proving completeness constructively but without using the Fan theorem. We prove that the disjunction-free fragment is constructively complete without appealing to it, and also without placing restrictions on the decidability of the theories and the size of the language, while the latter is a fundamental constraint in the general case when working in intuitionistic set theory. Along the way, we show that the completeness of Kripke semantics for the disjunction free fragment is equivalent, over intuitionistic Zermelo-Fraenkel set theory, to the Law of Excluded Middle.