BRICS RS-97-21 Awodey & Butz: Topological Completeness for Higher-Order Logic BRICS

Basic Research in Computer Science

Topological Completeness for Higher-Order Logic

Steve Awodey Carsten Butz BRICS Report Series RS-97-21 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/21/

Topological Completeness for Higher-Order Logic

S. Awodey^{∗}  C. Butz^{†}

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 higherorder 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.

Introduction

Higher-order logic (also known as “type theory”) is logic that includes quantification over functions or relations. Many basic mathematical objects and theories can only be defined using this logic; the natural numbers and topological spaces are familiar examples. A more precise specification of what we call classical higher-order logic is given in §1 below.

As is well-known, higher-order theories are generally incomplete with respect to (standard) models in Sets; that is, 𝕋 ⊧ σ does not imply 𝕋 ⊢ σ for 𝕋 a theory in higher-order logic and ⊢ the entailment relation of any reasonable deductive calculus. It is by now also well-known that higher-order logic can be modeled in suitable generalized categories of sets, namely (elementary) topoi, and that with regard to such topos-valued semantics, standard higher-order deduction is complete (see [11] for details).

∗Philosophy Department, Carnegie Mellon University, Pittsburgh PA 15213-3890, USA.

awodey@cmu.edu

†BRICS, Basic Research in Computer Science, Centre of the Danish National Research Foundation, Computer Science Department, Aarhus University, Ny Munkegade, Bldg. 540, 8000 Aahrus C., Denmark. butz@brics.dk

Our results in this paper are concerned with topos models of a very special and natural kind, namely sheaves over topological spaces. If X is a space, a model in the category Sh(X) of all sheaves on X shall be called a topological model. We will show that higher-order logic is complete with respect to such models; for the reader unfamiliar with sheaf theory, we wish to emphasize their elementary topological character. Under the equivalence Sh(X) ≃ Etale/X a sheaf on a space X is essentially the same thing as an étale space over X: a space E equipped with a local homeomorphism p : E → X (also called an étale bundle). The various fibers p^{−1}x of E (the stalks of the sheaf) for the points x ∈ X may be regarded as sets varying continuously over X. A morphism of étale spaces is just a continuous map f : E → E′ over X, i.e. with p′f = p as in the commutative triangle

E  \overline{f  _{>}} E′
[figure: p; p′]
X.

Products, exponentials (“function spaces”), etc. of étale spaces of course agree with those calculated as sheaves. A topological model of a singlesorted theory thus consists of an étale space p: E → X over a base space X together with suitable operations, which are simply continuous maps over X.

As the reader who is familiar with sheaf theory will have noted, our topological models are just what are usually called “sheaves of … s”, at least in the case of equational, first-order theories. Thus a topological model of the theory of groups is a sheaf of groups, and so on.

Despite the ultimately simple character of topological models, we use the more general language and methods of sheaf theory and topoi to study them. Our first theorem, proved in §3 below, asserts the completeness of standard, classical higher-order deduction ⊢^{c} with respect to such topological semantics.

Theorem A. Let 𝕋 be a higher-order theory. There exists a classical topological model M of 𝕋 such that, for any higher-order sentence σ in the language of 𝕋,

𝕋 ⊢^{c} σ  if and only if  M ⊧^{c} σ.

Moreover, the model M has the property that every continuous function between the interpretations of type symbols is logically definable.

What permits theorem A to be true is our notion of a classical model. In an arbitrary topological sheaf topos Sh(X) there are two natural candidates for the interpretation of the type 2 of formulas (or “propositions”, or “truth values”) of a higher-order theory; to wit, the sheaf Ω of open subsets of X and the coproduct 1 + 1. In the language of étale spaces, 1 + 1 is the double covering X × 2 → X. As detailed in §2 below, a classical model uses the latter to interpret the type of formulas. Function and power types are then interpreted as exponentials of sheaves (sometimes called “internal homs” or “sheaf-valued homs”). This standard treatment of exponentials is what chiefly distinguishes topological models from so-called Henkin models (see the appendix below for the exact relation between the two). Thus in particular, for any type Z the power type 2^{Z} is interpreted as the sheaf of complemented subsheaves of the interpretation of Z. By further requiring of a classical model that the types be interpreted by so-called decidable sheaves, we can model classical higher-order logic in non-boolean topoi like Sh(X), which is impossible when interpreting the type 2 by the subobject classifier Ω. Indeed under that interpretation the analogue of theorem A fails—even permitting arbitrary Grothendieck topoi in place of topological sheaf topoi— as can be seen using Gödel incompleteness.

