BRICS RS-97-22 C. Butz: Syntax and Semantics of the logic L_{ωω}^{λ} BRICS

Basic Research in Computer Science

Syntax and Semantics of the logic L_{ωω}^{λ}

Carsten Butz BRICS Report Series RS-97-22 ISSN 0909-0878 July 1997 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1997, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/97/22/

Syntax and Semantics of the Logic L_{ωω}^{λ}

Carsten Butz^{∗}

July 24, 1997

Abstract

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

In this paper we study aspects of completeness of the logic L_{ωω}^{λ}, which is intuitionistic first order logic extended by quantification over functions. This logic may be seen as well as λ–calculus enriched with first order logic. The details of the syntax are given in section 1.

The logic L_{ωω}^{λ} is of interest for many reasons: it is reasonably powerful and (therefore) incomplete with respect to models in Sets. But the logic L_{ωω}^{λ} is complete with respect to Heyting valued models. In fact, the infinitary variants L_{κω}^{λ} are the strongest logics we know that are complete with respect to Heyting valued models. Secondly, the logic L_{ωω}^{λ} characterises a class of geometric morphisms between Grothendieck toposes, namely the locally connected ones: We show that a geometric morphisms f: F → E between Grothendieck toposes is locally connected if and only if the inverse image f^{∗} preserves the internal L_{ωω}^{λ}–logic of the topos E.

∗BRICS, Basic Research in Computer Science, Centre of the Danish National Research Foundation, Computer Science Department, Aarhus University, Ny Munkegade, DK–8000 Århus C, Denmark, butz@brics.dk.

The first two sections discuss the syntax and semantics of the logic L_{ωω}^{λ}. Models of L_{ωω}^{λ}-theories naturally live in Heyting categories with exponentials (i.e., cartesian closed Heyting categories). After relating the logic to locally connected geometric morphism we present some completeness results in section 4: L_{ωω}^{λ} is complete with respect to models in Grothendieck toposes, therefore as well complete with respect to models in cartesian closed Heyting categories. A recent covering theorem for Grothendieck toposes implies that it is enough to look at Heyting valued models to get completeness. The last section contains some remarks about the infinitary variants L_{κω}^{λ}.

We assume familiarity with basic notions of categorical logic, see for example [14], or [9]. The results presented here are closely related to the joint paper with S. Awodey, [2]. In fact, they give a detailed exposition of one of the completeness result presented there. In case of pure typed λ-calculus, a more detailed exposition can be found in [1].

Our overall presentation is in the line of categorical model theory, as was done for geometric logic in [15] and for first order logic in [6]. One of the more prominent theories which can be formulated in the logic L_{ωω}^{λ} is SDG, synthetic differential geometry [13]. In contrast to this we do not intend to do proof theory here, as was one of the items in [14].

1 Syntax

We begin by describing the syntax of the logic L_{ωω}^{λ}. Given a set \underline{type} of basic sorts A, B, …, the set \underline{type}^{∗} of derived types is the closure of \underline{type} under products and exponentials:

\underline{type}^{∗} : : = A | Y × Z | Z^{Y} .

Thus, the only difference to full higher order logic is the absence of the type of propositions Ω.

Definition 1.1 A λ-signature 𝕊 consists of a list \underline{type}_{𝕊} of basic types and sets \underline{const}_{𝕊}, \underline{funct}_{𝕊}, and \underline{rel}_{𝕊} of constants, function and relation symbols, where each of these symbols is typed over \underline{type}^{∗}.

Since \underline{type}^{∗} has built in product types, we can assume that all functions and relations are unary. As usual, we write expressions like c: A, f: Z → Y, or R ⊂ Y to indicate the typing.

Next we define the sets \underline{term}(Y) of terms of type Y, which depend on a given λ-signature 𝕊:

— Each set \underline{term}(Y) contains countably many variables of type Y, and expressions like y: Y have their obvious meaning.

