Syntax and Semantics of the logic tex2html_wrap_inline28

Carsten Butz

July 1997


In this paper we study the logic tex2html_wrap_inline28 , 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 tex2html_wrap_inline28 with respect to models in Grothendieck toposes, which can be sharpened to completeness with respect to Heyting valued models. The logic tex2html_wrap_inline28 is the strongest for which Heyting valued completeness is known. Finally, we relate the logic to locally connected geometric morphisms between toposes

Available as PostScript, PDF, DVI.


Last modified: 2003-06-08 by webmaster.