The issue of how to interpret the type of formulas of course vanishes when one considers the fragment of higher-order logic that results from omitting that type. This fragment—which we call λ-logic and describe in §4 below— may be regarded as a marriage of elementary logic and the λ-calculus. In addition to the usual propositional and quantificational language of elementary logic, it includes equations between and quantification over functions, functions of functions, etc. But since there is no type of formulas, there is no quantification over “propositional functions”, i.e. over relations.

Many familiar mathematical constructions, theorems, and proofs can be formalized in λ-logic. A simple example is Cayley’s theorem that every group is isomorphic to a group of permutations of its elements. The axiom of choice, in the familiar form

∀x ∈ X∃y ∈ Y.φ(x, y) ⇒ ∃f ∈ Y^{X}∀x ∈ X.φ(x, fx),

is also a statement of λ-logic. An example of a (non-elementary) λ-theory is synthetic differential geometry, applications to which of the present work shall be discussed elsewhere.

Our theorem B states the completeness of λ-logic with respect to topological models. More generally than theorem A, theorem B holds for standard, intuitionistic deductive entailment ⊢.

Theorem B. Let 𝕋 be a λ-theory. There exists a topological model M of 𝕋 such that, for any λ-sentence σ in the language of 𝕋,

𝕋 ⊢ σ  if and only if  M ⊧ σ.

Moreover, the model M has the property that every continuous function between the interpretations of type symbols is logically definable.

Theorem B rests more squarely on one of the main supports of theorem A, namely a recent covering theorem for topoi due to the second author and I. Moerdijk. This covering theorem is the real heart of our completeness theorems; we sketch its application to our situation as an appendix to this paper. So as not to obscure the conceptual simplicity of this application, our treatment of the standard details of higher-order syntax and topos semantics is held quite brief.

Before getting down to business, we make two remarks on the statements of the completeness theorems. First, each has the form “there exists a model M such that 𝕋 ⊢ σ just if M ⊧ σ”, rather than the more familiar (for setvalued semantics) “𝕋 ⊢ σ just if for all models M, M ⊧ σ ”. The stronger form given here is made possible by considering models in topoi other than Sets. The situation is analogous to that of the familiar Heyting-valued completeness theorem for first-order intuitionistic logic [8], which follows directly from our theorem B and indeed is the inspiration thereof. Second, and more substantially, the additional “Moreover … ” clause of each theorem states a further property of the respective logical system that may be termed “definitional completeness”. It ensures that any function which is “present in every model” is logically definable. As in the case of deductive completeness, this definitional completeness is established in a strong form simply by exhibiting a single model in which every function of suitable type is definable. In light of the topological nature of the models at issue here, logical definability then coincides with continuity in that “minimal” model. For further discussion of this property (in the context of the λ-calculus) we refer to [1].

Acknowledgments. We have both benefitted greatly from conversations with Ieke Moerdijk on the spatial covering theorem and its logical applications. The Stefan Banach Mathematical Research Center in Warsaw, and the organizers of the Rasiowa memorial conference held there in December 1996, are thanked for supporting our collaboration.

1 Theories in classical higher-order logic

The systems of classical higher-order logic that we consider are essentially the same as those presented in [4, 11], which in turn are modern formulations of [7]. We summarize one particular formulation for the reader’s convenience and for the special purposes of §4.

Type symbols are built up inductively from a given list of basic type symbols X_{1}, …, X_{n} and the type of formulas 2 by the type-forming operations Y × Z and Z^{Y}.

Terms are built up inductively from variables and a given list of basic terms c_{1}, …, c_{m}. Each variable and basic term has a type. The terms and their types are as follows, writing τ : Z for “τ is a term of type Z”.

• If τ_{1} : Z_{1} and τ_{2} : Z_{2}, then ⟨τ_{1}, τ_{2}⟩ : Z_{1} × Z_{2}.

• If τ : Z_{1} × Z_{2}, then π_{1}(τ) : Z_{1} and π_{2}(τ) : Z_{2}.

• If τ : Z and y is a variable of type Y, then λy.τ : Z^{Y}.

• If α : Z^{Y} and τ : Y, then α(τ) : Z.

• If τ, τ′ : Z, then τ = τ′ : 2.

• If φ, ψ : 2 and y is a variable of type Y, then the following are terms of type 2:

⊤, ⊥, ¬φ, φ ∧ ψ, φ ∨ ψ, φ ⇒ ψ, ∀y.φ, ∃y.φ.

A basic language (or signature) consists of basic type symbols X_{1}, …, X_{n} and basic constant symbols c_{1}, …, c_{m}. A theory consists of a basic language and a list of sentences (closed formulas) σ_{1}, …, σ_{k} therein, called axioms. Given a theory 𝕋, the language L(𝕋) of 𝕋 is the set of terms in the basic language of 𝕋.