— If c is a constant of type Y, it is a term of type Y. If t is a term of type Y, and f: Y → Z is a function symbol, then f(t) is in \underline{term}(Z).

— If t_{1} ∈ \underline{term}(Y_{1}) and t_{2} ∈ \underline{term}(Y_{2}), then ⟨t_{1}, t_{2}⟩ is a term of type Y_{1}×Y_{2}. Conversely, if t is in \underline{term}(Y_{1} × Y_{2}), then π_{1}t is a term of type Y_{1}, and π_{2}t is a term of type Y_{2}.

— If t is a term of type Y and α ∈ \underline{term}(Z^{Y}), then α(t) is a term of type Z. If t is a term of type Z (possibly containing the free variable y: Y), then λy.t(y) is a term of type Z^{Y}.

The formulas are generated by the following rules:

— If t_{1} and t_{2} are terms of the same type, then t_{1} = t_{2} is a formula.

— If R ⊂ Y is a relation symbol and t is a term of type Y, then R(t) is a formula.

— The logical constants ⊥ and ⊤ are formulas. If φ and ψ are formulas, so are ¬φ, φ ∧ ψ, φ ∨ ψ, and φ → ψ.

— If ϕ(y) is a formula (possibly containing the free variable y: Y), then ∀y: Y φ(y) and ∃y: Y φ(y) are formulas.

If we type the formulas by the (imaginary) type Ω, these term and formula forming operations can be summarised in the familiar way:

Y  Y_{1} × Y_{2}  Y_{1}  Z  Z^{Y}  Ω
c  ⟨t_{1}, t_{2}⟩  π_{1}t̄ α(t) λy.t(y)  t = t′
f(t)  R(t)
⊥, ⊤
φ ∧ ψ, φ ∨ ψ
¬φ, φ → ψ
∀yϕ(y), ∃yϕ(y)

where c: Y, f: Z → Y, R ⊂ Z, and the sub-terms are of type

Z  Y_{1} Y_{2} Y_{1} × Y_{2} Z^{Y}  Ω
t, t′  t_{1}  t_{2}  t̄  α  φ, ψ
t(y)  ϕ(y)

For each finite set X of variables we define a deduction relation ⊢_{X} between formulas. If we write an expression p ⊢_{X} q it is always assumed that the free variables occurring on both sides are contained in the set X. Below, ⊢_{X} p abbreviates ⊤ ⊢_{X} p, and p ⊢ q stands for p ⊢_{∅} q. As in [14] we group the rules into different classes:

Structural rules.

1.1 p ⊢_{X} p;
1.2 p ⊢_{X} q and q ⊢_{X} r implies p ⊢_{X} r;
1.3 p ⊢_{X} q implies p ⊢_{X∪{y}} q;
1.4 φ(y) ⊢_{X} ψ(y) implies φ(b) ⊢_{X\{y}} ψ(b),

provided that y is a variable of type Y and b is a term of type Y with no free occurrence of variables other then those in X \ {y}. It is being assumed that b is substitutable for y in both sides, i.e., no free variable in b becomes bound after substitution.

Logical rules.

2.1 p ⊢_{X} ⊤;
⊥ ⊢_{X} p;
2.2 r ⊢_{X} p ∧ q iff r ⊢_{X} p and r ⊢_{X} q;
p ∨ q ⊢_{X} r iff p ⊢_{X} r and q ⊢_{X} r;
2.3 p ⊢_{X} q → r iff p ∧ q ⊢_{X} r;
2.4 p ⊢_{X} ∀yψ(y) iff p ⊢_{X∪{y}} ψ(y);
∃yψ(y) ⊢_{X} p iff ψ(y) ⊢_{X∪{y}} p.

Extralogical axioms.

3.1 ⊢ ∀z: Y_{1} × Y_{2} (z = ⟨π_{1}z, π_{2}z⟩);

3.2 ⊢ ∀z: Y_{1} × Y_{2}∀z′: Y_{1} × Y_{2} (z = z′ → (π_{1}z = π_{1}z′ ∧ π_{2}z = π_{2}z′));

