Topological Completeness for Higher-Order Logic

1997/07/24 by Awodey, Steve, Butz, Carsten
#Category Theory (math.CT) #FOS: Mathematics #Logic (math.LO)

paper · doi:10.48550/arxiv.math/9707206

Abstract

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.

Related

• Sheaf Representations and Duality in Logic
• Geometric contexts and applications to logic
• Recursive Difference Categories and Topos-Theoretic Universality
• Topological completeness of logics above S4
• Semantical Investigations on Non-classical Logics with Recovery Operators: Negation