A co-free construction for elementary doctrines
Logic
2014-01-31 v2
Abstract
We provide a co-free construction which adds elementary structure to a primary doctrine. We show that the construction preserves comprehensions and all the logical operations which are in the starting doctrine, in the sense that it maps a first order many-sorted theory into a the same theory formulated with equality. As a corollary it forces an implicational doctrine to have an extentional entailment.
Keywords
Cite
@article{arxiv.1211.1891,
title = {A co-free construction for elementary doctrines},
author = {Fabio Pasquali},
journal= {arXiv preprint arXiv:1211.1891},
year = {2014}
}