3.3 ⊢ ∀y_{1}: Y_{1}∀y_{2}: Y_{2} (π_{1}⟨y_{1}, y_{2}⟩ = y_{1} ∧ π_{2}⟨y_{1}, y_{2}⟩ = y_{2});

3.4 (Comprehension)

⊢ ∀y: Y [λy′.t(y′)](y) = t(y);

3.5 (Extensionality)

∀f: Z^{Y} ∀g: Z^{Y} ((∀y: Y f(y) = g(y)) → f = g).

Axioms for equality.

4.1 ⊢_{{y}} y = y;

y = y′ ⊢_{{y,y′}} y′ = y;

y_{1} = y_{2} ∧ y_{2} = y_{3} ⊢_{{y_{1},y_{2},y_{3}}} y_{1} = y_{3};

4.2 y = y′ ⊢_{{y,y′}} f(y) = f(y′);

for each functions symbol f: Y → Z;

y = y′ ⊢_{{y,y′}} R(y) ↔ R(y′);

for each relation symbol R ⊂ Y.

The calculus defined so far is intuitionistic. The deduction relations ⊢_{X}^{c} are defined by adding the logical rule

⊤ ⊢_{X} p ∨ ¬p.

In general, we write T ⊢ p (or T ⊢_{X} p) for derivability in the calculus with added axioms ⊢ τ for τ in T. In case T consists just of one formula, the two notions {τ} ⊢ p and τ ⊢_{p} coincide, so that that T ⊢ p just extends our definition of ⊢. Similar calculi as above for full second order logic can be found in [4] and in [14].

2 Semantics

It should be clear from the syntax that the right categories hosting models of L_{ωω}^{λ}–theories are (ω–) Heyting categories with exponentials (i.e., cartesian closed Heyting categories or logoi with exponentials in the language of [9]). Recall that a Heyting category is a regular category C that has, in addition to finite intersections of subobjects, unions of finite families of subobjects. Moreover, pulling back subobjects along a fixed morphism has a right adjoint. (It follows that the lattice of subobjects of each object in C is a Heyting algebra, and this Heyting algebra structure is preserved under pullbacks.) The most prominent examples of Heyting categories with exponentials are elementary toposes, in particular, Grothendieck toposes.

Let C be a Heyting category with exponentials. An interpretation M of a λ–signature 𝕊 in C assigns first of all to each basic sort A ∈ \underline{type}_{𝕊} an object A^{(M)}. This assignment extends naturally to all types, by (Y ×Z)^{(M)} = Y^{(M)} × Z^{(M)} and (Z^{Y})^{(M)} = Z^{(M)}^{Y^{(M)}}. Furthermore, the interpretation M assigns a global element c^{(M)}: 1 → Y^{(M)} for each constant c: Y in \underline{const}_{𝕊}, a function f^{(M)}: Y^{(M)} → Z^{(M)} for each function symbol f: Y → Z in \underline{funct}_{𝕊}, and a subobject R^{(M)} ↣ Y^{(M)} for each relation symbol R ⊂ Y in \underline{rel}_{𝕊}. Using the structure of the category C, we extend this interpretation to arbitrary terms and formulas. In particular, for a formula ψ(\overline{y}: \overline{Y}) (\overline{y} = (y_{1}, …, y_{n}) of type \overline{Y} = Y_{1}, …, Y_{n}) we get a subobject

\{\overline{y} | ψ(\overline{y})\}^{(M)} ↣ \overline{Y}^{(M)} = Y_{1}^{(M)} × ⋯ × Y_{n}^{(M)}.

As usually, we say that M is a model of a closed formula τ (M ⊧ τ) if {· | τ}^{(M)} ↣ ∅^{(M)} = 1_{C} is the top element in the Heyting algebra of subobjects of 1_{C}. This way we get a sound notion of models:

