arXiv · 1712.07743
Syntactic Forcing Models for Coherent Logic
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 ψ which is T-redundant (for any geometric implication ϕ, possibly with equality, if T + ψ proves ϕ, then T proves ϕ), yet false in the generic model of T. This answers in the negative a question by Wraith.
Explore related subjects
Keep this discovery
Explore connections, maps & timelines
Marc Bezem, Ulrik Buchholtz, Thierry Coquand. 2017-12-20. Syntactic Forcing Models for Coherent Logic. https://arxiv.org/abs/1712.07743
Cite the original work for its findings. Save a collection to share your selection of sources.