TY - JOUR AU - Awodey, Steve AU - Butz, Carsten PY - 1997/01/21 Y2 - 2024/03/28 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 SP - 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 -