BRICS RS-96-3 J. van Oosten: The Modi�ed Realizability Topos

BRICS

Basic Research in Computer Science

The Modi�ed Realizability Topos

Jaap van Oosten

BRICS Report Series RS-96-3 ISSN 0909-0878 February 1996 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1996, 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 publications in the BRICS Report Series. 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 WWW and anonymous FTP:

http://www.brics.dk/
ftp ftp.brics.dk (cd pub/BRICS)

The Modified Realizability Topos

Jaap van Oosten

BRICS^{∗}

Department of Computer Science, University of Aarhus Denmark

February 2, 1996

Abstract

The modified realizability topos is the semantic (and higher order) counterpart of a variant of Kreisel’s modified realizability (1957). These years, this realizability has been in the limelight again because of its possibilities for modelling type theory (Streicher, Hyland-Ong-Ritter) and strong normalization.

In this paper this topos is investigated from a general logical and topostheoretic point of view. It is shown that Mod (as we call the topos) is the closed complement of the effective topos inside another one; this turns out to have some logical consequences. Some important subcategories of Mod are described, and a general logical principle is derived, which holds in the larger topos and implies the well-known Independence of Premiss principle.

Introduction. The notion of “modified realizability” originates with Kreisel’s [Kre57] (see also [Kre62]). While Kreisel intended to give a consistency proof for the system HA^{ω} and, accordingly, defined a straightforward extension of Kleene’s realizability to this typed system, today’s meaning of the term ‘modified realizability’ derives from Troelstra’s collapse of this realizability ([Tro73]). Let me briefly indicate what this is.

In Kreisel’s notion, one defines for each formula φ of HA^{ω} a type τ(φ); realizers of φ have to be found in this type. For example, τ(∃x^{σ}.φ) = σ × τ(φ) and τ(φ → ψ) = τ(φ) → τ(ψ).

Now it is possible to interpret the whole of HA^{ω} in first order arithmetic HA, using the model of hereditarily recursive operations. Then one expresses Kreisel’s realizability in HA, and since HA is a subsystem of HA^{ω}, one obtains another realizability interpretation for HA, very different from Kleene’s one.

∗Basic Research in Computer Science, center of the Danish National Research Foundation.

Part of the research was carried out at the Department of Mathematics of Utrecht University, The Netherlands

The resulting interpretation is formulated with ‘potential’ and ‘actual’ realizers; the set of potential realizers of a formula φ is the collapse of the type τ(φ), and the actual realizers are a subset of these. In the following formal definition, U_{a}(φ) and U_{p}(φ) are the sets of, respectively, the actual and potential realizers of φ, and for subsets A, B of IN we use the abbreviations:

\begin{aligned}A × B & = & \{⟨a, b⟩| a ∈ A, b ∈ B\} \\ A → B & = & \{e| ∀a ∈ A∃n.T (e, a, n) & U(n) ∈ B\} \end{aligned}

Then by induction, the first clause for prime formulas:

U_{a}(P) = {n ∈ IN|P }  U_{p}(P) = IN
U_{a}(φ ∧ ψ) = U_{a}(φ) × U_{a}(ψ)  U_{p}(φ ∧ ψ) = U_{p}(φ) × U_{p}(ψ)
U_{a}(φ → ψ) = U_{a}(φ) → U_{a}(ψ)∩
U_{p}(φ) → U_{p}(ψ)  U_{p}(φ → ψ) = U_{p}(φ) → U_{p}(ψ)
U_{a}(∃xφ) = ⋃_{n∈IN}[{n} × U_{a}(φ(n))]  U_{p}(∃xφ) = ⋃_{n∈IN}[{n} × U_{p}(φ(n))]
U_{a}(∀xφ) = ⋂_{n∈IN}[{n} → U_{a}(φ(n))]  U_{p}(∀xφ) = ⋂_{n∈IN}[{n} → U_{p}(φ(n))]

In this definition, the intersection in the clause defining U_{a}(φ → ψ) reflects Kreisel’s definition that τ(φ → ψ) = τ(φ) → τ(ψ) i.e. realizers of an implication must be global elements of this function type. Of course, the clause is also reminiscent of the definition of intuitionistic implication in a Kripke structure: φ → ψ is only true in a node p if for all q ≥ p, if φ is true in q then ψ is true in q.

The following observation is basically due to Troelstra.

Proposition 0.1 Suppose our Gödel numbering of partial recursive functions and our primitive recursive, bijective pairing is such that:

\begin{matrix}φ_{0}(x) = 0 for all x \\ ⟨0, 0⟩ = 0 \end{matrix}

Then 0 ∈ U_{p}(φ) for all φ.

From this observation, Grayson, in an unpublished manuscript ([Gra81]), gave a sketch how to build a modified realizability tripos and consequently a topos, in de style of Hyland’s ([Hy82]) effective topos.

In my thesis ([vO91]) I filled in some details left blank by Grayson, and I observed that the Grayson topos is a sheaf subtopos of “the effective topos built over Set^{→}”.

In the nineties, interest in modified realizability was revived. Streicher ([Str93]) links the idea of actual and potential realizers to an interpretation of fully intensional type theory, via his category of modified assemblies.

Hyland and Ong ([HyO93], see also Ong & Ritter, [OR94]) give an account of modified realizability toposes based on conditional partial combinatory algebras. They develop some theory, analogous to [Hy82], and record the, at first sight surprising fact that there are two embeddings of Set into the modified realizability topos: one is the “logical” one, defined from the logic of the tripos; and the other is the direct image of the embedding of Set as ¬¬-sheaves in the topos.

Among others, this fact is accounted for in this paper. After setting up the topos, I relate it to the topos Eff_{·→·} which is the “effective topos constructed on sheaves over Sierpinski space”, Set^{·→·}, and show that the modified realizability topos, called Mod, is the closed complement of the effective topos in Eff_{·→·}. The two embeddings of Set into Mod come from the two points of Sierpinski space.

Some important subcategories of Mod are described, and Streicher’s Modified Assemblies turn out to live (as a full subcategory) in Eff_{·→·} rather than Mod. The projectives in Mod are described. Mod is, like many realizability toposes, an exact completion.

A generalization of Troelstra’s “Independence of Premiss” principle (see [Tro73]), formulated in the context of Eff_{·→·}, is derived.

1 Definition of Mod and basic properties

