Об интерпретации секвенций в ситусах.

Аннотация

An interpretation of a Gentzen-type formulation of intuitionistic, brouwerian, classical and H-В-logic in sites (see f 1]) is proposed. A main idea lies in the translation of sequents into coverings of Grothendieck pretopology in so-called N-categories [8]. In case of brouwerian, classical and H-B-logic we need to consider not coverings but cocoverings, polycoverings and bicoverings and as consequence the notions of cosite, polysite and bisite is introduced. By mapping those modifications of coverings into translations of formula counterparts of sequents we obtain the solution of the problem of completeness of such an interpretation. Also the notion of Da N-categories and Da N-sites is introduced which allows, in particular, to develop in such categories Martin-Lof’s type theory according to J. Lambek’s scheme in [6].