Proposition 2.1 (Soundness) The deduction relation ⊢ is sound for the notion of models just defined, i.e., for any set of L_{ωω}^{λ}-formulas T and any λ-formula τ, T ⊢ τ implies T ⊧ τ. □

One of our main goals will be to prove the converse of Proposition 2.1, i.e., completeness.

Next we turn the class of models of a theory in a fixed Heyting category C with exponentials into a category. A morphism h between 𝕊-interpretations M and M′ is a family of maps \{h_{Y}: Y^{(M)} → Y^{(M′)}\}_{Y ∈\underline{type}_{𝕊}^{∗}}, satisfying the following three conditions:

(i) h_{Y_{1}×Y_{2}} = ⟨h_{Y_{1}}, h_{Y_{2}}⟩: Y_{1}^{(M)} × Y_{2}^{(M)} → Y_{1}^{(M′)} × Y_{2}^{(M′)}

for all types Y_{1}, Y_{2} ∈ \underline{type}_{𝕊}^{∗}.

(ii) For all Y and Z in \underline{type}_{𝕊}^{∗} the following two diagrams commute:

\xymatrix{Y^{(M)} × (Z^{Y})^{(M)} \ar[r]^{⟨h_{Y} ,h_{Z^{Y}} ⟩} \ar[d]_{ϵ} & Y^{(M′)} × (Z^{Y})^{(M′)} \ar[d]^{ϵ} & Z^{(M)} \ar[r]^{h_{Z}} \ar[d]_{{ \atop const}} & Z^{(M′)} \ar[d]^{{ \atop const}} \\ Z^{(M)} \ar[r]_{h_{Z}} & Z^{(M′)} & (Z^{Y})^{(M)} \ar[r]_{h_{Z^{Y}}} & (Z^{Y})^{(M′)}}

where { \atop const} is the transposed of the projection map π_{2}: Z^{(−)} × Y^{(−)} → Z^{(−)}.

(iii) The maps \{h_{Y} \}_{Y ∈\underline{type}_{𝕊}^{∗}} preserve the interpretation of constants, function and relation symbols. For example, for a constant c: Y this means that

\xymatrix{Y^{(M)} \ar[r]^{h_{Y}} & Y^{(M′)} \\ 1 \ar[u]^{c^{(M)}} \ar[ur]_{c^{(M′)}}}

commutes.

For the following definition we remind the reader of the forcing relation ⊩ in C (usually only defined if C is a topos): For a λ-formula ψ(\overline{y}: \overline{Y}), for U in E, and for generalised elements α_{i}: U → Y_{i}^{(M)} we write U ⊩ ψ(α_{1}, …, α_{n}) if the map ⟨α_{1}, …, α_{n}⟩: U → \overline{Y}^{(M)} factors through \{\overline{y} | ψ(\overline{y})\}^{(M)} ↪ \overline{Y}^{(M)}.

Definition 2.2 Let M and M′ be two S-interpretations in C. A morphism of 𝕊-structures h: M → M′ is called an L_{ωω}^{λ}–homomorphism if for each L_{ωω}^{λ}- formula ψ(\overline{y}: \overline{Y}) and generalised elements α_{i}: U → Y_{i}^{(M)}

U ⊩ ψ(α_{1}, …, α_{n})  implies  U ⊩ ψ(h_{Y_{1}} ∘ α_{1}, …, h_{Y_{n}} ∘ α_{n}).

We denote by \underline{Mod}^{λ}(T, C) the category of models of T in C, with morphisms the L_{ωω}^{λ}–homomorphisms. Note that the condition of the definition is equivalent to the following: h: M → M′ is an L_{ωω}^{λ}–homomorphism if and only if for each formula ψ(\overline{y}: \overline{Y}) the composite h\overline{Y} ∘ i: \{\overline{y} | ψ(\overline{y})\}^{(M)} ↪ \overline{Y}^{(M)} → \overline{Y}^{(M′)} factors through \{\overline{y} | ψ(\overline{y})\}^{(M′)}, viz.

