TY - JOUR
AU - Steve Awodey
AU - Carsten Butz
PY - 1997/01/21
Y2 - 2020/04/06
TI - Topological Completeness for Higher-Order Logic
JF - BRICS Report Series
JA - BRICS
VL - 4
IS - 21
SE - Articles
DO - 10.7146/brics.v4i21.18947
UR - https://tidsskrift.dk/brics/article/view/18947
AB - Using recent results in topos theory, two systems of higher-order logic are shown to be complete with respect to sheaf models over topological spaces - so-called "topological semantics". The first is classical higher order logic, with relational quantification of finitely high type; the second system is a predicative fragment thereof with quantification over functions between types, but not over arbitrary relations. The second theorem applies to intuitionistic as well as classical logic.
ER -