Topological Completeness for Higher-Order Logic

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.

Cited by in corpus (3)

• Normalization for Cubical Type Theory
• Mathematical semantics of intuitionistic logic
• A proposition is the (homotopy) type of its proofs