Abstract: | The aim of the paper is to show that topoi are useful in the categorial analysis of the constructive logic with strong negation. In any topos ? we can distinguish an object Λ and its truth-arrows such that sets ?(A, Λ) (for any object A) have a Nelson algebra structure. The object Λ is defined by the categorial counterpart of the algebraic FIDEL-VAKARELOV construction. Then it is possible to define the universal quantifier morphism which permits us to make the first order predicate calculus. The completeness theorem is proved using the Kripke-type semantic defined by THOMASON . |