\xymatrix{\overline{Y}^{(M)} \ar[r] & \overline{Y}^{(M′)} \\ \{\overline{y} | ψ(\overline{y})\}^{(M)} \ar@{^{(}->}[u] \ar@{-->}[r] & \{\overline{y} | ψ(\overline{y})\}^{(M′)}. \ar@{^{(}->}[u]}

3 A topos theoretical characterisation of L_{ωω}^{λ}

Recall that a geometric morphism f: F → E between Grothendieck toposes is called locally connected (or molecular [3]) if the inverse image f^{∗} commutes with ∏–functors. Equivalently, f is locally connected iff for all E in E the inverse image of the induced geometric morphism f/E in

\xymatrix{F/f^{∗}E \ar[r] \ar[d]_{f/E} & F \ar[d]^{f} \\ E/E \ar[r] & E}

preserves exponentials. Locally connected geometric morphisms are open (see [11]) and hence preserve the internal first order logic. We sum this up in the following lemma:

Lemma 3.1 The inverse image of a locally connected geometric morphism f: F → E induces a functor

f^{∗}: \underline{Mod}^{λ}(T, E) → \underline{Mod}^{λ}(T, F),

for any L_{ωω}^{λ}–theory T. □

To prove a somehow converse of the lemma we need the following characterisation of locally connected geometric morphisms:

Proposition 3.2 A geometric morphism f: F → E between Grothendieck toposes is locally connected if and only if it is open and the inverse image f^{∗} preserves exponentials.

Proof. We know already one direction. For the other fix an object E in E and p = (P → E), q = (Q → E) in E/E. We note first that the exponential q^{p} is given by r = (R → E) for

R = {α ∈ Q^{P} | ∀x: P p(x) = q(α(x))},

which uses only exponentials, first order logic and (implicitly) the counit P × Q^{P} → Q. But all the data is preserved by f^{∗}, so

f^{∗}R = {α ∈ f^{∗}(Q)^{f^{∗}(P)} | ∀x: f^{∗}P f^{∗}p(x) = f^{∗}q(α(x))},

and f/E^{∗}(q^{p}) = f/E^{∗}(r) = (f^{∗}R → f^{∗}E) = (f/E^{∗}q)^{(f/E^{∗}p)}. □

Combining the proposition with the characterisation of open maps in terms of first order logic we get

Corollary 3.3 A geometric morphism f: F → E is locally connected if and only if its inverse image preserves the internal L_{ωω}^{λ}–logic of E, i.e., the interpretation of any L_{ωω}^{λ}–formula in the topos E. □

4 Completeness

Here we construct minimal models of L_{ωω}^{λ}–theories in a similar way as was done in [6] or [16].

Let T ⊂ L_{ωω}^{λ}(𝕊) be a set of axioms. We define a syntactic site Syn(T) as follows:

— Objects are pairs ([φ(x), X) where X is a (derived) type, x is a variable of type X, and [φ(x)] is an equivalence class of L_{ωω}^{λ}–formulas. Two formulas φ_{1}(x_{1}) and φ_{2}(x_{2}) are equivalent if

T ⊢ ∀x(φ_{1}(x) ↔ φ_{2}(x)),

where x is a new variable.

— Arrows from ([φ(x), X) to ([ψ(y)], Y) are triples ([σ(x, y)], X, Y) such that [σ(x, y)] is an equivalence class of L_{ωω}^{λ}–formulas and, moreover, σ is provably functional:

T ⊢ ∀x∀y(σ(x, y) → φ(x) ∧ ψ(y))
T ⊢ ∀x(φ(x) → ∃yσ(x, y))
T ⊢ ∀x∀y∀z(σ(x, y) ∧ σ(x, z) → y = z).

Here we used the same names for the variables occurring in φ, ψ and σ, indicating that we do not care about possibly renaming the variables.

— We say that a finite family of arrows ([σ_{i}(x_{i}, y)], X_{i}, Y): ([φ_{i}(x_{i})], X_{i}) → ([ψ(y)], Y) is a cover if

T ⊢ ∀y(ψ(y) → ⋁_{I} ∃x_{i}σ_{i}(x_{i}, y)).

It is easy to show that Syn(T) has all finite limits and some exponentials (namely those of the form ([z = z], Z)^{([y=y],Y)} = ([w = w], Z^{Y})), and the topology is subcanonical. But the category Syn(T) fails to be cartesian closed. Still, there is a canonical interpretation of our language in this category, and this interpretation yields a conservative model of T in Syn(T).

Write 𝔅^{λ}(T) for the topos of sheaves on Syn(T), equipped with the finite cover topology. The Yoneda embedding y: Syn(T) → 𝔅^{λ}(T) provides an interpretation U of the underlying language as follows:

A^{(U)} = y([x = x], A),

for each basic sort A. The above mentioned properties of Syn(T) and the fact that y preserves exponentials imply that

Y^{(U)} ≅ y([y = y], Y)

for any derived type Y. Constants and relations are interpreted as follows:

c^{(U)}: 1 → Y^{(U)}  := y([c = y], ∅, Y): y([⊤], ∅) → y([y = y], Y)
f^{(U)}: Y^{(U)} → Z^{(U)} := y([f(y) = z], Y, Z): y([y = y], Y) → y([z = z], Z)
R^{(U)} ↣ Y^{(U)}  := y([R(y)], Y) ↣ y([y = y], Y).

The core of this section is the following proposition:

Proposition 4.1 For each L_{ωω}^{λ}(𝕊)–formula ψ(y: Y) there is a canonical isomorphism y([ψ(y)], Y)≅ {y | ψ(y)}^{(U)}.

Proof. This is a long induction over the complexity of ψ. Roughly speaking, Syn(T) is a Heyting category, and the Yoneda embedding preserves the first order structure, see [6] for details. Moreover, since the topology is subcanonical, y preserves exponentials which happen to exist. □

As a corollary we derive the major result, namely completeness with respect to models in Grothendieck toposes:

Theorem 4.2 U is a conservative model of T. For a closed formula τ we have U ⊧ τ if and only if T ⊢ τ. In particular, L_{ωω}^{λ} is complete with respect to models in Grothendieck toposes (and therefore complete with respect to Heyting categories with exponentials).

Proof. The first part is immediate from proposition 4.1, the rest is trivial. □

Using a recent covering theorem for toposes with enough points, we can strengthen the theorem the following way:

Corollary 4.3 For each consistent set of axioms T ⊂ L_{ωω}^{λ}(𝕊) there exists a topological space X and an OX–valued model M of T (a Heyting valued model of T which takes its truth values in the complete Heyting algebra OX of open sets of X) such that M ⊧ τ iff T ⊢ τ for each closed formula τ.

Proof. Given T the site Syn(T) is coherent and therefore 𝔅^{λ}(T) has enough points. By theorem 13.5 of [5] (see as well [7]) there exists a connected, locally connected geometric morphism

m: Sh(X) → 𝔅^{λ}(T)

for X a topological space. By lemma 3.1, M = m^{∗}U is a model of T in Sh(X), which is conservative since m is a surjective geometric morphism. The corollary follows since models in Sh(X) correspond to OX–valued models, see [8] for details. □

What are the points of the topological space X? Classical second order logic is complete with respect to models which are called nowadays Henkin models, see [10]. Combining Henkin’s proof and the standard proof of Heyting valued completeness for first order intuitionistic logic one shows that our logic L_{ωω}^{λ} (but in fact, full intuitionistic second order logic) is complete with respect to Heyting valued Henkin models. Fixing a set of enough Heytingvalued Henkin models S_{T}, points of X are pairs (M, α) where M is in S_{T} and α is an enumeration of M, similar as in [2], appendix. The enumerations are used to define the topology.

Before we end this section let us mention that the model U in 𝔅^{λ}(T) is minimal in the following sense:

Proposition 4.4 For any model M of T in a Grothendieck topos F there is a unique (up to isomorphism) geometric morphism χ_{M}: F → 𝔅^{λ}(T) such that for each L_{ωω}^{λ}(𝕊)–formula ψ(y: Y)

{y | ψ(y)}^{(M)} ≅ χ_{M}^{∗}{y | ψ(y)}^{(U)}.  (1)

Thereby, we get a fully faithful functor

χ: \underline{Mod}^{λ}(T, F) ⟶ \underline{Hom}(F, 𝔅^{λ}(T)),

natural in locally connected geometric morphisms F′ → F.

Proof. Soundness of ⊢ implies that H_{M}: Syn(T) → F, defined on objects by

([ψ(y)], Y) ↦ {y | ψ(y)}^{(M)}

is a well defined functor. This functor preserves finite limits and covers, therefore induces by Diaconescu’s theorem a geometric morphism χ_{M}: F → 𝔅^{λ}(T) satisfying (1).

By the remark following definition 2.2, L_{ωω}^{λ}–homomorphisms h: M → M′ correspond exactly to natural transformations H_{M} → H_{M′}, which shows that χ_{(−)} extends to a fully faithful functor \underline{Mod}^{λ}(T, F) ⟶ \underline{Hom}(F, 𝔅^{λ}(T)), which is clearly natural in locally connected geometric morphisms. □

As a final remark we mention that given M in F, the geometric morphism χ_{M} is in general not open, hence in general not locally connected.

5 Concluding remarks

Our main goal was to study the logic L_{ωω}^{λ}, but there are as well the infinitary variants L_{κω}^{λ}, where one allows disjunctions and conjunctions over sets of formulas of cardinality less or equal to κ. In that case one has to use cartesian closed κ–Heyting categories as the natural categories where models live. The calculus of section 1 extends immediately to these infinitary logics, and the completeness results of section 4 remain true, although the complete Heyting algebra of corollary 4.3 does not have to come from a topological space: Given a theory T ⊂ L_{κω}^{λ}(𝕊), the site Syn_{κ}(T), defined similar as above using formulas from L_{κω}^{λ}, is not coherent and theorem 13.5 of [5] does not apply. Instead, one has to appeal to the covering theorem of [12]. As noted in the introduction, the logics L_{κω}^{λ} are the strongest logics we know for which a Heyting valued completeness theorem holds. Such a statement for full (intuitionistic) second order logic is certainly wrong: second order logic is even not complete with respect to models in arbitrary Grothendieck toposes.

Finally we should admit that there is something wrong with the syntax of our logic: We should not just extend first order logic by quantification over function types, but by quantification over definable function types, i.e., we should allow expressions like

∀f: {x | φ(x)}^{{y|ψ(y)}}( ⋯)

where (recursively) φ and ψ are formulas of our language. Write L_{κω}^{λ+} for this logic. Given a theory T ⊂ L_{κω}^{λ+}(𝕊) we can construct as before a syntactic site Syn_{κ}^{+}(T), which will now be a cartesian closed κ–Heyting category. In fact, it has the obvious universal property in the category of all cartesian closed κ–Heyting categories. Therefore, a presentation using L_{κω}^{λ+} would parallel [6] much more. But there are good reasons why we didn’t choose this way: Even though we know intuitively very well how to handle the syntax of L_{κω}^{λ+}, the formal presentation is clumsy. Any formula defines a type, so that there is no distinction between formulas and types, in particular, there are many identifications and subtypes.

References

[1] S. Awodey. Topological representation of the λ–calculus. In preparation.

[2] S. Awodey and C. Butz. Topological completeness for higher order logic. Preprint, June 1997, submitted.

[3] M. Barr and R. Paré. Molecular toposes. J. Pure and Appl. Algebra, 17:127–152, 1980.

[4] A. Boileau and A. Joyal. La logique des topos. J. Symbolic Logic, 46:6– 16, 1981.

[5] C. Butz. Logical and Cohomological Aspects of the Space of Points of a Topos. PhD thesis, Utrecht 1996.

[6] C. Butz and P. T. Johnstone. Classifying Toposes for First Order Theories. Preprint, June 1997. To appear in Ann. Pure Appl. Logic.

[7] C. Butz and I. Moerdijk. Representing topoi by topological groupoids. Preprint, September 1996. To appear in J. Pure and Appl. Algebra.

[8] M. P. Fourman and D. S. Scott. Sheaves and logic. In M. P. Fourman, C. J. Mulvey, and D. S. Scott, editors, Applications of Sheaves, Lecture Notes in Mathematics 753, pages 302–401, New York, 1979. Springer– Verlag.

[9] P. Freyd and A. Scedrov. Categories, Allegories. North–Holland, Amsterdam 1990.

[10] L. Henkin. Completeness in the theory of types. J. Symbolic Logic, 15:81–91, 1950.

[11] P. T. Johnstone. Open maps of toposes. Manuscripta Math., 31:217–247, 1980.

[12] A. Joyal and I. Moerdijk. Toposes are cohomologically equivalent to spaces. Am. J. Math., 112:87–96, 1990.

[13] A. Kock. Synthetic differential geometry. Cambridge University Press, Cambridge 1981.

[14] J. Lambek and P. J. Scott. Introduction to Higher–Order Categorical Logic. Cambridge University Press, Cambridge, 1983.

[15] M. Makkai and G. E. Reyes. First Order Categorical Logic, Lecture Notes in Mathematics 611. Springer–Verlag, Berlin, 1977.

[16] E. Palmgren. Constructive sheaf semantics. To appear in Mathematical Logic Quarterly.

Recent BRICS Report Series Publications

RS-97-22 Carsten Butz. Syntax and Semantics of the logic L_{ωω}^{λ}. July 1997. 14 pp.

RS-97-21 Steve Awodey and Carsten Butz. Topological Completeness for Higher-Order Logic. July 1997. 19 pp.

RS-97-20 Carsten Butz and Peter T. Johnstone. Classifying Toposes for First Order Theories. July 1997. 34 pp.

RS-97-19 Andrew D. Gordon, Paul D. Hankin, and Søren B. Lassen. Compilation and Equivalence of Imperative Objects. July 1997. iv+64 pp. Aappears also as Technical Report 429, University of Cambridge Computer Laboratory, June 1997. To appear in Foundations of Software Technology and Theoretical Computer Science: 17th Conference, FCT&TCS ’97 Proceedings, LNCS, 1997.

RS-97-18 Robert Pollack. How to Believe a Machine-Checked Proof. July 1997. 18 pp. To appear as a chapter in the book Twenty Five Years of Constructive Type Theory, eds. Smith and Sambin, Oxford University Press.

RS-97-17 Peter Bro Miltersen. Error Correcting Codes, Perfect Hashing Circuits, and Deterministic Dynamic Dictionaries. June 1997. 10 pp.

RS-97-16 Noga Alon, Martin Dietzfelbinger, Peter Bro Miltersen, Erez Petrank, and Gábor Tardos. Linear Hashing. June 1997. 22 pp. A preliminary version appeared with the title Is Linear Hashing Good? in The Twenty-ninth Annual ACM Symposium on Theory of Computing, STOC ’97, pages 465–474.

RS-97-15 Pierre-Louis Curien, Gordon Plotkin, and Glynn Winskel. Bistructures, Bidomains and Linear Logic. June 1997. 41 pp.

RS-97-14 Arne Andersson, Peter Bro Miltersen, Søren Riis, and Mikkel Thorup. Dictionaries on AC^{0} RAMs: Query Time Θ(\sqrt{log n/ log log n}) is Necessary and Sufficient. June 1997. 18 pp. Appears in 37th Annual Symposium on Foundations of Computer Science, FOCS ’96 Proceedings, pages 441–450.

RS-97-13 Jørgen H. Andersen and Kim G. Larsen. Compositional Safety Logics. June 1997. 16 pp.