Luchli’s Completeness Theorem from a Topos-Theoretic Perspective

摘要

We prove a variant of Luchls completeness theorem for intuitionistic predicate calculus. The formulation of the result relies on the observation (due to Lawvere) that Luchli’s theorem is related to the logic of the canonical indexing of the atomic topos of Z-sets. We show that the process that transforms Kripkecounter- models into Luchli-counter-models is (essentially) the inverse image of a geometric morphism. Completeness follows because this geometric morphism is an open surjection.