The entailment relation φ ⊢ ψ between formulas is specified in the usual way by a deductive calculus. To include the possibility of “empty” types, it is convenient to give a family of entailment relations φ ⊢_{x} ψ indexed by lists x = (x_{1}, …, x_{i}) of distinct variables including all those occurring free in φ and ψ. These relations are generated by the following conditions (“rules of inference”):

1. Order

(a) φ ⊢_{x} φ

(b) φ ⊢_{x} ψ and ψ ⊢_{x} ϑ implies φ ⊢_{x} ϑ

(c) φ ⊢_{x,y} ψ implies φ[τ/y] ⊢_{x} ψ[τ/y]

2. Equality (a) ⊤ ⊢_{x} τ = τ

(b) τ = τ′ ⊢_{x} φ[τ/y] ⇒ φ[τ′/y]

(c) ϑ ⊢_{x} φ ⇒ ψ and ϑ ⊢_{x} ψ ⇒ φ implies ϑ ⊢_{x} φ = ψ

(d) ∀y.α(y) = β(y) ⊢_{x} α = β

3. Products

(a) ⊤ ⊢_{x} ⟨π_{1}τ, π_{2}τ⟩ = τ

(b) ⊤ ⊢_{x} π_{i}⟨τ_{1}, τ_{2}⟩ = τ_{i}, i = 1, 2

4. Exponents

(a) ⊤ ⊢_{x} (λx.τ)(x) = τ

(b) ⊤ ⊢_{x} λx.α(x) = α

5. Elementary logic

(a) ⊥ ⊢_{x} φ

(b) φ ⊢_{x} ⊤

(c) φ ⊢_{x} ¬ψ iff φ ∧ ψ ⊢_{x} ⊥

(d) ϑ ⊢_{x} φ and ϑ ⊢_{x} ψ iff ϑ ⊢_{x} φ ∧ ψ

(e) ϑ ∨ φ ⊢_{x} ψ iff ϑ ⊢_{x} ψ and φ ⊢_{x} ψ

(f) ϑ ∧ φ ⊢_{x} ψ iff ϑ ⊢_{x} φ ⇒ ψ

(g) ϑ ⊢_{x,y} φ iff ϑ ⊢_{x} ∀y.φ

(h) ∃y.ϑ ⊢_{x} φ iff ϑ ⊢_{x,y} φ

In the foregoing, the τ’s are arbitrary terms; φ, ψ, ϑ are formulas; and α, β are terms of the same exponential type. In writing e.g. φ[τ/y] ⊢_{x} ψ[τ/y] in 1(c) it is assumed that φ[τ/y] and ψ[τ/y] are formulas with no free variables apart from x_{1}, …, x_{i}; so the term τ must have the same type as the variable y and no other free variables. As usual, the substitution notation φ[τ/y] is understood to include a convention to avoid binding free variables in τ.

A sentence σ is called provable if ⊤ ⊢ σ, also written ⊢ σ. For a theory 𝕋, the notions of 𝕋-entailment and 𝕋-provability are given by adding the rules ⊢ σ for each axiom σ of 𝕋.

The classical entailment relation ⊢^{c} results from ⊢ by adding the rule

⊢^{c} ∀p.p ∨ ¬p.

Remark 1. It is sometimes convenient to give a more succinct statement of the logical calculus by defining some of the logical primitives in terms of others. We mention one particularly simple primitive basis which will be useful in the next section (cf. [11]). Exponential types Z^{Y} occur only in the form 2^{Y} (“power types”, usually written P (Y)); λ-terms λx.φ and evaluations α(τ) are then restricted accordingly, and more naturally written {x|φ} and τ ∈ α. Projection operators π_{i}(τ) are eliminated in favor of additional rules of inference. The logical operations ⊤, ⊥, ¬, ∧, ∨, ⇒, ∀, ∃ are defined in terms of = and ⟨−, −⟩, {x|−}, ∈. We shall use the fact that this primitive basis suffices in the following way: to interpret the language of a theory it suffices to interpret the basic language, the type of formulas, product and power types, and the term-forming operations ⟨−, −⟩, {x|−}, ∈, =.

In the opposite direction, one can enlarge the primitive logical basis by including basic relation and function symbols in addition to basic constant symbols, although these are not needed in the presence of higher relation types. Relation symbols will be useful in §4, however, where there is no type of formulas; and both relation and function symbols are used in elementary logic, where there are no higher types at all.

2 Semantics in topoi

