Syntax and Semantics of the Logic

Notre Dame Journal of Formal Logic 38 (3):374-384 (1997)
  Copy   BIBTEX


In this paper we study the logic , which is first-order logic extended by quantification over functions (but not over relations). We give the syntax of the logic as well as the semantics in Heyting categories with exponentials. Embedding the generic model of a theory into a Grothendieck topos yields completeness of with respect to models in Grothendieck toposes, which can be sharpened to completeness with respect to Heyting-valued models. The logic is the strongest for which Heyting-valued completeness is known. Finally, we relate the logic to locally connected geometric morphisms between toposes



    Upload a copy of this work     Papers currently archived: 91,122

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles


Added to PP

19 (#732,197)

6 months
8 (#241,888)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Completeness in the theory of types.Leon Henkin - 1950 - Journal of Symbolic Logic 15 (2):81-91.
Sheaves and Logic.M. P. Fourman, D. S. Scott & C. J. Mulvey - 1983 - Journal of Symbolic Logic 48 (4):1201-1203.
La logique Des topos.André Boileau & André Joyal - 1981 - Journal of Symbolic Logic 46 (1):6-16.
Constructive Sheaf Semantics.Erik Palmgren - 1997 - Mathematical Logic Quarterly 43 (3):321-327.
Classifying toposes for first-order theories.Carsten Butz & Peter Johnstone - 1998 - Annals of Pure and Applied Logic 91 (1):33-58.

View all 8 references / Add more references