This section contains some tripos-theoretic terminology. In sofar as this remains unexplained, the reader is referred to [HJP80].

Convention. From now on we assume the conditions of proposition 0.1 to hold, i.e. 0·x = 0 (that’s how we’ll write partial recursive application) and ⟨0, 0⟩ = 0. We also use the abbreviations A → B and A × B for subsets A, B of IN, as defined in the introduction, and (·)_{0}, (·)_{1} for inverses of the pairing: z = ⟨(z)_{0}, (z)_{1}⟩.

Let R be the set {U = (U_{a}, U_{p}) ∈ P(IN)^{2}| U_{a} ⊆ U_{p} & 0 ∈ U_{p}}. For U, V ∈ R we put

U ⇒ V = (U_{a} → V_{a} ∩ U_{p} → V_{p}, U_{p} → V_{p})

For every set X we define a preorder on R^{X} by:

φ ⊢ ψ iff ⋂_{x∈X}(φ(x) ⇒ ψ(x))_{a} ≠ ∅

Apart from ⇒ we have the following operations on R^{X}:

\begin{aligned}φ ∧ ψ & = & λx.(φ(x)_{a} × ψ(x)_{a}, φ(x)_{p} × ψ(x)_{p}) \\ φ ∨ ψ & = & λx.(φ(x)_{a} + ψ(x)_{a}, φ(x)_{p} + ψ(x)_{p}) \end{aligned}

where, for A, B ⊆ IN, A + B = ({0} × A) ∪ ({1} × B).

Moreover, we have the elements ⊤_{X} = λx.(IN, IN) and ⊥_{X} = λx.(∅, IN).

Proposition 1.1 With the structure (⇒, ∧, ∨, ⊤_{X}, ⊥_{X}), R^{X} is a Heyting prealgebra.

Given f : X → Y there is a order-preserving map R^{Y} →^{R^{f}} R^{X}. This map has both adjoints. Define for φ ∈ R^{X}:

