Syntactic Forcing Models for Coherent Logic
Logic
2017-12-22 v1 Category Theory
Abstract
We present three syntactic forcing models for coherent logic. These are based on sites whose underlying category only depends on the signature of the coherent theory, and they do not presuppose that the logic has equality. As an application we give a coherent theory T and a sentence {\psi} which is T-redundant (for any geometric implication {\phi}, possibly with equality, if T + {\psi} proves {\phi}, then T proves {\phi}), yet false in the generic model of T. This answers in the negative a question by Wraith.
Cite
@article{arxiv.1712.07743,
title = {Syntactic Forcing Models for Coherent Logic},
author = {Marc Bezem and Ulrik Buchholtz and Thierry Coquand},
journal= {arXiv preprint arXiv:1712.07743},
year = {2017}
}
Comments
27 pages