Let 𝕋 be a theory in classical higher-order logic, as defined in the foregoing section. It is fairly obvious how to interpret 𝕋 in an arbitrary boolean topos B: An interpretation M of 𝕋 in B assigns to each basic type symbol X an object X_{M} of B, and to the type 2 of formulas, the coproduct 1_{B} + 1_{B} in B (which is the subobject classifier),

2_{M} = 1_{B} + 1_{B}.

The interpretation M is then extended to product and power types by setting

(Y × Z)_{M} = Y_{M} × Z_{M}  (product in B),
(2^{Y})_{M} = (2_{M})^{(Y_{M})}  (exponential in B).

On terms, M assigns to each basic constant symbol c of 𝕋, having say type Z, a morphism

c_{M}: 1_{B} → Z_{M}

of B, and variables are interpreted as identity morphisms. The interpretation is then extended inductively to all terms in L(𝕋) in the evident way, using the internal logic of B (cf. [12, §§VI.5–7], also for the external meaning of the logical operations thus modeled). For example,

(τ = τ′)_{M} = δ ∘ ⟨τ, τ′⟩_{M},

where δ: Z_{M} × Z_{M} → 1_{B} + 1_{B} classifies the diagonal morphism

Δ = ⟨1_{Z_{M}} , 1_{Z_{M}} ⟩: Z_{M} ↣ Z_{M} × Z_{M},

when Z is the type of the terms τ, τ′.

In particular, M assigns to each formula φ(y_{1}, …, y_{n}) with free variables y_{i} of types Y_{i} a morphism

φ(y_{1}, …, y_{n})_{M}: (Y_{1})_{M} × … × (Y_{n})_{M} ⟶ 1_{B} + 1_{B}

of B. A sentence σ is said to be true in M, written M ⊧ σ, if

σ_{M} = true: 1_{B} → 1_{B} + 1_{B},

where true: 1_{B} → 1_{B} + 1_{B} is the first coproduct inclusion, which is the universal subobject. Of course, an interpretation M is a model of 𝕋 if each axiom of 𝕋 is true in M.

2.1 Representing the category of models

Given models M and N of a theory 𝕋 in a boolean topos B, there is an evident notion of an isomorphism h: M ⟶^{∼} N of 𝕋-models, namely a family of isos h = (h_{X}: X_{M} ⟶^{∼} X_{N}) (indexed by the basic types X of 𝕋) that preserve the interpretations of the constant symbols of 𝕋, in the obvious sense. Together with the evident composites and identities, one thus has for any theory 𝕋 and any boolean topos B a category of models of 𝕋 in B, denoted

Mod_{𝕋}(B).

Observe that Mod_{𝕋}(B) is always a groupoid, i.e. a category in which every morphism is iso. For example, if 𝕋 is the theory of topological spaces and B is the topos Sets, then Mod_{𝕋}(B) is the category of all topological spaces and homeomorphisms. One can of course also consider other morphisms of models, but the groupoid of isomorphisms suffices for our purposes.

A logical morphism between boolean topoi plainly preserves models and their morphisms. Such a functor f: B → B′ therefore induces a functor

Mod_{𝕋}(f): Mod_{𝕋}(B) → Mod_{𝕋}(B′)

(a groupoid homomorphism) on the associated categories of models.

Now, every theory 𝕋 in classical higher-order logic has a (higher-order) classifying topos, a boolean topos B_{𝕋} determined uniquely (up to equivalence) by the property: for any boolean topos B there is an equivalence of categories, natural in B,

Log(B_{𝕋}, B) ≃ Mod_{𝕋}(B), (1)

where Log(B_{𝕋}, B) is the category of logical morphisms B_{𝕋} → B and natural isomorphisms between them (cf. [2]). The classifying topos B_{𝕋} can be constructed “syntactically” from L(𝕋) in the style of [4, 11]; in particular, it is a small category (indeed, it is countable). In virtue of its universal mapping property (1), B_{𝕋} is freely generated as a boolean topos by the “universal model” U_{𝕋} ∈ Mod_{𝕋}(B_{𝕋}) associated to the identity logical morphism B_{𝕋} → B_{𝕋} under (1). By the syntactic construction of B_{𝕋} this universal model has the following properties, which we record for later use:

Proposition 2. (i) For any sentence σ ∈ L(𝕋),

𝕋 ⊢^{c} σ just if U_{𝕋} ⊧ σ.

(ii) For any types Y and Z and any morphism f: Y_{U_{𝕋}} → Z_{U_{𝕋}} in B_{𝕋}, there is a formula φ(y, z) ∈ L(𝕋) such that