\begin{aligned}∀f(φ) & = & λy.(⋂_{f(x)=y} IN → φ(x)_{a}, ⋂_{f(x)=y} IN → φ(x)_{p}) \\ ∃f(φ) & = & λy. \{ \begin{matrix}(\{i\}, \{i, 0\}) ∧ (⋃_{f(x)=y} φ(x)_{a}, ⋃_{f(x)=y} φ(x)_{p}) & f^{−1}(y) ≠ ∅ \\ (∅, \{0\}) & f^{−1}(y) = ∅ \end{matrix} \end{aligned}

where i is some fixed, standard code for the identity function. We have that ∃f ⊣ R^{f} ⊣ ∀f; by way of example I show the first adjunction.

Suppose ∃f(φ) ⊢_{Y} ψ, say n ∈ ⋂_{y∈Y} (∃f(φ)(y) ⇒ ψ(y))_{a}. Then

λm.n·⟨i, m⟩ ∈ ⋂_{x∈X}(φ(x) ⇒ ψ(f(x)))_{a}

for let m ∈ φ(x)_{a}, then ⟨i, m⟩ ∈ ∃f(φ(f(x))_{a} so n·⟨i, m⟩ ∈ ψ(f(x))_{a}; same calculation for m ∈ φ(x)_{p}; therefore φ ⊢ R^{f}(ψ).

Conversely suppose φ ⊢ R^{f}(ψ), say n ∈ ⋂_{x∈X}(φ(x) ⇒ ψ(f(x)))_{a}. Then

w = λz.(z)_{0}·(n·(z)_{1}) ∈ ⋂_{y∈Y} (∃f(φ)(y) ⇒ ψ(y))_{a}

for let y ∈ Y, z ∈ ∃f(φ)(y)_{a}. Then f^{−1}(y) ≠ ∅ and z is of form ⟨i, (z)_{1}⟩ with (z)_{1} ∈ ⋃_{f(x)=y} φ(x)_{a} whence

n·(z)_{1} ∈ ⋃_{f(x)=y} ψ(f(x))_{a} = ψ(y)_{a}

so w·z = (z)_{0}·(n·(z)_{1}) = n·(z)_{1} ∈ ψ(y)_{a}. Moreover, if z ∈ ∃f(φ)(y)_{p} then either f^{−1}(y) = ∅ in which case z = 0 = ⟨0, 0⟩, n·0 is defined since we may assume X ≠ ∅ (if X = ∅ there is nothing to prove) and n ∈ ⋂_{x∈X} φ(x)_{p} → ψ(f(x))_{p}, whence w·z = 0·(n·0) = 0 ∈ ψ(y)_{p}; or f^{−1}(y) ≠ ∅ in which case (z)_{0} ∈ {i, 0} and (z)_{1} ∈ φ(x)_{p} for some x with f(x) = y. Then n·(z)_{1} is defined and n·(z)_{1} ∈ ψ(y)_{p} so (z)_{0}·(n·(z)_{1}) is either 0 or n·(z)_{1}, in both cases in ψ(y)_{p}. So ∃f(φ ⊢_{Y} ψ.

However, if f is surjective, as most projections are, ∃f(φ) and ∀f(φ) are isomorphic to λy.(⋃_{f(x)=y} φ(x)_{a}, ⋃_{f(x)=y} φ(x)_{p}) and λy.(⋂_{f(x)=y} φ(x)_{a}, ⋂_{f(x)=y} φ(x)_{p}).

Proposition 1.2 The assignment X ↦ R^{X}, (X →^{f} Y) ↦ R^{f}, defines a tripos on Set.

We call the topos represented by this tripos, Mod.

We shall have use for the following general construction. For this, it is necessary to know that the notion of a tripos is valid over any category C with finite limits (finite products suffice, in fact), not just Set; if P is a tripos on C, the topos represented by P is called P−C.

The “constant objects” functor is the functor Δ or Δ_{P} : C → P−C defined on objects by Δ(x) = (x, ∃δ(⊤_{x})) where δ : x → x × x is the diagonal, and on maps by: Δ(x →^{f} y) is the map represented by the functional relation ∃_{⟨id_{x},f⟩}(⊤_{x}) ∈ P(x × y). The following theorem is due to Andy Pitts ([Pit81]):

Theorem 1.3 Suppose P is a tripos on C and R a tripos on P−C such that Δ_{R} : P−C → R−(P−C) preserves epimorphisms. Then the composite R ∘ Δ_{P}^{op} (as a pseudofunctor: C^{op} → Cat) is a tripos on C, and the toposes R−(P−C) and (R∘Δ_{P}^{op})−C are equivalent by an equivalence which commutes with the Δ’s involved.

We only use this theorem to obtain the following easy consequence:

Corollary 1.4 Let S be the set {(A, B) ∈ P(IN)^{2}| A ⊆ B} and define ⇒ on S just as for R, as well as the preorder on S^{X}.

The assignment X ↦ S^{X} yields a Set-tripos, and the topos represented by this tripos is the effective topos built on Set^{·→·}, which we denote by Eff_{·→·}

Proposition 1.5 There is a geometric inclusion of triposes \xymatrix{R^{X} \ar[r] & S^{X} \ar[l]} ; hence, Mod is a sheaf subtopos of Eff_{·→·}

Proof. Since R ⊂ S we have R^{X} ⊂ S^{X}. Left adjoint to this is the map induced by the function Φ : S → R:

Φ(A, B) = (A^{+}, B^{+} ∪ {0})

where A^{+} = {a + 1| a ∈ A}. The adjunction is immediate, and Φ^{X} preserves finite meets.

There is, in complete analogy to the inclusion Set → Eff, an inclusion of toposes Set^{·→·} → Eff_{·→·}. Let (∇_{2})_{∗} : Set^{·→·} → Eff_{·→·} be defined as follows: (∇_{2})_{∗}(X →^{α} Y) = (X ⊔ Y, =) where X ⊔ Y is the disjoint union of X and Y, and

[[ z = z′]] = \{ \begin{matrix}(IN, IN) & if z, z′ ∈ X and z = z′ (1) \\ (∅, IN) & if not (1), but [ \begin{matrix}α \\ id \end{matrix} ] (z) = [ \begin{matrix}α \\ id \end{matrix} ] (z′) ∈ Y \\ (∅, ∅) & otherwise \end{matrix}

For a morphism γ = [figure: X; γ_{0}; α; X′; α′; Y; γ_{1}; Y′] its image (∇_{2})_{∗}(γ) is represented by the functional relation F ∈ S^{(X⊔Y)×(X′⊔Y′)} where

F (z, z′) = \{ \begin{matrix}(IN, IN) & if z ∈ X, z′ ∈ X′ and γ_{0}(z) = z′ (1) \\ (∅, IN) & if not (1), but γ_{1} ∘ [ \begin{matrix}α \\ id \end{matrix} ] (z) = [ \begin{matrix}α′ \\ id \end{matrix} ] (z′) ∈ Y′ \\ (∅, ∅) & otherwise \end{matrix}

For (X, =) an object of Eff_{·→·}, write =_{0}, =_{1} for the two components of =, i.e. [[ x = x′]] = ([[ x =_{0} x′]], [[ x =_{1} x′]]). Then (∇_{2})^{∗}(X, =) is X_{0} →^{d} X_{1} where X_{i} = {x ∈ X| [[ x =_{i} x]] ≠ ∅}/ ∼_{i}, x ∼_{i} x′ iff [[ x =_{i} x′]] ≠ ∅, and d the obvious map.

There are two embeddings from Set into Mod. The constant objects functor Δ sends the set X to (X, =_{Δ}) where

[[ x =_{Δ} x′]] = \{ \begin{matrix}(\{i\}, \{i, 0\}) & if x = x′ \\ (∅, \{0\}) & if x ≠ x′ \end{matrix}

There is another functor, ∇ : Set → Mod, defined by ∇(X) = (X, =_{∇}) where

[[ x =_{∇} x′]] = \{ \begin{matrix}(IN, IN) & if x = x′ \\ (∅, IN) & if x ≠ x′ \end{matrix}

As noted by Hyland and Ong, since the topos R^{(−)} is ∃-standard (see [HJP80]), by 4.5 of that paper ∇ is direct image of a geometric morphism Set → Mod, the inverse image of which is the global sections functor. This geometric morphism is an inclusion, and presents Set as ¬¬-sheaves in Mod.

The topos Set^{·→·}, being sheaves over Sierpinski space, has two points 0, 1 : Set → Set^{·→·}. We have 0_{∗}(X) = (X →^{id} X), 1_{∗}(X) = (X →^{!} 1), 0^{∗}(X →^{f} Y) = Y and 1^{∗}(X →^{f} Y) = X. Moreover, there is a 2-cell α : 1 ⇒ 0 (Recall that in the 2-category Top of toposes and geometric morphisms, a 2-cell α : f ⇒ g is a natural transformation α^{∗} : f^{∗} ⇒ g^{∗}, equivalently, a natural transformation α_{∗} : g_{∗} ⇒ f_{∗}). Let us denote the inclusion Mod → Eff_{·→·} by i.

Proposition 1.6 The functors ∇ and Δ are isomorphic to i^{∗}(∇_{2})_{∗}1_{∗} and i^{∗}(∇_{2})_{∗}0_{∗} respectively.

Proof. Easy verification.

We can extend the picture. We have also a geometric morphism Eff →^{δ} Eff_{·→·}, induced by the diagonal embedding of P(IN) into S and the map back, which sends (U, V) to V.

Moreover there is a geometric morphism v : Mod → Eff induced by the maps (U, V) ↦ U : R → P(IN) and A ↦ (A^{+}, A^{+} ∪ {0}) : P(IN) → R. The triangle of geometric morphisms:

[figure: Mod; i; v; Eff_{·→·}; Eff; δ]

does not commute, but there is a 2-cell β : i ⇒ δv. The component β^{∗} : i^{∗} ⇒ v^{∗}δ^{∗} is induced by the entailment (U^{+}, V^{+} ∪ {0}) ⊢ (V^{+}, V^{+} ∪ {0}) in R^{1}; i.e., β^{∗} is the composition

i^{∗} ⇒^{i^{∗}η} i^{∗}δ_{∗}δ^{∗} ⇒^{β^{∗}δ_{∗}δ^{∗}} w^{∗}δ^{∗}δ_{∗}δ^{∗} ≅ w^{∗}δ^{∗}

where the last two arrows are isomorphisms. Therefore, β^{∗} is an isomorphism on objects in the image of δ_{∗}, i.e.

β^{∗} ⋆ δ_{∗} : i^{∗}δ_{∗} ⇒ v^{∗}δ^{∗}δ_{∗} ≅ v^{∗}

is an isomorphism.

Let us denote the inclusions of Set into Mod and Eff by ∇_{E}, ∇_{M} respectively.

Proposition 1.7 The diagrams

[figure: Mod; i; Eff_{·→·}; Set; ∇_{M}; 1; _{Set_{·→·}}; ∇_{2}; Eff; δ; Eff_{·→·}; Set; ∇_{E}; 0; _{Set_{·→·}}; ∇_{2}; Mod; v; Eff; Set; ∇_{M}; ∇_{E}]

commute up to natural isomorphism. Moreover, the 2-cells ∇_{2}α and β ⋆ ∇_{M} coincide modulo these natural isomorphisms, i.e. the composites

∇_{2} ∘ 1 ⇒^{∇_{2}α} ∇_{2} ∘ 0

and

∇_{2} ∘ 1 ≅ i ∘ ∇_{M} ⇒^{β⋆∇_{M}} δ ∘ v ∘ ∇_{M} ≅ δ ∘ ∇_{E} ≅ ∇_{2} ∘ 0

are equal.

It follows, that the functor Δ : Set → Mod is isomorphic to v^{∗}(∇_{E})_{∗}, for we have

Δ ≅ i^{∗}(∇_{2})_{∗}0_{∗} ≅ i^{∗}δ_{∗}(∇_{E})_{∗} ⇒^{β^{∗}⋆δ_{∗}(∇_{E})_{∗}} v^{∗}δ^{∗}δ_{∗}(∇_{E})_{∗} ≅ v^{∗}(∇_{E})_{∗}

and we know that β^{∗} ⋆ δ_{∗} is a natural isomorphism.

2 Eff and Mod as subtoposes of Eff_{·→·}

Let U = ({∗}, =) be the subobject of 1 in Eff_{·→·} defined by [[ ∗ = ∗]] = (∅, IN).

Proposition 2.1 1. Eff is the open subtopos of Eff_{·→·} determined by the object U, and Mod is its closed complement;

2. The two commuting squares in proposition 1.7 are pullback squares in Top.

Proof. We have 5 internal topologies in Eff_{·→·} which I denote by k_{0}, k_{1}, k_{2}, k_{E}, k_{M}; they correspond respectively to the inclusions Set →^{∇_{2}0} Eff_{·→·}, Set →^{∇_{2}1} Eff_{·→·},

Set^{·→·} →^{∇_{2}} Eff_{·→·}, Eff →^{δ} Eff_{·→·} and Mod →^{i} Eff_{·→·}.

For each j ∈ {0, 1, 2, E, M}, k_{j} is induced by a map K_{j} : S → S. These maps are given by:

K_{0}(A, B) = ({n ∈ IN| B ≠ ∅}, {n ∈ IN| B ≠ ∅})
K_{1}(A, B) = ({n ∈ IN| A ≠ ∅}, IN)
K_{2}(A, B) = ({n ∈ IN| A ≠ ∅}, {n ∈ IN| B ≠ ∅})
K_{E}(A, B) = (B, B)
K_{M}(A, B) = (A^{+}, B^{+} ∪ {0})

Now clearly, in S^{S}, the maps K_{E} and (A, B) ↦ ((∅, IN) ⇒ (A, B)) are isomorphic, whence k_{E} is internally given as λw : Ω.u ⇒ w, u being the point of Ω which classifies the inclusion U → 1. By the definition of open subtoposes ([Joh76]), Eff is the open subtopos determined by U. Likewise, the map K_{M} is isomorphic (in S^{S}) to (A, B) ↦ ((∅, IN) ∨ (A, B)), so k_{M} is internally the topology λw : Ω.u ∨ w, which is the complement (in the lattice of internal topologies) of k_{E}. This proves statement 1.

For the second statement, since both diagrams are diagrams of inclusions, it is enough to prove that k_{1} is the join of k_{2} and k_{M}, and k_{0} is the join of k_{2} and k_{E}. This is immediate from the equalities K_{1} = K_{2} ∘ K_{M} and K_{0} = K_{2} ∘ K_{E}.

Corollary 2.2 Every k_{M}-closed subobject is k_{E}-dense, and every map from a k_{M}-separated object to a k_{E}-separated object is constant.

In fact there are two other topologies which belong in the picture, viz. the meets k_{2} ∧ k_{E} and k_{2} ∧ k_{M}. Abusing notation,

k_{2} ∧ k_{E} (A, B) = \{ \begin{matrix}(B, B) & if A ≠ ∅ \\ (∅, B) & else \end{matrix}

and

k_{2} ∧ k_{M} (A, B) = \{ \begin{matrix}(A^{+}, B^{+} ∪ \{0\}) & if B ≠ ∅ \\ (∅, ∅) & else \end{matrix}

and we have

[figure: ⊤ = λw : Ω.⊤; k_{0}; k_{1}; k_{E}; k_{2}; k_{M}; k_{2} ∧ k_{E}; k_{2} ∧ k_{M}; ⊥ = id_{Ω}]

as a sublattice of the lattice of internal topologies in Eff_{·→·}

3 Subobjects of ∇’s, Δ’s and projectives in Mod

In this section I characterize the full subcategories of Mod on respectively: the objects which are subobject of a ∇(X), those which are subobject of a Δ(X) and the projective objects.

The characterization of the sub-∇’s was already given, without proof, by Hyland and Ong. For completeness’ sake and for understanding, I give a proof. The global sections functor Γ : Mod → Set can be rendered as: Γ(X, =) = X_{0}/∼ where X_{0} = {x ∈ X| [[ x = x]]_{a} ≠ ∅} and x∼x′ iff [[ x = x′]]_{a} ≠ ∅; if F : X × Y → R represents a morphism f : (X, =) → (Y, =) then Γ(f) sends the class [x] to the unique class [y] for which F (x, y)_{a} ≠ ∅. Given a function f : Γ(X, =) → Y in Set, its transpose: (X, =) → ∇(Y) is represented by

F (x, y) = \{ \begin{matrix}[[ x = x]] & if x ∈ X_{0} & f([x]) = y \\ (∅, [[ x = x]]_{p}) & o.w. \end{matrix}

Therefore the unit η : (X, =) → ∇Γ(X, =) is represented by H : X ×X_{0}/∼ → R where H(x, [x′]) = [[ x = x]] if x ∈ [x′], and (∅, [[ x = x]]_{p}) otherwise.

Proposition 3.1 For an object (X, =) of Mod, the following are equivalent:

1. η_{(X,=)} is a monomorphism;

2. (X, =) is ¬¬-separated;

3. (X, =) is isomorphic to an object (Y, =) of the form:

[[ y = y′]] = \{ \begin{matrix}(A_{y}, B) & if y = y′ \\ (∅, B) & o.w. \end{matrix}

with A_{y} ≠ ∅ for all y ∈ Y, and B constant (of course, 0 ∈ B and all A_{y} ⊆ B)

Proof. 1 ⇒ 2: suppose η mono, so

H(x, [z]) ∧ H(x′, [z]) ⇒ x = x′

holds. Suppose a is an actual realizer of this. Furthermore suppose b_{0} ∈ [[ x = x]]_{0}, b_{1} ∈ [[ x′ = x′]]_{0} and b_{2} ∈ ¬¬[[ x = x′]]_{0}. Then [x] = [x′], b_{0} ∈ H(x, [x]), b_{1} ∈ H(x′, [x′]) so a·⟨b_{0}, b_{1}⟩ ∈ [[ x = x′]]_{0}; similar for potential realizers. So

x = x ∧ x′ = x′ ∧ ¬¬(x = x′) ⇒ x = x′

holds and (X, =) is ¬¬-separated.

2 ⇒ 3: suppose a is an actual realizer of x = x∧x′ = x′ ∧¬¬(x = x′) ⇒ x = x′. Let Y = Γ(X, =) and put A_{y} = ⋃_{x,x′∈y}[[ x = x′]]_{a} and B = ⋃_{x,x′∈X}[[ x = x′]]_{p}. Then (X, =) and (Y, =) are easily seen to be isomorphic, via F : X ×Y → R where

F (x, y) = \{ \begin{matrix}([[ x = x]]_{a} × A_{y}, [[ x = x]]_{p} × B) & if x ∈ y \\ (∅, [[ x = x]]_{p} × B) & o.w. \end{matrix}

The implication 3 ⇒ 1 is left to the reader.

The full subcategory of Mod on the ¬¬-separated objects can be described as follows: objects are triples (X, {A_{x}| x ∈ X}, B) where X is a set, ∅ ≠ A_{x} ⊆ B ⊆ IN and 0 ∈ B; maps from (X, {A_{x}| x ∈ X}, B) to (Y, {C_{y}| y ∈ Y }, D) are functions f : X → Y such that (⋂_{x∈X} A_{x} → C_{f(x)}) ∩ (B → D) is nonempty.

As to the sub-Δ’s, the description of the objects is almost as simple, but the morphisms are different. Thomas Streicher defined the following category, which he calls the category of modified assemblies ModAss:

Definition 3.2 (Streicher) A modified assembly is a pair (X, ϕ) with X a set and ϕ : X → R such that ϕ(x)_{a} ≠ ∅ for all x ∈ X. A morphism of modified assemblies (X, ϕ) → (Y, ψ) is a function f : X → Y which is tracked in the sense that

⋂_{x∈X}(ϕ(x) ⇒ ψ(f(x)))_{a}

is nonempty. Modified assemblies and morphisms form a category ModAss.

There is, as will be seen explicitly below, an embedding ModAss → Mod which lands in the sub-Δ’s; as (X, ϕ) is sent to a subobject of Δ(X). The question therefore arises whether ModAss is equivalent to the full subcategory of Mod on the sub-Δ’s. There are two obstacles here.

The first one is the requirement that ϕ(x)_{a} ≠ ∅ for all x ∈ X. Consider the object (IN, =) where

[[ n = m]] = \{ \begin{matrix}(\{n + 1\}, \{0, n + 1\}) & if n = m & n ∈ K \\ (∅, \{0, n + 1\}) & if n = m & n ∉ K \\ (∅, \{0\}) & else \end{matrix}

(K is the halting set) Clearly, (IN, =) is a subobject of Δ(IN) but it is not isomorphic to any object in the image of ModAss, since that would imply the decidability of K.

The other obstacle is that the embedding ModAss → Mod is not full. Consider the two objects (X, ϕ) and (Y, ψ) of ModAss with X = {x_{1}, x_{2}}, Y = {y_{1}, y_{2}}, ϕ(x_{1}) = ψ(y_{1}) = ({1}, {0, 1}), ϕ(x_{2}) = ({2}, {0, 1, 2}) and ψ(y_{2}) = ({2}, {0, 2}). There is a morphism in Mod between them, represented by the function F : X × Y → R defined by

\begin{aligned}F (x_{1}, y_{1}) & = & (\{1\}, \{0, 1\}) \\ F (x_{1}, y_{2}) & = & (∅, \{0\}) \\ F (x_{2}, y_{1}) & = & (∅, \{0, 1\}) \\ F (x_{2}, y_{2}) & = & (\{2\}, \{0, 2\}) \end{aligned}

Strictness and totality of F are realized by (a code of) the identity function. Relationality is easy, and single-valuedness is realized by sending the pair ⟨n, m⟩ to n if n = m, and to 0 otherwise. Now this morphism cannot come from a ModAss-morphism which is a function f : X → Y; suppose e ∈ ⋂_{x∈X}(ϕ(x) ⇒ ψ(f(x)))_{a}. Since 1 ∈ ϕ(x_{1})_{a} ∩ϕ(x_{2})_{p}, we must have e·1 ∈ ψ(f(x_{1}))_{a} ∩ψ(f(x_{2}))_{p} which, by inspection of (Y, ψ), implies that f(x_{1}) = f(x_{2}); but then F can not represent the image of f.

Convention. From now on, in talking about ModAss, we drop the requirement on objects (X, φ) that φ(x)_{a} ≠ ∅ for all x ∈ X.

Every φ ∈ R^{X} is automatically a relation for the equality =_{Δ} and determines therefore a subobject of Δ(X), viz. the object (X, =) where [[ x = x′]] = φ(x) ∧ [[ x =_{Δ} x′]], and every subobject of Δ(X) arises in this way.

The predicate φ(x) ∧ [[ x =_{Δ} x′]] is, in R^{X×X}, isomorphic to the function which sends x, x′ to (φ(x)_{a}^{+}, φ(x)_{p}^{+}∪{0}) if x = x′, and to (∅, {0}) else; therefore, every sub-Δ is isomorphic to an object (X, =) where

[[ x = x′]] = \{ \begin{matrix}φ(x) & if x = x′ \\ (∅, \{0\}) & else \end{matrix}

for some φ ∈ R^{X} such that 0 ∉ φ(x)_{a} for all x. I call objects of this form canonical sub-Δ’s.

So every sub-Δ is the i^{∗}-image of an object (X, =_{φ}) of Eff_{·→·} where now

[[ x =_{φ} x′]] = \{ \begin{matrix}φ(x) & if x = x′ \\ (∅, ∅) & else \end{matrix}

for some φ ∈ R^{X} arbitrary. The objects (X, =) of Eff_{·→·} such that [[ x = x′]] = (∅, ∅) whenever x ≠ x′ are precisely the subobjects of some (∇_{2}0)_{∗}(X); the fact that φ ∈ R^{X} rather than S^{X} means that the (X, =_{φ}) are the k_{M}-closed subobjects of objects in the image of (∇_{2}0)_{∗}.

Now any morphism in Eff_{·→·} between such objects is uniquely determined by a function on the underlying sets which is tracked in the sense of ModAss. Therefore we have, noting that (∇_{2}0)_{∗} is the inclusion of the ¬¬-sheaves in Eff_{·→·}:

Proposition 3.3 ModAss is equivalent to the full subcategory of Eff_{·→·} on those objects which are a k_{M}-closed subobject of a ¬¬-sheaf.

The full subcategory of Mod on the sub-Δ’s is a localization of this by a calculus of fractions. Freely invert those arrows in ModAss which are, from the point of view of Eff_{·→·}, k_{M}-almost iso (i.e. their i^{∗}-image is iso). This is because of the isomorphism of Δ and i^{∗}(∇_{2}0)_{∗}: a sub-Δ is the same thing as a k_{M}-closed subobject of some (∇_{2}0)_{∗}(X). Now the sub-Δ’s are closed under products in Mod, so if A →^{f} B is a map between sub-Δ’s in Mod, the graph of f, as subobject of A × B, is also a sub-Δ and corresponds therefore to a k_{M}-closed subobject of some (∇_{2}0)_{∗}(X), with projections to the objects corresponding to A and B respectively, the first being k_{M}-almost iso.

I want to give a concrete description of the sub-Δ’s in terms of ModAss. We need some structure of ModAss (familiar from ordinary assemblies) and a representation of ModAss-morphisms which are, in Eff_{·→·}, k_{M}-dense inclusions.

ModAss is regular: the pullback of [figure: (Y, ψ); g; (Xφ); f; (Z, χ)] is (X ×_{Z} Y, ω) with

ω(x, y) = ⟨φ(x), ψ(y)⟩ and X ×_{Z} Y is the pullback in Set.

A morphism (X, φ) →^{f} (Y, ψ) is regular epi iff

⋂_{y∈Y} (ψ(y) ⇒ ( ⋃_{f(x)=y} φ(x)_{a}, ⋃_{f(x)=y} φ(x)_{p}))_{a} ≠ ∅

To describe the k_{M}-dense inclusions we recall that k_{M} = λω : Ω.u ∨ ω and define:

Definition 3.4 Given an object (X, φ) of ModAss, a relatively recursive subset of φ is a set P such that ⋃_{x∈X} φ(x)_{a} ⊆ P ⊆ ⋃_{x∈X} φ(x)_{p} and there is a partial recursive function f, defined on ⋃_{x∈X} φ(x)_{p}, such that P = (⋃_{x∈X} φ(x)_{p})∩ f^{−1}(0).

Given such P, we define the object (X_{P} , φ_{P}) where X_{P} = {x ∈ X | φ(x)_{p} ∩ P ≠ ∅} and φ_{P} (x) = (φ(x)_{a}, (φ(x)_{p} ∩ P) ∪ {0})

(X_{P} , φ_{P}) is an object of ModAss, the inclusion (X_{P} , φ_{P}) → (X, φ) is k_{M}-dense and every k_{M}-dense mono in ModAss is isomorphic to one of this form.

Proposition 3.5 Let Σ be the class of ModAss-morphisms (X, φ) →^{f} (Y, ψ) such that:

1. There is a relatively recursive subset P of ψ such that f factors as (X, φ) →^{f′} (Y_{P} , ψ_{P}) → (Y, ψ) and f′ is a regular epi in ModAss;

2. if \xymatrix{(Z, χ) \ar[r] \ar[r] & (X, φ)} is the kernel pair of f, there is a relatively recursive subset Q of χ such that the composite (Z_{Q}, χ_{Q}) → (Z, χ) → (Y, ψ) is monic.

Then the full subcategory of Mod on the sub-Δ’s is equivalent to ModAss[Σ^{−1}].

Projectives in Mod. The study of projectives in Mod is facilitated by the fact that the functors i_{∗} : Mod → Eff_{·→·} and (∇_{2})_{∗} : Set^{·→·} → Eff_{·→·} both preserve epi’s; their left adjoints therefore preserve projectives.

As the projectives in Set^{·→·} are exactly the monic arrows in Set, a projective object (X, =) in Eff_{·→·} will have [[ x = x′]]_{p} = ∅ whenever [[ x = x′]]_{a} = ∅, for x ≠ x′. In complete analogy to the situation for Eff (see [RR90]) we arrive at the characterization of projective objects in Eff_{·→·} as, up to isomorphism, objects (X, =) such that [[ x = x′]] = (∅, ∅) if x ≠ x′, and [[ x = x]] is (∅, {n}) or ({n}, {n}) for some n.

Every object of Eff_{·→·} is covered by a projective object so every object of Mod is covered by a projective object. This easily implies that the projectives in Mod are of form (X, =) where [[ x = x′]] = (∅, {0}) if x ≠ x′, and [[ x = x]] is either (∅, {0, n + 1}) or ({n + 1}, {0, n + 1}) for some n: that is, the i^{∗}-image of a projective in Eff_{·→·}.

Suppose F : X × Y → R represents a morphism in Mod between two such objects (X, =) and (Y, =). There are partial recursive functions tot and sv such that

\begin{aligned}tot & ∈ & ⋂_{x∈X}([[ x = x]] ⇒ (⋃_{y∈Y} F (x, y)_{a}, ⋃_{y∈Y} F (x, y)_{p}))_{a} \\ sv & ∈ & ⋂_{x∈X,y,y′∈Y} (F (x, y) ∧ F (x, y′) ⇒ [[ y = y′]])_{a} \end{aligned}

Let P ⊆ ⋃_{x∈X}[[ x = x]]_{p} be defined by

P = {n ∈ ⋃_{x∈X}[[ x = x]]_{p} | sv(⟨tot(n), tot(n)⟩) ≠ 0}

Then P is a relatively recursive subset for [[ · = ·]] since ⋃_{x∈X}[[ x = x]]_{a} ⊆ P.

For X_{P} = {x ∈ X | [[ x = x]]_{p}∩P ≠ ∅}, the predicate F determines a function f : X_{P} → Y. If Y is a one-element set, this is the unique function; if Y has more than one element, since sv(⟨tot(0), tot(0)⟩) = 0, for x ∈ X_{P} and n unique with n + 1 ∈ [[ x = x]]_{p} ∩ P, there is a unique y with tot(n) ∈ F (x, y).

Then the predicate [[ x = x]] ∧ [[ f(x) = y]] is a functional relation which is isomorphic to (the restriction to X_{P} × Y of) F.

Thus we arrive at the following characterization of the projectives in Mod, in the style of [RR90]:

Proposition 3.6 Let C be the category given by:

• Objects are diagrams \xymatrix{X \ar[r] & Y \ar[r] & I} such that X → Y is an injective function of sets and Y → I is a surjection of Y onto a subset of IN;

• morphisms are commuting diagrams

[figure: X; Y; I; φ; X′; Y′; I′]

with φ partial recursive.

Let Σ be the class of morphisms

[figure: X; =; Y′; J; X; Y; I]

for which J → I is an inclusion of a subset which contains the image of X and is moreover such that for some partial recursive f, defned on I, J = I ∩ f^{−1}(0); and the right hand square is a pullback square in Set.

Then the category C[Σ^{−1}] is equivalent to the full subcategory of Mod on the projective objects.

4 A general “Independence of Premiss” principle for Eff_{·→·}

Definition 4.1 Let us call an object (Y, =) of Eff_{·→·} diagonal if

⋂_{y∈Y} ([[ y = y]]_{p} → [[ y = y]]_{a}) ≠ ∅

Every diagonal object is isomorphic to an object (Y, =) such that [[ y = y]] is of the form (A, A). Every k_{E}-sheaf (i.e., object of Eff) is diagonal, but also objects in the image of (∇_{2}1)_{∗} are. All diagonal objects are quotients of k_{E}-sheaves.

Proposition 4.2 An object of Eff_{·→·} is diagonal if and only if its k_{E}-separated reflection is already a k_{E}-sheaf; equivalently, if its canonical map to its k_{E}- sheafification is an epimorphism.

Proposition 4.3 Let (X, =) and (Y, =) be objects of Eff_{·→·} with (Y, =) diagonal; let A(x) a k_{1}-closed subobject of (X, =) and B(x, y) an arbitrary subobject of (X, =) × (Y, =). Then the principle

∀x ∈ (X, =).[(A(x) → ∃y ∈ (Y, =).B(x, y)) → ∃y ∈ (Y, =).(A(x) → B(x, y))]

holds.

Proof. Let’s write E(x), E(y) for [[ x = x]], [[ y = y]].

Since A(x) is k_{1}-closed there is a partial recursive function f such that for all x ∈ X and n ∈ E(x)_{p}, f(n) ∈ [[ A(x) ]]_{p} and moreover, if n ∈ E(x)_{a} and [[ A(x) ]]_{a} is nonempty, then f(n) ∈ [[ A(x) ]]_{a}.

Let g ∈ ⋂_{y∈Y} E(y)_{p} → E(y)_{a} and φ be the partial recursive function

Λn.Λw.⟨g·(w·f(n))_{0}, Λv.(w·f(n))_{1}⟩

I claim that φ is an actual realizer of the principle in the proposition, which I abbreviate as ∀x ∈ (X, =).[Φ(x) → Ξ(x)]. We have to show:

\begin{aligned}1) & n ∈ E(x)_{p} & ⇒ & φ(n) ∈ Φ(x)_{p} → Ξ(x)_{p} \\ 2) & n ∈ E(x)_{a} & ⇒ & φ(n) ∈ Φ(x)_{a} → Ξ(x)_{a} \end{aligned}

As to 1), let n ∈ E(x)_{p}, w ∈ Φ(x)_{p}. Since f(n) ∈ [[ A(x) ]]_{p}, w·f(n) is defined and in [[ ∃y ∈ (Y, =).B(x, y) ]]_{p} so for some y ∈ Y, (w·f(n))_{0} ∈ E(y)_{p} and (w·f(n))_{1} ∈ [[ B(x, y) ]]_{p}. Then g·(w·f(n))_{0} ∈ E(y)_{a} ⊆ E(y)_{p}, and Λv.(w·f(n))_{1} ∈ [[ A(x) ]]_{p} → [[ B(x, y) ]]_{p}, so φ(n) ∈ Φ(x)_{p} → Ξ(x)_{p}.

As to 2), let n ∈ E(x)_{a}. We have f(n) ∈ [[ A(x) ]]_{p} and if [[ A(x) ]]_{a} is nonempty, then f(n) ∈ [[ A(x) ]]_{a}. Let w ∈ Φ(x)_{a}.

Again, w·f(n) is defined, and there is y ∈ Y with g·(w·f(n))_{0} ∈ E(y)_{a} and (w·f(n))_{1} ∈ [[ B(x, y) ]]_{p}.

But if v ∈ [[ A(x) ]]_{a} then f(n) ∈ [[ A(x) ]]_{a} so w·f(n) ∈ [[ ∃y ∈ (Y, =).B(x, y) ]]_{a}, i.e. for some y ∈ Y, g·(w·f(n))_{0} ∈ E(y)_{a} and (w·f(n))_{1} ∈ [[ B(x, y) ]]_{a}.

So Λv.(w·f(n))_{1} ∈ [[ A(x) ]]_{a} → [[ B(x, y) ]]_{a}. The rest is left to the reader.

Troelstra ([Tro73]) calls the following principle in arithmetic:

(¬A(x) → ∃y.B(x, y)) → ∃y.(¬A(x) → B(x, y))

the Independence of Premiss principle (IP). He shows that IP is valid under modified realizability (a fact which is also quoted in [HyO93]). This is a consequence of proposition 4.3, since (for u ∈ Ω as in proposition 2.1) u is k_{1}-closed and so is therefore A(x) → u, which is the meaning in Eff_{·→·} of the negation in Mod; and the natural numbers object in Eff_{·→·} is a k_{E}-sheaf, so diagonal.

Further directions

In this section I mention some further issues and topics for research.

4.1 Mod over Eff

Since every object of Mod is a subquotient of some Δ(X) and Δ ∼ v^{∗}∇_{E}, every object of Mod is a subquotient of some v^{∗}(X); this is to say that v : Mod → Eff is localic and that Mod is sheaves (in Eff) on the internal locale v_{∗}(Ω) in Eff. Yet another way of saying this is that Mod is the classifying topos for a propositional theory in Eff.

It would be nice to have a description of this theory. A natural way to start is to look at the object of points of v_{∗}(Ω), but this did not bring me much enlightenment.

4.2 Internal complete categories in Mod

There should be several of these, and it is probably easier to consider them from the point of view of Eff_{·→·}. Hyland and Ong introduce the category of “PERextension pairs”: these are objects (X, {A_{x} | x ∈ X}, B) as in the description of the ¬¬-separated objects in Mod (proposition 3.1), satisfying A_{x} ∩ A_{y} = ∅ for x ≠ y. In Eff_{·→·} these are the k_{1}-separated subquotients of the object (IN, =) with [[ n = m]] = ({n}, IN) if n = m, and (∅, IN) else; that is the k_{1}-separated reflection of the natural numbers object in Eff_{·→·}. A proof that this gives an internal complete category (at least with respect to the ¬¬-separated objects in Mod) should be possible via the orthogonality approach, basically due to Peter Freyd, and given in [HRR90].

4.3 Mod over a c-pca

As Hyland and Ong show, one can build a modified realizability topos over a structure weaker than a partial combinatory algebra, namely a partial applicative structure with elements k and s where the applications sf and sfg need not be defined. They point out that the construction of an effective topos over such a c-pca fails, and for the same reason the construction of Eff_{·→·} fails.

It seems to me legitimate to ask, whether maybe every c-pca U can be embedded in a partial combinatory algebra A such that they yield equivalent modified realizability toposes.

4.4 Axiomatization of modified realizability

A straightforward axiomatization for modified realizability can be given, in a system of first order arithmetic extended by a propositional constant u (for the object U of proposition 2.1). This will be done in a subsequent paper.

Acknowledgement

I am indebted to Thomas Streicher for asking me questions and many discussions.

References

[Gra81] R. Grayson, Modified realisability toposes, manuscript, Münster 1981

[Hy82] J.M.E. Hyland, The Effective Topos, in: A.S. Troelstra & D. van Dalen (eds), The L.E.J. Brouwer Centenary Symposium, North-Holland 1982

[HJP80] J.M.E. Hyland, P.T. Johnstone & A.M. Pitts, Tripos Theory, Math.Proc.Camb.Phil.Soc. 88(1980), 205-232

[HyO93] J.M.E. Hyland & L. Ong, Modified Realizability Toposes and Strong Normalization Proofs, in: M. Bezem & J.F. Groote (eds), Typed Lambda Calculi and Applications, LNCS 664, Springer 1993, pp. 179-194

[Joh76] P.T. Johnstone, Topos Theory, Academic Press 1976

[Kre57] G. Kreisel, Interpretation of Analysis by means of constructive Functionals of finite Types, in: A. Heyting (ed.), Constructivity in Mathematics, North-Holland 1959, pp. 101-128

[Kre62] G. Kreisel, On weak completeness of intuitionistic predicate logic, JSL 27 (1962), Number 2 (June), pp. 139-158

[OR94] L. Ong & E. Ritter, A Generic Strong Normalization Argument: Application to the Calculus of Constructions, in: Computer Science Logic: 7th Workshop CSL ’93, LNCS 832, Springer 1994

[vO91] J. van Oosten, Exercises in Realizability, thesis, Amsterdam 1991

[Pit81] A.M. Pitts, The Theory of Triposes, thesis, Cambridge 1981

[Str93] T. Streicher, Investigations into Intensional Type Theory, Habilitationsschrift, München 1993

[Tro73] A.S. Troelstra, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, LNM 344, Springer 1073

Recent Publications in the BRICS Report Series

RS-96-3 Jaap van Oosten. The Modi�ed Realizability Topos. February 1996. 17 pp.

RS-96-2 Allan Cheng and Mogens Nielsen. Open Maps, Behavioural Equivalences, and Congruences. January 1996. A short version of this paper is to appear in the proceedings of CAAP ’96.

RS-96-1 Gerth St�lting Brodal and Thore Husfeldt. A Communication Complexity Proof that Symmetric Functions have Logarithmic Depth. January 1996. 3 pp.

RS-95-60 J�rgen H. Andersen, Carsten H. Kristensen, and Arne Skou. Speci�cation and Automated Veri�cation of Real-Time Behaviour � A Case Study. December 1995. 24 pp. Appears in 3rd IFAC/IFIP workshop on Algoritms and Architectures for Real-Time Control, AARTC ’95 Proceedings, 1995, pages 613�628.

RS-95-59 Luca Aceto and Anna Ing� olfsd� ottir. On the Finitary Bisimulation. November 1995. 29 pp.

RS-95-58 Nils Klarlund, Madhavan Mukund, and Milind Sohoni. Determinizing Asynchronous Automata on In�nite Inputs. November 1995. 32 pp.

RS-95-57 Jaap van Oosten. Topological Aspects of Traces. November 1995. 16 pp.

RS-95-56 Luca Aceto, Wan J. Fokkink, Rob J. van Glabbeek, and Anna Ing� olfsd� ottir. Axiomatizing Pre�x Iteration with Silent Steps. November 1995. 25 pp.

RS-95-55 Mogens Nielsen and Kim Sunesen. Trace Equivalence - Partially Decidable! November 1995.

RS-95-54 Nils Klarlund, Mogens Nielsen, and Kim Sunesen. Using Monadic Second-Order Logic with Finite Domains for Speci�cation and Veri�cation. November 1995.

RS-95-53 Nils Klarlund, Mogens Nielsen, and Kim Sunesen. Automated Logical Veri�cation based on Trace Abstractions. November 1995. 19 pp.