Hostname: page-component-cd9895bd7-dk4vv Total loading time: 0 Render date: 2024-12-22T10:19:40.984Z Has data issue: false hasContentIssue false
  • English
  • Français

Topological completeness for higher-order logic

Published online by Cambridge University Press:  12 March 2014

S. Awodey  and
C. Butz
S. Awodey
Affiliation:
Department of Philosophy, Carnegie Mellon University, Pittsburgh, Pennsylvania 15213-3890, USA E-mail: awodey@cmu.edu
C. Butz
Affiliation:
Brics, Basic Research in Computer Science, Centre of the Danish National Research Foundation, Computer Science Department, Aarhus University, NY Munkegade, Bldg. 540, 8000 Aarhus C., Denmark E-mail: butz@brics.dk
Get access Rights & Permissions [Opens in a new window]

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
The Journal of Symbolic Logic , Volume 65 , Issue 3 , September 2000 , pp. 1168 - 1182
Copyright
Copyright © Association for Symbolic Logic 2000

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

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