Premium
TOPOS BASED SEMANTIC FOR CONSTRUCTIVE LOGIC WITH STRONG NEGATION
Author(s) -
Klunder Barbara,
Klunder B.
Publication year - 1992
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.19920380146
Subject(s) - topos theory , mathematics , morphism , negation , gödel's completeness theorem , intuitionistic logic , predicate (mathematical logic) , constructive , object (grammar) , predicate logic , algebra over a field , discrete mathematics , calculus (dental) , pure mathematics , propositional calculus , programming language , computer science , artificial intelligence , description logic , medicine , art , literature , dentistry , process (computing)
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 .