Open AccessTopological Completeness for Higher-Order Logic
Author(s) -
Steve Awodey,
Carsten Butz
Publication year - 1997
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v4i21.18947
Subject(s) - predicative expression , topos theory , mathematics , sheaf , completeness (order theory) , intermediate logic , gödel's completeness theorem , higher order logic , topology (electrical circuits) , discrete mathematics , pure mathematics , computer science , theoretical computer science , description logic , combinatorics , mathematical analysis , art , philosophy , linguistics , literature
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.