graph(f) = {⟨y, z⟩ | φ(y, z)}_{U_{𝕋}}

(as subobjects of Y_{U_{𝕋}} × Z_{U_{𝕋}}).

Observe that (i) of proposition 2 and the universal mapping property (1) together entail the soundness and completeness of the deductive calculus of §1 with respect to topos semantics: 𝕋 ⊢^{c} σ if and only if for every 𝕋-model M, M ⊧ σ.

2.2 Classical semantics

We now extend the foregoing topos semantics for classical higher-order logic to non-boolean topoi. Let 𝕋 be a fixed theory and E an arbitrary topos. We begin with a bit of notation: Let true: 1_{E} → Ω_{E} be the subobject classifier in E, and let us write

|−| = (true, false): 1_{E} + 1_{E} ⟶ Ω_{E}

for the canonical map from the coproduct which, observe, is a monomorphism. An arbitrary morphism φ: E → Ω_{E} of E factors through |−| just if the subobject S_{φ} ↣ E it classifies is complemented, i.e. if there is a subobject S ↣ E with S_{φ} + S ≅ E (canonically). When this is the case, let us write \overline{φ}: E → 1_{E} + 1_{E} for the unique morphism such that

φ = |\overline{φ}|,

as indicated in

E \overline{φ} ^{>} 1_{E} + 1_{E}
[figure: φ]
Ω_{E}.^{^{∨} |−|}

Recall that an object E of E is said to be decidable if its diagonal Δ: E ↣ E × E is complemented, thus just if \overline{δ}: E × E → 1_{E} + 1_{E} exists.

Next, we define an interpretation of the basic language of 𝕋 in E exactly as in a boolean topos; in particular the type 2 of formulas is interpreted as 1_{E} + 1_{E}, which is plainly decidable. An interpretation M such that for each type symbol Z the object Z_{M} in E is decidable shall be called a classical interpretation (or c-interpretation).

Finally, by remark 1 any c-interpretation M can be extended to all of L(𝕋) exactly as in a boolean topos, by interpreting the term-forming operations ⟨−, −⟩, \{x|−\}, ∈ as before and taking \overline{δ}: Z_{M} × Z_{M} → 1_{E} + 1_{E} to interpret = at each type Z. Thus just as before a c-interpretation M assigns to each formula φ(y_{1}, …, y_{n}) with free variables y_{i} of types Y_{i} a morphism

φ(y_{1}, …, y_{n})_{M}: (Y_{1})_{M} × … × (Y_{n})_{M} ⟶ 1_{E} + 1_{E}.

Definition 3. The relation ⊧^{c} of satisfaction for c-interpretations is defined by:

M ⊧^{c} σ iff |σ_{M}| = true .

Thus a c-interpretation M satisfies a sentence σ just if the following triangle commutes

1_{E}  \overline{σ_{M} _{>}} 1_{E} + 1_{E}
[figure: true]
Ω_{E}.^{^{∨} |−|}

A c-model of the theory 𝕋 is of course a c-interpretation that satisfies the axioms of 𝕋. A c-interpretation M is therefore a c-model just if for each axiom σ the interpretation

σ_{M}: 1_{E} ⟶ 1_{E} + 1_{E}

is the first coproduct inclusion, just as in the boolean case. Indeed, if the topos E is boolean, then every object is decidable, and a c-model in E is the same thing as a model.

Proposition 4 (Soundness). If M is a c-model then for any sentence σ,

𝕋 ⊢^{c} σ implies M ⊧^{c} σ.

Proof. Consider the classifying topos B_{𝕋} with universal model U_{𝕋}. There is an evident functor m : B_{𝕋} → E with M = m(U_{𝕋}) and

σ_{M} = σ_{m(U_{𝕋})} = m(σ_{U_{𝕋}})

for each sentence σ. Although m is not logical if E is not boolean, it still takes true : 1_{B_{𝕋}} → 1_{B_{𝕋}} + 1_{B_{𝕋}} to \overline{true} : 1_{E} → 1_{E} + 1_{E}. The claim thus follows from the soundness of standard topos semantics (in particular, from proposition 2).

Remark 5. If the interpretation Z_{M} is decidable then for any type Y the canonical inclusion (Z_{M})^{(Y_{M})} ↣ Ω^{(Y_{M} ×Z_{M})} factors as indicated in the following diagram.

(1_{E} + 1_{E})^{(Y_{M} ×Z_{M})}

[figure]

(Z_{M})^{(Y_{M})} ^{>  >} Ω^{(Y_{M} ×Z_{M})}^{^{∨} |−|^{(Y_{M} ×Z_{M})}}

