arXiv · 1211.1891
A co-free construction for elementary doctrines
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.
Explore related subjects
Keep this discovery
Fabio Pasquali. 2014-01-30. A co-free construction for elementary doctrines. https://arxiv.org/abs/1211.1891
Cite the original work for its findings. Save a collection to share your selection of sources.