TOPOS BASED SEMANTIC FOR CONSTRUCTIVE LOGIC WITH STRONG NEGATION
Barbara Klunder, Barbara Klunder · Mathematical logic quarterly · 1992
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.