Thus even when defined in terms of power types as mentioned in remark 1, the exponential types Z^{Y} are still interpreted as exponentials by a cinterpretation.

3 Topological completeness

In this section we consider small topoi equipped with the finite epi topology. The covering families for this Grothendieck topology on a topos E are finite families of morphisms (C_{i} → E)_{i} such that the canonical map ∐_{i} C_{i} → E is epic. Of the following two technical lemmas, we omit the straightforward proof of the first; its second part is folklore.

Lemma 6. (i) The finite epi topology is subcanonical.

(ii) For each morphism e : E′ → E in E, the sheafified Yoneda embedding y : E → Sh(E) preserves not only the pullback functor e^{∗} : E/E → E/E′, but also its left and right adjoints,

Σ_{e} ⊣ e^{∗} ⊣ Π_{e} : E/E′ → E/E.

(Indeed, this is true for any subcanonical topology on a small category and any locally cartesian closed structure present there.)

Lemma 7. Let F: B → E be a left-exact functor from a boolean topos B to any topos E. If F is continuous for the finite epi topology then it preserves finite coproducts and first-order logic. If F also preserves exponentials, then it preserves c-models.

Proof. An object of a topos has an empty covering family for the finite epi topology just if it is initial; so the continuous functor F preserves initial objects. The coproduct inclusions B_{1}, B_{2} ↣ B_{1} + B_{2} are a covering family of monos with B_{1} ∧ B_{2} = 0 ↣ B_{1} + B_{2}. Since F is also left-exact, it then preserves coproducts as well. Moreover, it then preserves boolean complements of subobjects, whence it preserves negation ¬ since B is boolean. The logical operations ⇒ and ∀ are then also preserved, since in a boolean topos these can be constructed from negation and operations that are preserved by left-exact, continuous functors generally. Finally, if F also preserves exponentials then by the foregoing it preserves the interpretations of all types and the associated term-forming operations, in addition to first-order logic; whence it clearly preserves c-models.

Theorem A will now follow by applying the covering theorem of the appendix, which states that every Grothendieck topos with enough points can be covered by a topological space via a connected, locally connected geometric morphism. We remind the reader that a Grothendieck topos G is said to have enough points if the geometric morphisms p : Sets → G are jointly surjective (i.e. if the inverse images p^{∗} : G → Sets of these are jointly faithful), and that a geometric morphism f^{∗} ⊣ f_{∗}: E → F of topoi is connected if the inverse image functor f^{∗} is full and faithful, and locally connected ([3]: “molecular”) if f^{∗} commutes with Π-functors.

Theorem A. Let 𝕋 be a higher-order theory. There exists a topological space X_{𝕋} and a c-model M of 𝕋 in Sh(X_{𝕋}) such that:

(i) for any sentence σ ∈ L(𝕋),

𝕋 ⊢^{c} σ  if and only if  M ⊧^{c} σ;

(ii) given types Y, Z, every continuous function f: Y_{M} → Z_{M} over X_{𝕋} is definable: there is a formula φ(y, z) ∈ L(𝕋) such that

graph(f) = {⟨y, z⟩|φ(y, z)}_{M}

(as subsheaves of Y_{M} × Z_{M}).

Proof. First, one has the universal model U_{𝕋} in the classifying topos B_{𝕋}, as in §2.1. The Grothendieck topos Sh(B_{𝕋}) of sheaves on B_{𝕋} for the finite epi topology is coherent, and so has enough points (cf. [12]). The covering theorem of the appendix therefore guarantees the existence of a topological space X_{𝕋} and a connected, locally-connected geometric morphism

m: Sh(X_{𝕋}) → Sh(B_{𝕋}).

The inverse image m^{∗}: Sh(B_{𝕋}) → Sh(X_{𝕋}) of m satisfies all hypotheses of the foregoing lemma 7, as does the sheafified Yoneda embedding

y: B_{𝕋} → Sh(B_{𝕋}).

In particular, these functors preserve exponentials since they preserve Πfunctors (using lemma 6). The composite m^{∗} ∘ y: B_{𝕋} → Sh(X_{𝕋}) therefore also satisfies the hypotheses of lemma 7, whence one has the c-model

M = m^{∗} ∘ y(U_{𝕋})

in Sh(X_{𝕋}). Since each of its factors is full and faithful, so is the functor m^{∗} ∘ y; the assertions (i) and (ii) thus follow from proposition 2.

