Syntax and Semantics of the logic L_omega omega^lambda

Abstract

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