Article contents
Topological completeness for higher-order logic
Published online by Cambridge University Press: 12 March 2014
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.
- Type
- Research Article
- Information
- Copyright
- Copyright © Association for Symbolic Logic 2000
References
REFERENCES
[1]Awodey, S., Logic in topoi: Functorial semantics for higher-order logic, Ph.D. thesis, The University of Chicago, 1997.Google Scholar
[2]Awodey, S., Topological representation of the λ-calculus, Report CMU-PHIL-85, Carnegie Mellon University, May 1998, 21 pp., to appear in Mathematical Structures in Computer Science.Google Scholar
[3]Barr, M. and Paré, R., Molecular toposes, Journal of Pure and Applied Algebra, vol. 17 (1980), pp. 127–152.CrossRefGoogle Scholar
[4]Boileau, A. and Joyal, A., La logique des topos, this Journal, vol. 46 (1981), pp. 6–16.Google Scholar
[5]Butz, C., Logical and cohomological aspects of the space ofpoints of a topos, Ph.D. thesis, Universiteit Utrecht, 1996.Google Scholar
[6]Butz, C. and Moerdijk, I., Topological representation of sheaf cohomology of sites, Preprint 973, Department of Mathematics, Utrecht University, September 1996, 17 pp., to appear in Compositio Mathematica.Google Scholar
[7]Church, A., A foundation for the simple theory of types, this Journal, vol. 5 (1940), pp. 56–68.Google Scholar
[8]Fourman, M. P. and Scott, D. S., Sheaves and logic, Applications of sheaves (Fourman, M. P., Mulvey, C., and Scott, D. S., editors), Lecture Notes in Mathematics, vol. 753, Springer-Verlag, 1977, pp. 302–401.Google Scholar
[9]Henkin, L., Completeness in the theory of types, this Journal, vol. 15 (1950), pp. 81–91.Google Scholar
[10]Joyal, A. and Moerdijk, I., Toposes as homotopy groupoids, Advances in Mathematics, vol. 80 (1990), pp. 22–38.CrossRefGoogle Scholar
[11]Lambek, J. and Scott, P. J., Introduction to higher-order categorical logic, Cambridge University Press, 1986.Google Scholar
[12]Lane, S. Mac and Moerdijk, I., Sheaves in geometry and logic: A first introduction to topos theory, Springer-Verlag, 1992.Google Scholar
- 3
- Cited by