Remark 8. (Infinitary generalizations) Theorem A clearly applies equally to “theories” 𝕋 with infinitely many type and/or constant symbols and/or axioms, since in such cases the foregoing proof can begin with a small topos B_{𝕋} which is a suitable colimit of classifying topoi for (finite) theories. We also merely mention that for the case of infinitary logic, with set-indexed meets and joins of formulas, a theorem analogous to theorem A holds, with complete Heyting algebras in place of topological spaces.

4 λ-logic

What we call λ-logic differs from classical higher-order logic in that it has no type 2 of formulas. Type symbols are now built up inductively from basic type symbols by the operations −×? and −^{?}. Terms are built up inductively from variables, basic constant symbols, and just the term-forming operations ⟨−,?⟩, π_{1}(−), π_{2}(−), λy.(−), and ?(−). Formulas are then constructed from terms and basic relation symbols in the customary way, using the language of first-order logic with equality. Finally, a λ-theory consists of (finitely many) basic type, constant, and relation symbols, and closed formulas in these parameters.

As rules of inference for the (intuitionistic) entailment relation φ ⊢_{x} ψ on formulas one may take a standard deductive calculus for (intuitionistic) many-sorted, first-order logic with equality, augmented by the usual rules for the (typed) λ-calculus. Indeed, the rules given in §1 above are suitable, under the omission of 2(c).

The notion of a model of a λ-theory in a topos is essentially the same as that already given in §2. It is, however, now more natural to interpret basic relation symbols and other formulas by subobjects (rather than their classifying morphisms), as is usually done for first-order logic (cf. [12]). In particular, the equality sign = is interpreted in the standard way as a diagonal morphism, and since classical logic is not being assumed, the notion of a cmodel is not required.

Deduction is clearly sound with respect to such semantics. To show that it is also complete—even with regard to just topological models—one can proceed as in the classical higher-order case in §3:

(i) Construct the syntactic category S_{𝕋} of provable equivalence classes of formulas, to be equipped with the finite epi topology (which is subcanonical).

(ii) Apply the sheafified Yoneda embedding y: S_{𝕋} → Sh(S_{𝕋}) (which preserves λ-logic by lemma 6) to get a full and faithful model in a Grothendieck topos with enough points.

(iii) Apply the covering theorem of the appendix to get a connected, locally connected geometric covering map Sh(X_{𝕋}) → Sh(S_{𝕋}) from a topological sheaf topos Sh(X_{𝕋}).

We leave it to the reader to fill in the details of this sketch to provide the proof of the following.

Theorem B. Let 𝕋 be a λ-theory. There exists a topological space X_{𝕋} and a model M of 𝕋 in Sh(X_{𝕋}) such that:

(i) for any λ-sentence σ in the language of 𝕋,

𝕋 ⊢ σ  if and only if  M ⊧ σ;

(ii) given types Y, Z, every continuous function f: Y_{M} → Z_{M} over X_{𝕋} is definable: there is a λ-formula φ(y, z) in the language of 𝕋 such that

graph(f) = {⟨y, z⟩|φ(y, z)}_{M}

(as subsheaves of Y_{M} × Z_{M}).

Appendix: The spatial cover

In the proofs of theorems A and B, use was made of the following covering theorem for topoi, which is part of theorem 13.5 of [5] (also see [6]; cf. [10] for a related result).

Covering theorem. For any Grothendieck topos G with enough points there is a topological space X_{G} and a connected, locally connected geometric morphism

ϕ: Sh(X_{G}) → G.

Thus in particular the inverse image functor ϕ^{∗}: G → Sh(X_{G}) is fully faithful and preserves exponentials and the internal first-order logic of G.

The purpose of this appendix is to describe the space X_{G} and the covering map ϕ: Sh(X_{G}) → G in the case of principal interest here, namely when G = Sh(B_{𝕋}) for B_{𝕋} the small classifying topos of a (classical) higher-order theory, equipped with the finite epi topology. Thus we consider the situation of theorem A; that of theorem B of course has a similar description. Before going into details, let us mention that in fact there are many different spaces which will do the job, depending on various parameters that one is free to choose. We exhibit here just one such choice, intended to be illuminating.

To begin, recall from [9] that classical higher-order logic is complete with respect to general models, nowadays called Henkin models. The basic feature of a Henkin model M of a theory 𝕋 is that a function type Z^{Y} (or power type 2^{Y}) is interpreted by a subset (Z^{Y})_{M} ⊂ (Z_{M})^{(Y_{M})} of the set of all functions from Y_{M} to Z_{M} (resp. of the power set ℘Y_{M}), rather than by the set itself. Of course, certain closure conditions also have to be satisfied. We mention only by the way that such models can be shown to arise “naturally” as images of the universal model U_{𝕋} under continuous, left exact functors B_{𝕋} → Sets, and that the said completeness can be inferred from this fact. For the following, it will be convenient to define the underlying set or universe |M| of a Henkin model M to be the (disjoint) union of the sets Z_{M} for all types Z,

|M| = ⋃{Z_{M} | Z a type}.

To define the space X_{𝕋} for the topos Sh(B_{𝕋}), fix a sufficient set S_{𝕋} of countable Henkin models M of 𝕋, i.e. S_{𝕋} satisfies:

M ⊧ σ for all M ∈ S_{𝕋} implies 𝕋 ⊢ σ

for all 𝕋-sentences σ. For example, we could take (a set of representatives of) all countable Henkin models of 𝕋 as the set S_{𝕋}. We then define a labeling of a Henkin model M in S_{𝕋} to be a partial function

ℕ ⊃ dom(α) ⟶^{α} |M|

such that for each a ∈ |M| the fiber α^{−1}(a) is infinite.

The points of the space X_{𝕋} are labeled Henkin models in S_{𝕋}, i.e. pairs

(M, α)

where M ∈ S_{𝕋} and α is a labeling of M. The topology is generated by basic open sets of the form

U_{φ(z̄),n̄} = \{(M, α) | \begin{matrix}α(n_{i}) is defined and of type Z_{i}, \\ and M ⊧ φ(α(n_{1}), …, α(n_{m})) \} \end{matrix}

for φ(z̄) = φ(z_{1}, …, z_{m}) a 𝕋-formula and n̄ = (n_{1}, …, n_{m}) a tuple of natural numbers.

To describe the covering map ϕ: Sh(X_{𝕋}) → Sh(B_{𝕋}) we sketch the construction of the c-model Φ in Sh(X_{𝕋}) induced by ϕ^{∗}. Here we use the equivalence, mentioned in the introduction, Sh(X_{𝕋}) ≃ Etale/X_{𝕋} of sheaves on X_{𝕋} and étale bundles over X_{𝕋}. For each type Z we have the set

Z_{Φ} = ∑_{(M,α)∈X_{𝕋}} Z_{M},

with the evident projection

π_{Z}: Z_{Φ} → X_{𝕋}.

We generate a topology on Z_{Φ} by declaring to be open:

• the sets π_{Z}^{−1}(U) for U ⊂ X_{𝕋} open (thus making π_{Z} continuous),

• the sets V_{n} = {(M, α, a) | a ∈ Z_{M}, α(n) is defined, and α(n) = a}.

It is easily checked that π_{Z} then becomes a local homeomorphism (an étale map). The assignment Z ↦ Z_{Φ} extends in the obvious way to a left exact, continuous functor B_{𝕋} → Sh(X_{𝕋}) that preserves exponentials, inducing the covering map ϕ: Sh(X_{𝕋}) → Sh(B_{𝕋}). Finally, the stalk x^{∗}Φ of the c-model Φ at a point x = (M, α) of X_{𝕋} is just the Henkin model M itself, which gives the relationship between our results and [9].

References

[1] S. Awodey, Topological representation of the λ-calculus, in preparation.

[2] , Logic in topoi: Functorial semantics for higher-order logic, Ph.D. thesis, The University of Chicago, 1997.

[3] M. Barr and R. Paré, Molecular toposes, Journal of Pure and Applied Algebra 17 (1980), 127–152.

[4] A. Boileau and A. Joyal, La logique des topos, Journal of Symbolic Logic 46 (1981), 6–16.

[5] C. Butz, Logical and cohomological aspects of the space of points of a topos, Ph.D. thesis, Universiteit Utrecht, 1996.

[6] C. Butz and I. Moerdijk, Topological representation of sheaf cohomology of sites, Tech. report, Universiteit Utrecht, 1996.

[7] A. Church, A foundation for the simple theory of types, Journal of Symbolic Logic 5 (1940), 56–68.

[8] M. P. Fourman and D. S. Scott, Sheaves and logic, Applications of Sheaves (M. P. Fourman, C. Mulvey, and D. S. Scott, eds.), LNM 753, Springer, 1977, pp. 302–401.

[9] L. Henkin, Completeness in the theory of types, Journal of Symbolic Logic 15 (1950), 81–91.

[10] A. Joyal and I. Moerdijk, Toposes as homotopy groupoids, Advances in Mathematics 80 (1990), 22–38.

[11] J. Lambek and P. J. Scott, Introduction to higher-order categorical logic, Cambridge University Press, 1986.

[12] S. Mac Lane and I. Moerdijk, Sheaves in geometry and logic: A first introduction to topos theory, Springer, 1992.

Recent BRICS Report Series Publications

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.