BRICS LS-98-2 C. Butz: Regular Categories and Regular Logic BRICS

Basic Research in Computer Science

Regular Categories and Regular Logic

Carsten Butz BRICS Lecture Series LS-98-2 ISSN 1395-2048 October 1998 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1998, 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 Lecture 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 LS/98/2/

Regular Categories and Regular Logic

Carsten Butz

Carsten Butz

butz@brics.dk

BRICS^{1}

Department of Computer Science

University of Aarhus

Ny Munkegade DK-8000 Aarhus C, Denmark

October 1998

1Basic Research In Computer Science, Centre of the Danish National Research Foundation.

Preface

Notes handed out to students attending the course on Category Theory at the Department of Computer Science in Aarhus, Spring 1998. These notes were supposed to give more detailed information about the relationship between regular categories and regular logic than is contained in Jaap van Oosten’s script on category theory (BRICS Lectures Series LS-95-1). Regular logic is there called coherent logic. I would like to thank Jaap van Oosten for some comments on these notes. vi

Contents

Preface v 1 Prologue 1 2 Regular Categories 2 3 Regular Logic 11 4 A Sound Calculus 18 5 The Internal Logic of a Regular Category 22 6 The Generic Model of a Regular Theory 25 7 Epilogue 31 viii

Regular Categories and Regular Logic

1 Prologue

In these notes we describe in detail the relation between regular categories and regular logic, the latter being the fragment of first order logic that can express statements of the form ∀x̄(φ(x̄) → ψ(x̄)), where φ and ψ are built up using atomic formulae, the truth constant ⊤, binary meets ∧ and existential quantification ∃. A regular category is a category with all finite limits in which every arrow can be factored as a regular epimorphism followed by a monomorphism. Intuitively, the object arising in this factorisation is the image of the map. A regular functor between such categories is a functor that preserves all this structure. This gives the category RegCat of small regular categories.

In such a regular category we can interpret signatures and extend such interpretations to all regular formulae, i.e., to those formulae built up using atomic formulae, binary meets and existential quantification. Then an interpretation is a model of a sequent ∀x̄(φ(x̄) → ψ(x̄)) if the interpretation of φ(x̄) factors through the interpretation of ψ(x̄) (necessarily as a monomorphism). With the appropriate notion of maps between models this gives for each theory T (i.e., for each set of sequents) and for each regular category C a category \underline{Mod}(T, C) of models of T in C. This construction is natural in C because a regular functor preserves models, so that we have a functor, for each theory T,

\underline{Mod}(T, −): RegCat → Cat,

from small regular categories to small categories.

An important point is that this functor is representable (in a weak sense) by a small regular category R(T), that is, there are equivalences such that for each functor F: C → D the diagram

\xymatrix{\underline{Mod}(T, C) \ar[d]_{\underline{Mod}(T,F)} \ar[r]^{≅} & RegCat(R(T), C) \ar[d]^{F ∘(−)} \\ \underline{Mod}(T, D) \ar[r]_{≅} & RegCat(R(T), D)}

commutes. The representing object is constructed with the help of a small calculus for regular logic, sound for interpretations in regular categories. In particular, applying the above equivalence to the identity functor, this representing category contains a generic model U of T, generic in the sense that a sequent is satisfied by U if and only if it is derivable from T in the calculus. Hence we have a completeness theorem for regular logic with respect to regular categories.^{2}

Our treatment of the material is fairly detailed, but we hope that the reader does not get bored. We included all those minor facts, almost trivial, that one really has to check. For the logician among the readers we should stress that the results of this note are an example of the relationship between logic and category theory. They present the kind of results one can get.

2 Regular Categories

Let C be a category, X an object of C. A subobject of X is an equivalence class of monomorphisms α: A ↪ X where α ∼ β if A and B are isomorphic over X, i.e., there should be an isomorphism i: A →^{≅} B so that

\xymatrix{ & X \\ A \ar@{^{(}->}[ur] \ar[rr]_{≅} &  & B \ar@{^{(}->}[ul]}

commutes. We write A ↣ X to indicate that A is a subobject of X, leaving α often unspecified although it is an important part of the data. Sub(X) denotes the class of subobjects of X, being partially ordered by A ≤ B if and only if α: A ↪ X factors through β: B ↪ X. This partially ordered class has a largest element, represented by the identity map id_{X}.

Definition 2.1 We say that C is well-powered if Sub(X) is a set for all objects X of C.

Suppose now that C has pullbacks. Then for all X the class Sub(X) is a

meet-semilattice, the meet of A ↣^{α} X and B ↣^{β} X being represented by the composition A ×_{X} B ↪ X arising in the pullback square

\xymatrix{A ×_{X} B \ar@{^{(}->}[r] \ar@{^{(}->}[d] & B \ar@{^{(}->}[d]^{β} \\ A \ar@{^{(}->}[r]_{α} & X}

2Of course, regular logic is complete with respect to models in the regular category of sets, thanks to Gödel’s completeness theorem for first-order logic. But similar results as in this note hold for other pairs of logics/categories, where one can not appeal to known results of logic.

2. Regular Categories

Moreover, for each arrow f: X → Y in C, pullback along f induces a meetpreserving map

f^{−1}: Sub(Y) → Sub(X), (B ↣ Y) ↦ (f^{−1}B ↣ X).

(Sometimes one writes f^{∗} instead of f^{−1}.) The object f^{−1}B is called the inverse image of B along f. If C is well-powered the resulting functor Sub(−): C^{op} → Set (or the functor Sub(−): C^{op} → ∧-SLat to the category of meet-semilattices) is called the subobject functor.

Definition 2.2 A category C is called regular^{3} if it has all finite limits, if coequalisers of kernel pairs exist, and if regular epimorphisms are stable under pullbacks.

Here the kernel pair (p_{1}, p_{2}) of an arrow f: X → Y consists of the two projections X ×_{Y} X ⇉ X.

The important point to note about regular categories is that any arrow can be factored as a regular epimorphism followed by a monomorphism. Moreover, this factorisation is unique (up to isomorphism). Before proving this we collect some minor facts about regular epimorphisms in such a category:

Lemma 2.3 Let C be a regular category.

(i) Any regular epimorphism is the coequaliser of its kernel pair. (ii) A regular epimorphism which is mono is an isomorphism. (iii) The composite of two regular epimorphisms is again a regular epimor-

phism. (iv) If f: X → Y and g: Y → Z are arrows such that both g ∘ f and f are

regular epimorphisms, so is g.

Proof. For the first part take some coequaliser \xymatrix{A \ar[r]^{f} \ar[r]_{g} & B \ar@{->>}[r]^{e} & E}, construct

the kernel pair of e to get

\xymatrix{A \ar[r]^{⟨f,g⟩} & B ×_{E} B \ar[r]^{π_{2}} \ar[r]_{π_{1}} & B \ar@{->>}[r]^{e} & E}

3We note that the literature knows many different ‘definitions’ of regular categories.

But they all give the same class of categories provided the request for finite limits is included.

and denote by e′: B ↠ E′ the coequaliser of π_{1} and π_{2}. Since eπ_{1} = eπ_{2} there is a unique map h: E′ → E satisfying he′ = e. Since e′ coequalises π_{1} and π_{2} it satisfies e′f = e′g, so that we find a map h^{−1}: E → E′ such that h^{−1}e = e′. Clearly, h and h^{−1} are inverses of each other.

For the second part note that since e: B ↠ E is the coequaliser of its kernel pair π_{1} and π_{2} and since e is mono that π_{1} = π_{2}: B ×_{E} B ⇉ B. Therefore, the identity map id_{B} coequalises them and e is in fact a split monomorphism and an epimorphism, hence an isomorphism.

Now let B ↠^{e} E ↠^{e′} E′ be two regular epimorphisms. We first look at the pullback diagram

\xymatrix{B ×_{E′} B \ar[r] \ar@{->>}[d] & E ×_{E′} B \ar[r] \ar[d] & B \ar@{->>}[d]^{e} \\ B ×_{E′} E \ar@{->>}[r] \ar[d] \ar[d] & E ×_{E′} E \ar[r] \ar[d] & E \ar@{->>}[d]^{e′} \\ B \ar@{->>}[r]_{e} & E \ar@{->>}[r]_{e′} & E′}

to see that the canonical map e ×_{E′} e: B ×_{E′} B → E ×_{E′} E is epi, as it is the composite of two (regular) epimorphisms. Next we use the diagram

\xymatrix{B ×_{E} B \ar[r]^{q} & B ×_{E′} B \ar@{->>}[r]^{e×_{E′}e} \ar[d]_{q_{1}} \ar[d]^{q_{2}} & E ×_{E′} E \ar[d]_{p_{1}} \ar[d]^{p_{2}} \\  & B \ar@{->>}[r]_{e} & E \ar@{->>}[r]_{e′} & E′}

to show that e′e is the coequaliser of the two parallel arrows (projections) q_{1} and q_{2}. Note that p_{1} ∘ (e ×_{E′} e) = eq_{1} and p_{2} ∘ (e ×_{E′} e) = eq_{2}. Moreover, (p_{1}, p_{2}) is the kernel pair of e′ and (q_{1}q, q_{2}q) is the kernel pair of e.

If g: B → G is such that gq_{1} = gq_{2} then g coequalises the kernel pair of e, so we find a unique g′: E → G satisfying g′e = g. Using that e ×_{E′} e is epi and commutativity of the diagram above we see that g′p_{1} = g′p_{2}, so that there is a unique arrow g′′: E′ → G that satisfies g′ = g′′e′. Thus, e′e is the coequaliser of q_{1} and q_{2}.

Finally, let f: X → Y and g: Y → Z be two arrows such that both gf and f are regular epimorphisms. Write q_{1}, q_{2}: X ×_{Z} X ⇉ X for the kernel pair of gf and p_{1}, p_{2}: Y ×_{Z} Y ⇉ Y for the kernel pair of g. (Note that, as above, q_{1} = p_{1} ∘ (f ×_{Z} f) and similar for the second projections.) If h: Y → H is a map such that hp_{1} = hp_{2} then hf coequalises q_{1} and q_{2}, so that we find a unique h̄: Z → H satisfying h̄gf = hf. Since f is epi, h̄g = h. □

Proposition 2.4 In a regular category C each arrow can be factored as a regular epimorphism followed by a monomorphism. Moreover, for each commutative diagram

\xymatrix{X′ \ar[r]^{f} \ar[d]_{e} & Y \ar[d]^{m} \\ X′ \ar[r]_{g} & Y′}

with e a regular epimorphism and m a monomorphism there exists a (unique) diagonal d: X′ → Y making both triangles commute. In particular, the regular epi–mono factorisation is unique up to isomorphism.

Proof. For the factorisation let f: X → Y be arbitrary and e: X ↠ E the coequaliser of the kernel pair p_{1}, p_{2}: X ×_{Y} X ⇉ X of f. In particular, there exists a unique arrow m: E → Y such that f = m ∘ e. We have to show that m is mono.

Let q_{1}, q_{2}: E ×_{Y} E ⇉ E be the kernel pair of m. Since m(ep_{1}) = m(ep_{2}) there exists a unique arrow b: X ×_{Y} X → E ×_{Y} E such that q_{1}b = ep_{1} and q_{2}b = ep_{2} as in

\xymatrix{X ×_{Y} X \ar[rr]^{p_{1}} \ar[rr]_{p_{2}} \ar[dr]_{b} &  & X \ar[rr]^{f} \ar@{->>}[dr]^{e} &  & Y \\  & E ×_{Y} E \ar[rr]^{q_{1}} \ar[rr]_{q_{2}} &  & E \ar[ur]^{m}}

As in the proof of Lemma 2.3 we observe that b is an epimorphism. But then q_{1} = q_{2} because q_{1}b = ep_{1} = ep_{2} = q_{2}b, which implies that m is a monomorphism: Indeed, for two parallel arrows g, h: Z → E with mh = mg the arrow ⟨g, h⟩: Z → E ×_{Y} E exists, and g = q_{1}⟨g, h⟩ = q_{2}⟨g, h⟩ = h.

To show the second part consider the kernel pair (p_{1}, p_{2}) of e. Since mfp_{1} = f′ep_{1} = f′ep_{2} = mfp_{2} and m is mono we deduce fp_{1} = fp_{2}, and there exists a unique map d: X′ → Y such that f = de. Then f′e = mf = mde and f′ = md because e is epi. □

Let f: X → Y be an arrow in a regular category. The monomorphism m: E ↪ Y arising in the factorisation of f is called the (direct) image of f, denoted Im(f). Sometimes we also say that E is the image of X under f. The image is only unique up to isomorphism, but determines a unique subobject of Y which is denoted ∃_{f}(X). We often confuse Im(f), ∃_{f}(X) and the object E.

More generally, for a subobject A ↣^{α} X of X we define

∃_{f}(A) := Im(f ∘ α),

which gives a well-defined map ∃_{f}: Sub(X) → Sub(Y).

Lemma 2.5 Let f: X → Y be an arrow.

(i) The map ∃_{f} is monotone and left-adjoint to the pullback functor f^{−1}, that is, ∃_{f}: Sub(X) ⇄ Sub(Y): f^{−1}, ∃_{f} ⊣ f^{−1}.

(ii) If g: Y → Z is another arrow then ∃_{g} ∘ ∃_{f} = ∃_{g∘f}: Sub(X) → Sub(Z).

Proof. For monotonicity of ∃_{f} take B′ ≤ B in Sub(X). We factorise first B → Y and then B′ → ∃_{f}B (!) to get the diagram

\xymatrix{X \ar[r]^{f} & Y \\ B \ar@{^{(}->}[u]_{β} \ar@{->>}[r] & ∃_{f}B \ar@{^{(}->}[u] \\ B′ \ar@{->>}[r] \ar@{^{(}->}[u] \ar@{^{(}->}[uu]^{β′} & Z . \ar@{^{(}->}[u]}

The factorisation B′ ↠ Z ↪ Y is a regular epi–mono factorisation of f ∘ β′, so Z represents ∃_{f}B′ and ∃_{f}B′ ≤ ∃_{f}B.

For adjointness we take subobjects A ↣^{α} X and B ↣^{β} Y and look at the solid arrows in

[figure: X; f; Y; f^{−1}B; B; β; A; α; ∃_{f}A]

If ∃_{f}A ≤ B then the dashed map ∃_{f}A → B exists and the outer square commutes, hence the dashed arrow A → f^{−1}B exists (being a monomorphism since α is), and A ≤ f^{−1}B. Conversely, if A ≤ f^{−1}B we can just factorise the map A → B to get the image of A under f, in particular, this image then factors through B.

Finally, the identity ∃_{g} ∘ ∃_{f} = ∃_{g∘f} holds since it just states how leftadjoints compose. □

As a consequence we observe that f^{−1} preserves all meets which exist in Sub(Y). Next we prove the so-called Frobenius identity:

Lemma 2.6 Let C be a regular category, f: X → Y an arrow and A ↣^{α} X,

B ↣^{β} Y two subobjects. Then ∃_{f}(A ∧ f^{−1}B) = ∃_{f}A ∧ B, as subobjects of Y.

Proof. Note first that A ∧ f^{−1}B is obtained as the pullback of B ↪ Y along f ∘ α, which factors as A ↠ ∃_{f}A ↪ Y as in the top part of

\xymatrix{ & X \ar@{->>}[rr] &  & ∃_{f}X \ar@{^{(}->}[r] & Y \\ A \ar@{^{(}->}[ur]^{α} \ar@{->>}[rr] &  & ∃_{f}A \ar@{^{(}->}[ur] \\ A ∧ f^{−1}B \ar@{^{(}->}[u] \ar[rr] &  & ∃_{f}A ∧ B \ar@{^{(}->}[u] \ar@{^{(}->}[rr] &  & B . \ar@{^{(}->}[uu]_{β}}

Thus, pulling back B we first get ∃_{f}A ∧ B (as a subobject of ∃_{f}A and Y), and then A∧f^{−1}B. The map A∧f^{−1}B → ∃_{f}A∧B is a regular epimorphism, since it is the pullback of one, so A ∧ f^{−1}B ↠ ∃_{f}A ∧ B ↪ Y is the regular epi–mono factorisation of A ∧ f^{−1}B ↪ X →^{f} Y and we get the equality of the lemma. □

Next we show how we can code an arrow f: X → Y by its graph, a subobject of X × Y. We define

graph(f) ↣ X × Y

as the image of the map ⟨id_{X}, f⟩: X → X×Y (observe that the canonical map X → graph(f) is an isomorphism). Let π_{X} and π_{Y} denote the projections from X × Y to X and Y respectively.

Lemma 2.7 Let A ↣^{α} X be a subobject of X. Then ∃_{f}A = ∃_{π_{Y}} (π_{X}^{−1}A ∧ graph(f)).

Logically, the lemma says that, for A a predicate of X and f: X → Y, the interpretation of ∃_{f}A is {y | ∃x(f(x) = y ∧ A(x))}.

Proof. Again this is a matter of looking at the right diagram, where all squares are pullback squares, constructed from right to left (we end up with the monomorphism A ↪ X since the composite horizontal map X → X is the identity):

\xymatrix{ &  & Y \\ X \ar[urr]^{f} \ar@{->>}[r] & graph(f) \ar@{^{(}->}[r] & X × Y \ar[r]^{π_{X}} \ar[u]_{π_{Y}} & X \\ A \ar@{^{(}->}[u]^{α} \ar@{->>}[r] & π_{X}^{−1}A ∧ graph(f) \ar@{^{(}->}[u] \ar@{^{(}->}[r] & π_{X}^{−1}A \ar@{^{(}->}[u] \ar[r] & A . \ar@{^{(}->}[u]_{α}}

The map A → π_{X}^{−1}A ∧ graph(f) is a regular epimorphism, so we get the image factorisation of f ∘ α as the image factorisation of the map π_{X}^{−1}A ∧ graph(f) → X × Y → Y composed with A ↠ π_{X}^{−1}A ∧ graph(f) (here we use Lemma 2.3(iii)). In particular, the identity of the lemma holds. □

We note that we can recover f from its graph: A subobject R ↣^{r} X × Y may be seen as a relation between ‘elements’ of X and Y. Call R total if ∃_{π_{Y}} R = X (which means intuitively that the set of all x such that there exists some y with xRy equals X); and functional if the canonical arrow R ×_{X} R → X × Y × Y factors through the inclusion id_{X} × Δ_{Y}: X × Y → X × Y × Y. (Since R ×_{X} R represents the ‘object’ of triples (x, y_{1}, y_{2}) such that xRy_{1} and xRy_{2} this means intuitively that from xRy_{1} and xRy_{2} one should be able to deduce y_{1} = y_{2}.)

The graph of an arrow f in C is a total and functional relation on X × Y (Exercise E.3).

Lemma 2.8 For each total and functional relation R ↣^{r} X × Y there exists a unique arrow f: X → Y in C such that R = graph(f).

Proof. Since R is total the composite R ↪^{r} X × Y →^{π_{X}} X is a regular epimorphism which is the coequaliser of its kernel pair (p_{1}, p_{2}) constructed in

\xymatrix{R ×_{X} R \ar[rr] \ar@{^{(}->}[dd] \ar[rrr]^{p_{2}} \ar[ddd]_{p_{1}} \ar@{-->}[dr] &  & Y ×_{X} R \ar[r] \ar[dd] & R \ar@{^{(}->}[dd]^{r} \\  & P = X × Y \ar@{-->}[dr]^{id_{X}×Δ_{Y}} \\ R ×_{X} Y \ar@{^{(}->}[rr] \ar[d] &  & X × Y × Y \ar[r]^{π_{1,3}} \ar[d]_{π_{1,2}} & X × Y \ar[d]^{π_{X}} \ar[ddr]^{π_{Y}} \\ R \ar@{^{(}->}[rr]_{r} &  & X × Y \ar[r]_{π_{X}} \ar[drr]_{π_{Y}} & X \\  &  &  &  & Y .}

(The dashed factorisation exists since R is functional.) The two ways from P to Y are just the projection onto the second coordinate, hence we deduce that π_{Y} ∘ r coequalises p_{1} and p_{2} so that there exists a unique f: X → Y satisfying fπ_{X}r = π_{Y} r.

To show that R = graph(f) we look at the following diagram where the right part is just the definition of graph(f):

[figure: Y; R; r; X × Y; π_{X}; X; ⟨id_{X},f⟩; f; graph(f); X × Y; π_{Y}; π_{X}; X]

The composite R ↪ X ×Y → X is a regular epimorphism and we can obtain graph(f) as well as the regular epi–mono factorisation of the composite R → X × Y. But this map is the unique such map when composed with π_{X} gives id_{X}π_{X}r and when composed with π_{Y} gives π_{Y} ∘⟨id_{X}, f⟩∘π_{X}∘r = fπ_{X}r = π_{Y} r! So this map has to be the mono r: R ↪ X × Y, the image of which is R. □

Another important fact one has to know is the behaviour of images of maps that are related by a pullback square:

Lemma 2.9 Let

\xymatrix{Z ×_{Y} X \ar[r]^{g′} \ar[d]_{f′} & X \ar[d]^{f} \\ Z \ar[r]_{g} & Y}

be a pullback square. Then ∃_{g′}f^{′−1} = f^{−1}∃_{g}: Sub(Z) → Sub(X).

Proof. For a subobject A ↣^{α} Z we look at the following cube, where the front is our pullback square, the left side is a pullback square obtained from pulling back A along f′, the bottom fact is the image factorisations of A → Y, while the right side and the back side are again two pullback squares:

[figure: A ×_{Y} X; f^{−1}∃_{g}A; Z ×_{Y} X; f′; X; f; A; ∃_{g}A; Z; g; Y]

Since A ×_{Y} X = f^{′−1}(A) the factorisation A ×_{Y} X ↠ f^{−1}∃_{g}A ↪ X is the regular epi–mono factorisation of f^{′−1}(A) ↪ Z ×_{Y} X → X, so we get the equality as stated in the lemma. □

Call a functor F: C → D between regular categories regular if it preserves finite limits and coequalisers of kernel pairs (the latter makes sense since F preserves finite limits). We denote by RegCat the category with objects the small regular categories and arrows regular functors. Since in a category with pullbacks an arrow f is mono if and only if

\xymatrix{• \ar[r]^{id} \ar[d]_{id} & • \ar[d]^{f} \\ • \ar[r]_{f} & •}

3. Regular Logic

is a pullback square, any regular functor F: C → D induces, for each object X of C, a map F_{X} (or just F)

F: Sub_{C}(X) → Sub_{D}(F (X))

which preserves finite meets and the top element. In particular, it is monotone. Moreover, if f: X → Y and if B ↣ Y then F (f^{−1}B) = F (f)^{−1}(F (B)) because F preserves pullbacks. One way to sum this up is to say that F induces a natural transformation

Sub_{C}(−) ⇒ Sub_{D}(F (−)): C^{op} ⇉ Set.

In addition, F preserves by definition as well images: If A ↪^{α} X →^{f} Y is given then F (∃_{f}A) = ∃_{F (f)}(F (A)). For this just remember that ∃_{f}A was defined as the coequaliser of the kernel pair of f ∘ α: A → Y. For the record:

Lemma 2.10 A regular functor between regular categories preserves both inverse images and (direct) images. □

3 Regular Logic

Regular logic is roughly speaking the ∃–∧–fragment of many-sorted firstorder logic. Although we do not prove this here we mention that there is no difference between the intuitionistic and the classical version.

A (typed) signature S consists of a set of basic sorts (basic types) \underline{sort}_{S} = \{X_{1}, X_{2}, …\}, and of sets \underline{const}_{S}, \underline{funct}_{S} and \underline{rel}_{S} of typed constants, function and relation symbols. We write expressions like

c: X,  f: X_{1} × ⋯ × X_{n} → Y,  R ↣ X_{1} × ⋯ × X_{m},

to indicate the typing of these symbols. (Note that X_{1} × ⋯ × X_{n} is just a formal expression that should support our intuition!) We usually abbreviate X_{1} × ⋯ × X_{n} as X̄.

Given a signature S, the language L(S) (or better L_{ωω}^{r}(S), where the superscript r stands for regular)^{4} consists of the signature S, for each sort X a countable list of variables x (we write x: X to indicate that x is a variable of type X, as well, x̄: X̄ has its obvious meaning), and the sets of (typed) terms and formulae defined as follows:

4There are some conventions on how to denote logics. Here the first subscript ω stands for the fact that there are only finite conjunctions, i.e., conjunctions over sets of cardinality less then ω. The second ω stands for the fact that there are only finite blocks of quantifiers (in our case, of existential quantifiers).

(T1) x is a term of type X, provided that x is a variable of type X. (T2) Similarly, a constant c is a term of type X if c: X. (T3) If t_{1}, …, t_{n} are terms of type X_{1}, …, X_{n} respectively and if f: X_{1}×⋯×

X_{n} → Y is a function symbol then f(t_{1}, …, t_{n}) is a term of type Y. (F1) If t_{1} and t_{2} are terms of type X then t_{1} = t_{2} (or better: t_{1} =_{X} t_{2}) is a

formula. (F2) If t_{1}, …, t_{m} are terms of type X_{1}, …, X_{m} respectively, and if R ↣

X_{1} × ⋯ × X_{m} is a relation symbol, then R(t_{1}, …, t_{m}) is a formula. (F3) ⊤ (the logical constant ‘true’) is a formula. (F4) If φ and ψ are formulae so are φ ∧ ψ and ∃xφ (x a variable of some

type).

For a formula φ, FV(φ) denotes the the set of free variables of φ. A theory T (formulated in L(S)) is a set of sequents

φ ⇒ ψ

where φ and ψ are (regular) formulae. The latter is shorthanded to ψ if φ ≡ ⊤.

Below we will define interpretations M of a language L(S) in a regular category. Then M will be a model of φ ⇒ ψ if {x̄ | φ}^{(M)} ≤ {x̄ | ψ}^{(M)}, as subobjects of X_{1}^{(M)} × ⋯ × X_{n}^{(M)} (and x̄ the set of variables occurring free in either φ or ψ). In Set this is equivalent to say that M is a model of ∀x̄(φ → ψ), and indeed, this is the intuition one should have about a sequent φ ⇒ ψ.

Remark 3.1 In what follows we will always assume that a regular category comes equipped with a choice of a terminal object, of binary products and of equalisers. Using bracketing from left to right, a sequence C_{1} × ⋯ C_{n} then means (⋯ ((C_{1} × C_{2}) × C_{2}) × ⋯) × C_{n}. Of course, to make such choices we have to use the Axiom of Choice.

To be precise, an interpretation M of L(S) in a regular category C consists of

— an object X^{(M)} of C for each basic sort X ∈ \underline{sort}_{S}; — an arrow c^{(M)}: 1_{C} → X^{(M)} for each constant c: X;

— an arrow f^{(M)}: X_{1}^{(M)} × ⋯ × X_{n}^{(M)} → Y^{(M)} for each function symbol f: X_{1} × ⋯ × X_{n} → Y in \underline{funct}_{S};

— and a subobject R^{(M)} ↣ X_{1}^{(M)} × ⋯ × X_{n}^{(M)} for each relation symbol R ↣ X_{1} × ⋯ × X_{n}.

We write X̄^{(M)} for the product X_{1}^{(M)} ×⋯×X_{n}^{(M)}. This interpretation of the signature is extended to all terms and all formulae. To a term t of type Y with free variables among z̄: Z̄ we assign an arrow t(z̄)^{(M)}: Z̄^{(M)} → Y^{(M)}, to a formula φ with free variables among z̄: Z̄ we assign a subobject {z̄ | φ}^{(M)} of Z̄^{(M)} as follows:

(T1) If x is a variable of type X then x(z̄)^{(M)} is the composite Z̄^{(M)} →^{π} X^{(M)} →^{id} X^{(M)}. (Here we are very specific: x: X is interpreted by the identity X^{(M)} → X^{(M)}, the projection π is needed to handle the ‘dummy’ variables occurring in z̄. Note that, by assumption, the free variables of the term x (i.e., the variable x) are contained in the list z̄.)

(T2) If c: X is a constant then c(z̄)^{(M)} is the composite Z̄^{(M)} → 1 →^{c^{(M)}} X^{(M)}. (T3) Let f: X_{1} × ⋯ × X_{n} → Y be a function symbol, t_{i} terms of type X_{i}. By

induction, the terms t_{i} are interpreted by arrows t_{i}(z̄)^{(M)}: Z̄^{(M)} → X_{i}^{(M)}, and f(t_{1}, …, t_{n}) = f(t̄(z̄)) is interpreted by the composite

\xymatrix{f^{(M)}(t_{1}^{(M)}, …, t_{n}^{(M)}): Z̄^{(M)} \ar[r]^{⟨t_{1}^{(M)},...,t_{n}^{(M)}⟩} & X̄^{(M)} \ar[r]^{f^{(M)}} & Y^{(M)}}.

(F1) \{z̄ | t_{1} = t_{2}\}^{(M)} is the equaliser of \xymatrix{Z̄^{(M)} \ar[r]^{t_{1}(z̄)^{(M)}} \ar[r]_{t_{2}(z̄)^{(M)}} & X^{(M)}}.

(F2) {z̄ | R(t_{1}, …, t_{n})}^{(M)} is the subobject of Z̄^{(M)} defined by the pullback

in

\xymatrix{pb \ar@{^{(}->}[r] \ar[d] & Z̄^{(M)} \ar[d]^{⟨t_{1}^{(M)},...,t_{n}^{(M)}⟩} \\ R^{(M)} \ar@{^{(}->}[r] & X̄^{(M)}.}

(F3) {z̄ | ⊤}^{(M)} is Z̄^{(M)}. (F4) {z̄ | φ ∧ ψ}^{(M)} = {z̄ | φ}^{(M)} ∧ {z̄ | ψ}^{(M)}; and finally, {z̄ | ∃yφ}^{(M)} =

∃_{π}{(y, z̄) | φ}^{(M)}, where π is the projection Y^{(M)} × Z̄^{(M)} → Z̄^{(M)}.

An interpretation M is called a model of a sequent φ ⇒ ψ (notation: M ⊧ φ ⇒ ψ) if {x̄ | φ}^{(M)} ≤ {x̄ | ψ}^{(M)} as subobjects of X̄^{(M)}, where x̄: X̄ is the tuple (or set) of those variables occurring free either in φ or in ψ. The interpretation M is a model of a theory T (M ⊧ T) if it is a model of each sequent in T.

Example 3.2 Let S be the signature with sorts X, Y, Z and three function symbols f: X → Y, g: Y → Z and h: X → Z. An interpretation M of L(S) in a regular category C is a model of h(x) = g(f(x)) if and only if h^{(M)} = g^{(M)} ∘ f^{(M)}: X^{(M)} → Z^{(M)}. Indeed, {x | h(x) = g(f(x))}^{(M)} is the subobject

determined by the equaliser E of the two arrows \xymatrix{X^{(M)} \ar[r]^{h^{(M)}} \ar[r]_{g^{(M)}∘f^{(M)}} & Z^{(M)}}; and

M ⊧ h(x) = g(f(x)) iff E ≅ X^{(M)} iff h^{(M)} = g^{(M)} ∘ f^{(M)}.

In the next section we will give a sound (and complete) calculus for regular logic. Here we have to prove two technical lemmas which give information about dummy variables and about substitution.

Lemma 3.3 Let φ be a formula with free variables among the tuple z̄. Write moreover π: Y^{(M)} × Z̄^{(M)} → Z̄^{(M)} for the projection to Z̄^{(M)}. Then {(y, z̄) | φ}^{(M)} = π^{−1}{z̄ | φ}^{(M)}.

Proof. We first note that for terms t of type X one proves by induction that t(y, z̄)^{(M)} = t(z̄)^{(M)} ∘ π: Y^{(M)} × Z̄^{(M)} → X^{(M)}.

Then we proceed again by induction, this time on φ. The case φ ≡ ⊤ is trivial, while φ ≡ R(t̄) follows since we have the diagram

\xymatrix{\{(y, z̄) | R(t̄)\}^{(M)} \ar@{^{(}->}[r] \ar[d] & Y^{(M)} × Z̄^{(M)} \ar[d]^{π} \ar[r] & Y^{(M)} \ar[d] \\ \{z̄ | R(t̄)\}^{(M)} \ar@{^{(}->}[r] \ar[d] & Z̄^{(M)} \ar[d]^{⟨t̄^{(M)}⟩} \ar[r] & 1 \\ R \ar@{^{(}->}[r] & X̄}

where all squares are pullbacks. The case φ ∧ ψ holds (by induction) because π^{−1} preserves binary meets. For φ ≡ ∃xψ we calculate

{(y, z̄) | ∃xψ}^{(M)} = ∃_{p}{(y, x, z̄) | ψ}^{(M)}  (by definition)
= ∃_{p}(π_{X×Z̄})^{−1}{(x, z̄) | ψ}^{(M)} (by induction)
= (πZ̄)^{−1}∃_{q}{(x, z̄) | ψ}^{(M)}  (by Lemma 2.9)
= (πZ̄)^{−1}{z̄ | ∃xψ}^{(M)}

where we used the pullback square

\xymatrix{Y^{(M)} × X^{(M)} × Z̄^{(M)} \ar[r]^{p} \ar[d]_{π_{X×Z̄}} & Y^{(M)} × Z̄^{(M)} \ar[d]^{πZ̄} \\ X^{(M)} × Z̄^{(M)} \ar[r]_{q} & Z̄^{(M)}}

The case φ ≡ t_{1} = t_{2} holds since taking the equaliser of two arrows commutes with taking products. □

As a consequence of the proof we can always write t^{(M)} instead of t(z̄)^{(M)}, since these arrows are uniquely determined provided we know what they are in the case z̄ = FV(t).

Lemma 3.4 Let ψ be a formula with free variables among z̄, y and let b be a term of type Y (with free variables among z̄) which is substitutable for y in ψ, i.e., after substitution no free variable of b becomes bound in ψ(b). Then {z̄ | ψ(b)}^{(M)} = ⟨b^{(M)}, idZ̄^{(M)}⟩^{−1}{(y, z̄) | ψ}^{(M)}; that is, there is a pullback square

\xymatrix{\{z̄ | ψ(b)\}^{(M)} \ar[d] \ar@{^{(}->}[r] & Z̄^{(M)} \ar[d]^{⟨b^{(M)},idZ̄^{(M)}⟩} \\ \{(y, z̄) | ψ\}^{(M)} \ar@{^{(}->}[r] & Y^{(M)} × Z̄^{(M)}}

Proof. We prove this by induction on ψ, but first we note that for a term t of type X with free variables among (y, z̄),

t(b/y, z̄)^{(M)} = t^{(M)} ∘ ⟨b^{(M)}, idZ̄^{(M)}⟩: Z̄^{(M)} → Y^{(M)} × Z̄^{(M)} → X^{(M)}.

(The proof is by induction as well.) Then the case ψ ≡ t_{1} = t_{2} follows from Exercise E.1, while the cases ψ ≡ R(t̄), ψ ≡ ⊤, and ψ ≡ ψ_{1} ∧ ψ_{2} are either trivial or easy.

Finally, suppose ψ = ∃xφ(x). By assumption (b is substitutable in ψ) we have x ∉ FV(b). The proof of this case is contained in the following cube, where we assumed for simplicity that z̄ is the empty sequence. Here the front square is just the pullback square, as is the left side. Then the map {(x, y) | φ(x, y)}^{(M)} → Y^{(M)} is factored as a regular epimorphism followed by a monomorphism, with the image by definition {y | ∃xφ}^{(M)}. This yields the bottom of the cube. Finally, the right side and the back side are obtained as pullbacks of the regular epi–mono factorisation along the map b^{(M)}:

[figure: {x | φ(x, b)}^{(M)}; (b^{(M)})^{−1}{y | ∃xφ}^{(M)}; X^{(M)}; ⟨id,b^{(M)}⟩; 1; b^{(M)}; {(x, y) | φ}^{(M)}; {y | ∃xφ}^{(M)}; X^{(M)} × Y^{(M)}; π; Y^{(M)}]

We deduce that the factorisation

{x | φ(x, b)}^{(M)} ↠ (b^{(M)})^{−1}{y | ∃xφ(x, y)}^{(M)} ↪ 1

is the regular epi–mono factorisation of {x | φ(x, b)}^{(M)} → 1, so that we get the equality {· | ∃xφ(x, b)}^{(M)} = (b^{(M)})^{−1}{y | ∃xφ(x, y)}^{(M)}. □

We want to make the class of models of a theory T in a regular category C into another category \underline{Mod}(T, C). A morphism h between two models M and N of T is a family of maps \{h_{X}: X^{(M)} → X^{(N)}\}_{X∈\underline{sort}_{S}} which commute with the interpretations of the basic operations in our language, i.e., for c: X a constant, f: X̄ → Y a function symbol the diagrams

\xymatrix{1 \ar[r]^{c^{(M)}} \ar[dr]_{c^{(N)}} & X^{(M)} \ar[d]^{h_{X}} & X̄^{(M)} \ar[r]^{f^{(M)}} \ar[d]_{h_{X_{1}}×···×h_{Xn}} & Y^{(M)} \ar[d]^{h_{Y}} \\  & X^{(N)} & X̄^{(N)} \ar[r]_{f^{(N)}} & Y^{(N)}}

commute; while for a relation symbol R ↣ X̄ the composite (h_{X_{1}}×⋯×h_{X_{n}})∘ i^{(M)}: R^{(M)} → X̄^{(M)} → X̄^{(N)} should factor through the inclusion R^{(N)} ↪ X̄^{(N)}.

By induction one proves that for all terms t(z̄) of type Y,

\xymatrix{Z̄^{(M)} \ar[r]^{t^{(M)}} \ar[d]_{hZ̄} & Y^{(M)} \ar[d]^{h_{Y}} \\ Z̄^{(N)} \ar[r]_{t^{(N)}} & Y^{(N)}}

commutes (hZ̄ being the product h_{Z_{1}} × ⋯ × h_{Z_{n}}); and for each formula φ(z̄) the composite {z̄ | φ}^{(M)} ↪ Z̄^{(M)} → Z̄^{(N)} factors through {z̄ | φ}^{(N)}.

Let F: C → D be a regular functor between regular categories. If M is a model of a theory T (formulated in L(S)) we get an interpretation F (M) of L(S) in D as follows: We define^{5}

— for a sort X in \underline{sort}_{S}, X^{(F (M))} = F (X^{(M)});

— for a constant c: X, c^{(F (M))} = F (c^{(M)}): 1_{D} → X^{(F (M))};

— for an arrow f: X̄ → Y in \underline{sort}_{S}, f^{(F (M))} = F (f^{(M)});

— and for R ↣ X̄ a relation symbol, R^{(F (M))} = F (R^{(M)}) ↣ X̄^{(F (M))}.

A straightforward induction shows that for all terms t of type Y with free variables among z̄: Z̄,

t^{(F (M))} = F (t^{(M)}): Z̄^{(F (M))} → X^{(F (M))},

and finally, again by induction, one proves that for all regular formulae φ in the underlying language

{x̄ | φ}^{(F (M))} = F ({x̄ | φ}^{(M)}).

5Strictly speaking, F does not preserve the chosen terminal objects, the binary products and the equalisers. But, for example, there is a canonical isomorphism F (1) ≅ 1. We suppressed mentioning explicitly these isomorphisms, but for being precise they should be present. The point is that they do no harm because they are unique.

It follows that F (M) is a model of T, since for a sequent φ ⇒ ψ in T we have {x̄ | φ}^{(M)} ≤ {x̄ | ψ}^{(M)} and F preserves the order of subobjects.

Moreover, if h: M → N is a map in \underline{Mod}(T, C) we can apply F pointwise to get a map F (h) = \{F (h_{X}): X^{(F (M))} → X^{(F (N))}\}_{X∈\underline{sort}_{S}} between the models F (M) and F (N). For the record:

Lemma 3.5 A regular functor F: C → D between regular categories induces, for each regular theory T, a functor \underline{Mod}(T, −): F_{T}: \underline{Mod}(T, C) → \underline{Mod}(T, D). In particular we have a functor RegCat → Cat, from small regular categories to small categories. □

On the other side, if M is a fixed model of T in a regular category E we get for each regular category D a functor

𝔐_{M,D} = (−)_{T} (M): RegCat(E, D) → \underline{Mod}(T, D),

which on objects sends a functor G: E → D to the model G(M) in D. A natural transformation α: G ⇒ H is sent to the map between models

\{α_{X^{(M)}}: G(X^{(M)}) → H(X^{(M)})\}_{X∈\underline{sort}_{S}}.

Moreover, if F: D → C is a regular functor the diagram of functors

\xymatrix{RegCat(E, D) \ar[r]^{𝔐_{M,D}} \ar[d]_{F ∘(−)} & \underline{Mod}(T, D) \ar[d]^{F_{T}} \\ RegCat(E, C) \ar[r]_{𝔐_{M,C}} & \underline{Mod}(T, C)}

commutes.

4 A Sound Calculus

Here we fix a language L(S) and define a sequence of entailment relations (or deduction relations) ⊢_{F} between formulae, the relations being indexed by finite sets F of (typed) variables. The sequent φ ⊢_{F} ψ (or φ ⊢x̄ ψ) is only defined if both the free variables of φ and ψ are contained in the set F. Writing down expressions like that it is always assumed that this side condition is fulfilled.

4. A Sound Calculus

The reason for the subscripts is as follows: Even in the simplest case where p is a closed regular formula there is an essential difference between the two interpretations {· | p}^{(M)} ↣ 1 and {x̄ | p}^{(M)} ↣ X̄^{(M)} (M some interpretation in a regular category). From the first we can always get the second by pullback along !_{X^{(M)}}: X^{(M)} → 1, but the second does not determine the first. This is only the case if !_{X^{(M)}} is a regular epimorphism, in which case {· | p}^{(M)} = ∃_{!_{X^{(M)}}}{x̄ | p}^{(M)}. Thus, if we would have restricted ourselves to interpretations in which each sort X is interpreted by an object X^{(M)} with ‘global support’ (i.e., objects such that !_{X^{(M)}} is a regular epimorphism), then we could get rid of these subscripts. We remark as well that X^{(M)} has global support if and only if M ⊧ ∃x.x = x, i.e., if it is true in M that X^{(M)} is ‘inhabited’^{6}.

We group the axioms and rules of inference for our entailment relations as follows:

1. Structural rules

1.1 p ⊢_{F} p;

1.2 \frac{p ⊢_{F} q q ⊢_{F} r}{p ⊢_{F} r} ;

1.3 \frac{p ⊢_{F} q}{p ⊢_{F ∪\{y\}} q} ;

1.4 \frac{φ(y) ⊢_{F} ψ(y)}{φ(b) ⊢_{F \\{y\}} ψ(b)} ,

where y: B is a variable, b is a term of type B, and b is substitutable for y on both sides, that is, no free variable of b becomes bound in φ(b) and ψ(b) after substitution. As well, implicitly it is assumed that FV(b) ⊂ F \ {y}.

2. Logical rules

2.1 p ⊢_{F} ⊤;

2.2 if r ⊢_{F} p ∧ q then r ⊢_{F} p and r ⊢_{F} q; and if both r ⊢_{F} p and r ⊢_{F} q then r ⊢_{F} p ∧ q; 2.3 if ∃yψ(y) ⊢_{F} p then ψ(y) ⊢_{F ∪{y}} p; and conversely if ψ(y) ⊢_{F ∪{y}} p then

6In intuitionistic logic being inhabited is a positive way to express non-emptiness.

∃yψ(y) ⊢_{F} p.

3. Rules for equality

3.1 ⊤ ⊢_{x} x = x;

3.2 x_{1} = x_{2} ⊢_{x_{1},x_{2}} x_{2} = x_{1};

3.3 x_{1} = x_{2} ∧ x_{2} = x_{3} ⊢_{x_{1},x_{2},x_{3}} x_{1} = x_{3};

3.4 x̄^{1} = x̄^{2} ⊢_{x̄^{1},x̄^{2}} f(x̄^{1}) = f(x̄^{2}), for each function symbol f: X̄ → Y in the language. (Here x̄^{1} = x̄^{2} stands of course for ⋀_{i} x_{i}^{1} = x_{i}^{2}.)

3.5 x̄^{1} = x̄^{2} ∧ R(x̄^{1}) ⊢_{x̄^{1},x̄^{2}} R(x̄^{2}), for each relation symbol R ↣ X̄ in the language.

We write ⊢ for ⊢_{∅} and ⊢_{F} ψ for ∅ ⊢_{F} ψ. Given a theory T we write T, φ ⊢_{F} ψ if φ ⊢_{F}^{T} ψ, where ⊢_{F}^{T} denotes entailment in the calculus above extended by the axioms

φ ⊢_{FV(φ)∪FV(ψ)} ψ for φ ⇒ ψ in T .

To give the whole a more symmetric outlook we write as well T ⊢x̄ φ ⇒ ψ for the fact that (modulo T), φ implies ψ. Then T ⊢x̄ φ ⇔ ψ stands for the fact that modulo T the formula φ is provably equivalent to the formula ψ.

Lemma 4.1 (Soundness.) Let T be a theory, and M a model of T in a regular category. If T, φ ⊢x̄ ψ then {x̄ | φ}^{(M)} ≤ {x̄ | φ}^{(M)}, as subobjects of X̄^{(M)}.

Proof. We prove this lemma by induction over a derivation of φ ⊢T ; x̄ ψ. In case of an axiom φ ⇒ ψ of T this is part of the definition of being a model. The case of the axiom 1.1 is trivial, while 2.1 holds since {x̄ | p}^{(M)} ≤ X̄^{(M)} = {x̄ | ⊤}^{(M)}.

For the induction steps rule 1.2 is sound since the order on X̄^{(M)} is transitive, while 1.3 is sound because pullback along the projection π: Y^{(M)} × X̄^{(M)} → X̄^{(M)} induces a monotone map Sub(X̄^{(M)}) → Sub(Y^{(M)} × X̄^{(M)}). (Note that Lemma 3.3 enters here describing {(y, x̄) | p}^{(M)} as π^{−1}{x̄ | p}^{(M)}.)

Rule 2.2 is sound because {x̄ | p∧q}^{(M)} = {x̄ | p}^{(M)} ∧^{Sub(X̄^{(M)})} {x̄ | q}^{(M)}, while 2.3 is sound since {x̄ | ∃yψ(y)}^{(M)} = ∃_{π}{(y, x̄) | ψ(y)}^{(M)} ≤ {x̄ | p}^{(M)} if and only if {(y, x̄) | ψ(y)}^{(M)} ≤ Y^{(M)} × {x̄ | p}^{(M)} = {(y, x̄) | p}^{(M)}, for π the projection Y^{(M)} × X̄^{(M)} → X̄^{(M)} (here we use Lemma 3.3 again).

Soundness of rule 1.4 follows from Lemma 3.4.

It remains to prove soundness of the rules for equality. Rule 3.1 is sound since {x | x = x}^{(M)} is the equaliser of id_{X}, id_{X}: X^{(M)} ⇉ X^{(M)}, which is X^{(M)}; rule 3.2 is sound because the equaliser of π_{1}, π_{2}: X^{(M)}×X^{(M)} ⇉ X^{(M)} factors through (in fact, is equal to) the equaliser of π_{2} and π_{1}.

The interpretation of x_{1} = x_{2} ∧ x_{2} = x_{3} is the pullback

\xymatrix{P \ar@{^{(}->}[r]^{q} \ar@{^{(}->}[d]_{p} & E_{2,3} \ar@{^{(}->}[d]^{i_{2,3}} \\ E_{1,2} \ar@{^{(}->}[r]_{i_{1,2}} & X^{(M)} × X^{(M)} × X^{(M)} \ar[r]^{π_{1}} \ar[r]_{π_{2}} \ar[d]^{π_{3}} \ar[d]_{π_{2}} & X \\  & X}

Since π_{1}i_{1,2}p = π_{2}i_{1,2}p = π_{2}i_{2,3}q = π_{3}i_{2,3}q the canonical map P → X^{(M)} × X^{(M)} × X^{(M)} factors through the equaliser of π_{1} ad π_{2}, the interpretation of {(x_{1}, x_{2}, x_{3}) | x_{1} = x_{3}}^{(M)}.

Rule 3.4 is sound since the diagonal X̄^{(M)} → X̄^{(M)} × X̄^{(M)}, the interpretation of x̄^{1} = x̄^{2}, equalises fπ_{1} and fπ_{2},

\xymatrix{\{(x̄^{1}, x̄^{2}) | f(x̄^{1})) = f(x̄^{2})\}^{(M)} \ar@{^{(}->}[r] & X^{(M)} × X^{(M)} \ar[r]^{fπ_{1}} \ar[r]_{fπ_{2}} \ar[d]^{π_{2}} \ar[d]_{π_{1}} & Y \\ X̄^{(M)} \ar@{-->}[u] \ar@{^{(}->}[ur] \ar[r]_{id} & X̄^{(M)} \ar[ur]_{f}}

Finally, for rule 3.5, the left side x̄^{1} = x̄^{2} ∧ R(x̄^{1}) is the pullback

\xymatrix{P \ar@{^{(}->}[r]^{q} \ar@{^{(}->}[d]_{p} & X̄^{(M)} \ar@{^{(}->}[d]^{Δ} \\ R^{(M)} × X̄^{(M)} \ar[d] \ar@{^{(}->}[r]_{r^{(M)}×id} & X̄^{(M)} × X̄^{(M)} \ar[d]^{π_{1}} \\ R^{(M)} \ar@{^{(}->}[r]_{r^{(M)}} & X̄^{(M)} .}

It follows that P ↪ X̄^{(M)} × X̄^{(M)} factors through R^{(M)} ↪ X̄^{(M)} ↪ X̄^{(M)} × X̄^{(M)}, in particular through X̄^{(M)} × R^{(M)}, the interpretation of R(x̄^{2}). □

Let us mention that classical first-order logic is conservative over regular logic (provided one allows empty domains as well), so that intuitively all clauses of the following lemma are true. We leave the proof as an exercise, but mention the connection between (i) and Lemma 2.6.

Lemma 4.2 (i) ⊢z̄ ∃x̄(p(x̄) ∧ q) ⇔ (∃x̄p(x̄)) ∧ q,

provided x̄ does not occur free in q. (ii) ⊢_{x̄,x̄′} p(x̄) ∧ x̄ = x̄′ ⇒ p(x̄′). □

5 The Internal Logic of a Regular Category

Let C be a regular category. To it we associate a signature and language as follows: S_{C} has as basic sorts the objects of the category C. Again we fix a terminal object and for each finite list of objects of C one specified product of this finite set of objects.

Then our signature has for each arrow c: 1 → X in C one constant symbol c: X, for each arrow f: X̄ → Y one function symbol f: X̄ → Y, and for each subobject R ↣ X̄ one relation symbol R ↣ X̄. Obviously, the language L(S) has a canonical interpretation I^{C} in C. We define T_{C} to be the theory of this interpretation, i.e., the set of all sequents φ ⊢_{F} ψ in the language L(S) which are true under the interpretation I^{C}. Instead of I^{C} one writes usually just C. In what follows, we do not distinguish between a symbol, say a function symbol f, in our language and its interpretation f^{(I^{C})} in the category C.

We will first show how different categorical notions are captured by the internal language of the category.

Lemma 5.1 Let C be a regular category.

(i) Let A →^{f} B →^{g} C be two arrows and h: A → C. Then h = g ∘ f if and only if C ⊧ h(x) = g(f(x)), where x is a free variable of type A.

(ii) An arrow m: X → Y is mono if and only if C ⊧ m(x_{1}) = m(x_{2}) ⇒

x_{1} = x_{2}. (iii) The arrow f: X → Y is a regular epimorphism if and only if C ⊧

∃xf(x) = y. (One should read this as ‘ ∀y∃xf(x) = y’.)

5. The Internal Logic of a Regular Category

Proof. The first part is as in Example 3.2. For the characterisation of monomorphisms we look at

\xymatrix{\{(x_{1}, x_{2}) | x_{1} = x_{2}\}^{(C)} \ar@{^{(}->}[r] & X × X \ar[r]^{π_{1}} \ar[r]_{π_{2}} & X \ar[d]^{m} \\ \{(x_{1}, x_{2}) | m(x_{1}) = m(x_{2})\}^{(C)} \ar@{^{(}->}[ur]_{i} &  & Y,}

that is, the top line is an equaliser diagram and {(x_{1}, x_{2}) | m(x_{1}) = m(x_{2})}^{(C)} is the equaliser of mπ_{1} and mπ_{2}. If m is a monomorphism then the inclusion i equalises π_{1} and π_{2}, so factors through {(x_{1}, x_{2}) | x_{1} = x_{2}}^{(C)}. Conversely, if we have this factorisation then for two parallel arrows f, g: Z ⇉ X such that mf = mg the map ⟨f, g⟩: Z → X × X factors through i, in particular through the interpretation of x_{1} = x_{2}. Hence f = π_{1}⟨f, g⟩ = π_{2}⟨f, g⟩ = g, and m is a monomorphism.

For the last part we note first that graph(f) ↪ X × Y is the equaliser of fπ_{1} and π_{2} (Exercise E.4), the interpretation of f(x) = y. Then we can apply Lemma 2.3 to the diagram

\xymatrix{X \ar@{->>}[r] \ar[drr]_{f} & graph(f) \ar@{^{(}->}[r] \ar[dr] & X × Y \ar[d]^{π_{2}} \\  &  & Y}

to see that f is a regular epimorphism iff graph(f) → Y is, which holds if and only if C ⊧ ∃xf(x) = y. □

The following lemma characterises finite limits in a regular category with the help of the internal logic.

Lemma 5.2 Let C be again a regular category.

(i) An object X is C is terminal iff C ⊧ x_{1} = x_{2} and C ⊧ ∃xx = x. (ii) Two maps f: Z → X and g: Z → Y make Z a product of X and Y

if and only if C ⊧ f(z_{1}) = f(z_{2}) ∧ g(z_{1}) = g(z_{2}) ⇒ z_{1} = z_{2} and C ⊧ ∃z(f(z) = x ∧ g(z) = y).

(iii) In a diagram \xymatrix{Z \ar[r]^{e} & X \ar[r]^{f} \ar[r]_{g} & Y} such that fe = ge, the object E is the

equaliser of f and g if and only if e is a mono and C ⊧ f(x) = g(x) ⇒ ∃ze(z) = x. This can be expressed using the predicate Z associated to the subobject Z ↪ X as C ⊧ f(x) = g(x) ⇒ Z(x).

Proof. For an object X of C, C ⊧ x_{1} = x_{2} if and only if Δ: X ↪ X × X is an isomorphism, which is equivalent to say that !_{X}: X → 1 is a monomorphism. Combining this with the fact that C ⊧ ∃x(x = x) if and only if !_{X}: X → 1 is a regular epimorphism we get the first part of the lemma.

For the second part note first that the interpretation of f(z_{1}) = f(z_{2}) ∧ g(z_{1}) = g(z_{2}) is the equaliser of ⟨f, g⟩π_{1} and ⟨f, G⟩π_{2} as in

\xymatrix{E \ar@{^{(}->}[r]^{e} & Z × Z \ar[r]^{π_{1}} \ar[r]_{π_{2}} & Z \ar[r]^{⟨f,g⟩} & X × Y.}

Then, we have seen arguments like this before, E factors through the diagonal Δ_{Z}: Z ↪ Z × Z (the interpretation of z_{1} = z_{2}) if and only if ⟨f, g⟩ is a monomorphism.

Moreover, from the following diagram of pullbacks, constructed by first pulling back the right vertical map along X → 1 and then pulling back the resulting map X × Z → X × Z × Y along Z × Y → X × Z × Y, we deduce that graph(f) × Y ∧ X × graph(g), the interpretation of f(z) = x ∧ g(z) = y, is the image of the map ⟨f, id_{Z}, g⟩: Z → X × Z × Y:

\xymatrix{Z \ar@{->>}[r] \ar@{->>}[d] & • \ar@{->>}[d] \ar@{^{(}->}[r] & X × Z \ar@{->>}[d] \ar[r] & Z \ar@{->>}[d] \\ graph(g) \ar@{->>}[r] \ar@{^{(}->}[d] & \{(x, z, y) | f(z) = x ∧ g(z) = y\} \ar@{^{(}->}[r] \ar@{^{(}->}[d] & X × graph(g) \ar[r] \ar@{^{(}->}[d] & graph(g) \ar@{^{(}->}[d] \\ Z × Y \ar@{->>}[r] & graph(f) × Y \ar@{^{(}->}[r] & X × Z × Y \ar[r] & Z × Y .}

Therefore ⟨f, g⟩ is a regular epimorphism if and only if C ⊧ ∃z(f(z) = x ∧ g(z) = y):

\xymatrix{Z \ar@{->>}[r]^{≅} \ar[drr]_{⟨f,g⟩} & • \ar@{^{(}->}[r] \ar[dr] & X × Z × Y \ar[d]^{π} \\  &  & X × Y .}

Finally, {x | fx = gx}^{(C)} is the equaliser of f and g, and because fe = ge there is a factorisation

\xymatrix{∃_{e}Z \ar@{^{(}->}[r] & \{x | fx = gx\}^{(C)} \ar@{^{(}->}[r] & X \ar[r]^{f} \ar[r]_{g} & Y . \\ Z \ar@{->>}[u] \ar[urr]_{e}}

6. The Generic Model of a Regular Theory

Then e is a mono if and only if Z → ∃_{e}Z is a monomorphism (which is equivalent to being an isomorphism since this map is a regular epimorphism), and C ⊧ f(x) = g(x) ⇒ ∃ze(z) = x if and only if the monomorphism ∃_{e}Z ↪ {x | fx = gx}^{(C)} is a regular epimorphism. These two conditions are clearly equivalent to Z being the coequaliser of f and g. □

In the previous lemmas we saw that we can characterise all those properties of a category which make it a regular category. Therefore it should be no surprise that we can describe regular functors in terms of logic as well.

If F: C → D is a functor between regular categories (not necessarily regular) we get an interpretation 𝔉 of the (functional part of the) signature S_{C} as follows:

— X^{(𝔉)} = F (X), for X ∈ \underline{sort}_{S}.

— f^{(𝔉)}: X^{(𝔉)} → Y^{(𝔉)} = F (f: X → Y), for f an arrow in C.

Proposition 5.3 The functor F is regular if and only if 𝔉 ⊧ T_{C}.

To be precise we have to restrict ourselves to those sequents φ ⇒ ψ which involve only function symbols.

Proof. One direction is just part of Lemma 3.5. For the other, if X is a terminal object then C ⊧ x_{1} = x_{2} and C ⊧ ∃x(x = x). Then 𝔉 ⊧ x_{1} = x_{2} and 𝔉 ⊧ ∃x(x = x), i.e., using the internal logic of D we see that F (X) = X^{(𝔉)} is a terminal object (by Lemma 5.2 again). In the same way one proves that F preserves products and equalisers, which can be defined using the functional part of the internal language of a category.

As well, F preserves the image factorisation of a map, hence in particular those regular epimorphisms arising as the coequaliser of the kernel pair of an arrow (and this kernel pair, being a pullback, is preserved as well). □

6 The Generic Model of a Regular Theory

The aim of this section is to show that there is a regular category R(T) and equivalences of categories

\underline{Mod}(T, C) ≅ RegCat(R(T), C),

natural in C. (This just means that the functor \underline{Mod}(T, −): RegCat → Cat is representable in a weak sense.) In particular, R(T) will contain a conservative model of T, a model in which provability in the calculus for regular logic and satisfiability coincide.

We fix T, and construct R(T) as a sort of Lindenbaum–Tarski-category:

— Objects are equivalence classes of pairs (X̄, p(x̄)) where x̄: X̄ is a finite list of sorts, and p is a regular formula. (Here X̄ is called the context of p.) Only formulae in the same context can be equivalent. Then (X̄, p_{1}(x̄_{1})) and (X̄, p_{2}(x̄_{2})) are equivalent if

T ⊢x̄ p_{1}(x̄) ⇔ p_{2}(x̄),

where x̄ is a set of fresh variables of type X̄. We denote equivalence classes by {x̄ | p} and assume that the context is understood. (Note that this notion somehow binds the variables x̄ occurring in p.)

— A morphism from {x̄ | p} to {ȳ | q} is an equivalence class of regular formulae–in–context (X̄Ȳ , γ(x̄, ȳ)) where γ is provably functional:

T ⊢_{x̄,ȳ} γ(x̄, ȳ) ⇒ p(x̄) ∧ q(ȳ)
T ⊢x̄ p(x̄) ⇒ ∃ȳγ(x̄, ȳ)
T ⊢_{x̄,ȳ_{1},ȳ_{2}} γ(x̄, ȳ_{1}) ∧ γ(x̄, ȳ_{2}) ⇒ ȳ_{1} = ȳ_{2}

(Intuitively this says that γ(x̄, ȳ) is the graph of a function.) Again, two such formulae–in–context are equivalent if they are provably equivalent in ⊢^{T}. Here we denote equivalence classes by {(x̄, ȳ) | γ(x̄, ȳ)} or simply by {γ}.

— The composition of two arrows {γ}: {x̄ | p} → {ȳ | q} and {χ}: {ȳ | q} → {z̄ | r} is given by the equivalence class of the formula

∃x̄(γ(ȳ, x̄) ∧ χ(x̄, z̄)).

(We leave it as an exercise to show that this is indeed well-defined.)

Summing up this construction we get a small category R(T).

Lemma 6.1 The category R(T) has finite limits:

(i) The object {· | ⊤} (the equivalence class of the formula–in–context (∅, ⊤)) is the terminal object in R(T).

(ii) The product of {x̄ | p} and {ȳ | q} is given by the object {(x̄, ȳ) | p ∧ q}, with projection to {x̄ | p} the equivalence class {(x̄ȳ, x̄′) | p(x̄)∧q(ȳ)∧x̄ = x̄′}, and similar for the other projection. (Here we use the comma in (x̄ȳ, x̄′) to separate source and target!)

(iii) The equaliser of two parallel arrows {γ}, {γ′}: {x̄ | p} ⇉ {ȳ | q} is the object E = {x̄ | ϵ(x̄)} for ϵ(x̄) ≡ ∃ȳ(γ(x̄, ȳ) ∧ γ(x̄, ȳ)), with inclusion the map {(x̄, x̄′) | ϵ(x̄) ∧ x̄ = x̄′}.

(iv) Given two arrows {φ}: {x̄ | p} → {z̄ | r} and {γ}: {ȳ | q} → {z̄ | r} their pullback is the object {(x̄, ȳ) | ∃z̄(φ(x̄, z̄) ∧ γ(ȳ, z̄))} with canonical projections.

We note that in our category R(T) objects like the terminal object or the product of two given objects are actually unique, and not just unique up to isomorphism. The reason is the equivalence relation we incorporated in the definition of the objects of R(T). Strictly speaking, this was not necessary (see Exercise E.13), but it facilitates our proofs.

Proof. We argue informally and make extensive use of the properties of the provability relation ⊢^{T}.

Obviously, given an arbitrary object {x̄ | p} there is at least one arrow {x̄ | p} → {· | ⊤} namely the one induced by the formula–in–context (X̄∅, p(x̄)). If there are two of them, say {γ} and {γ′}, then by definition of being arrows, γ(x̄) ⊢T ; x̄ p(x̄) and p(x̄) ⊢T ; x̄ ∃_{∅}γ′(x̄). The latter is equivalent to p(x̄) ⊢T ; x̄ γ′(x̄) so that by monotonicity of the deduction relation γ ⊢T ; x̄ γ′. By a similar argument for the other direction we conclude that modulo T, γ is provably equivalent to γ′ so that the induced arrows are identical.

For products fix {x̄ | p} and {ȳ | q}, and the two projections

\xymatrix{\{(x̄, ȳ) | p ∧ q\} \ar[r]^{\{π_{2}\}} \ar[d]_{\{π_{1}\}} & \{ȳ | q\} \\ \{x̄ | p\}}

where for example {π_{1}} is given by π_{1}(x̄, ȳ, x̄′) ≡ p(x̄) ∧ q(ȳ) ∧ x̄ = x̄′. (We leave it to the reader to check that both {π_{1}} and {π_{2}} are indeed arrows in R(T).) If {φ}: {z̄ | r} → {x̄ | p} and {γ}: {z̄ | r} → {ȳ | q} are arrows in R(T) we define

μ(z̄, x̄, ȳ) ≡ φ(z̄, x̄) ∧ γ(z̄, ȳ)

and claim that μ induces the unique arrow {z̄ | r} → {(x̄, ȳ) | p ∧ q} such that {π_{1}} ∘ {μ} = {φ} and {π_{2}} ∘ {μ} = {γ}.

Clearly, μ ⊢_{z̄,x̄,ȳ}^{T} r(z̄) ∧ (p(x̄) ∧ q(ȳ)) since φ ⊢_{z̄,x̄}^{T} r ∧ p and γ ⊢_{z̄,ȳ}^{T} q. Then

r(z̄) ⊢T ; z̄ ∃x̄φ(z̄, x̄) ∧ ∃ȳγ(z̄, ȳ) ⊢T ; z̄ ∃x̄∃ȳ(φ(z̄, x̄) ∧ γ(z̄, ȳ))

shows that μ is total. It is functional because we deduce (modulo T) from μ(z̄, x̄, ȳ) ∧ μ(z̄, x̄′, ȳ′) first φ(z̄, x̄) ∧ φ(z̄, x̄′) and then x̄ = x̄′, and similar for ȳ = ȳ′. Summing up we see that {μ} is indeed a map {x | r} → {(x̄, ȳ) | p∧q}.

The composite {π_{1}}∘{μ} is given by ∃x̄ȳ(μ(z̄, x̄, ȳ)∧p(x̄)∧q(ȳ)∧x̄ = x̄′), with free variables z̄ and x̄′. Since x̄ = x̄′ we can get rid of the existential quantifier ∃x̄, and the formula is equivalent (modulo T) to φ(z̄, x̄′) ∧ p(x̄′) ∧

∃ȳ(γ(z̄, ȳ) ∧ q(ȳ)). Because φ ⊢_{z̄,x̄}^{T} p, γ ⊢_{z̄,ȳ}^{T} q and φ(z̄, x̄′) ⊢_{z̄,x̄′}^{T} r(z̄) ⊢T ; z̄

∃ȳγ(z̄, ȳ) we deduce that {π_{1}} ∘ {μ} is induced by a formula provably equivalent to φ, and this arrow thus equals {φ}. By a similar argument the other triangle commutes.

It remains to show uniqueness: This we prove by showing that if {π_{1}} ∘ {μ} = {φ} and {π_{2}} ∘ {μ} = {γ} then T ⊢_{z̄,x̄,ȳ} μ ⇔ φ ∧ γ. The assumptions for the first triangle say that modulo T the formula φ(z̄, x̄) is equivalent to

∃x̄′ȳ′(μ(z̄, x̄′, ȳ′) ∧ p(x̄′) ∧ q(ȳ′) ∧ x̄ = x̄′),

that is, φ(z̄, x̄) ⇔ ∃ȳ′(μ(z̄, x̄, ȳ′) and similar for γ. Thus, again modulo T, φ(z̄, x̄) ∧ γ(z̄, ȳ) is equivalent to ∃ȳ′(μ(z̄, x̄, ȳ′) ∧ ∃x̄′μ(z̄, x̄′, ȳ)), which in turn is equivalent to μ(z̄, x̄, ȳ) because μ is functional and the image of z̄, i.e., the tuple (x̄, ȳ) such that μ(z̄, x̄, ȳ) is provably unique.

We leave the case of equalisers as an exercise (Exercise E.10) and note that the description of pullbacks follows from the construction of pullbacks using products and equalisers (see Exercise E.2). □

The proof of the following lemma is left as an exercise:

Lemma 6.2 An arrow {φ}: {x̄ | p} → {ȳ | q} is

(i) a monomorphism if and only if T ⊢_{x̄^{1},x̄^{2}} ∃ȳ(φ(x̄^{1}, ȳ) ∧ φ(x̄^{2}, ȳ)) ⇒ x̄^{1} = x̄^{2};

(ii) and a regular epimorphism if and only if T ⊢ȳ q(ȳ) ⇒ ∃x̄φ(x̄, ȳ). (iii) A map {p(x̄) ∧ x̄ = x̄′}: {x̄ | p} → {x̄ | q} is a monomorphism if and

only if T ⊢x̄ p ⇒ q. □

Proposition 6.3 R(T) is a regular category.

Proof. ¿From Lemma 6.1 we know that R(T) has finite limits. In a pullback diagram

\xymatrix{\{(ȳ, x̄) | ∃z̄(γ ∧ φ)\} \ar[r] \ar[d]_{\{π\}} & \{x̄ | p\} \ar[d]^{\{φ\}} \\ \{ȳ | q\} \ar[r]_{\{γ\}} & \{z̄ | r\}}

the map {π} is induced by π(ȳ, x̄, ȳ′) = ∃z̄(γ ∧ φ) ∧ ȳ = ȳ′.

Suppose φ is a regular epimorphism, i.e., ⊢z̄ r(z̄) ⇒ ∃x̄φ(x̄, z̄). Then from q(ȳ) we deduce ∃z̄γ(ȳ, z̄), which is equivalent to ∃z̄(γ(ȳ, z̄) ∧ r(z̄)). Modulo T we can deduce further (using the assumption) ∃z̄(γ(ȳ, z̄) ∧ ∃x̄φ(x̄, z̄)). By Lemma 4.2 this is provably equivalent to ∃x̄∃z̄(γ(ȳ, z̄) ∧ φ(x̄, z̄)) (we interchanged the existential quantifiers), as we wanted. So regular epimorphisms are stable under pullbacks. □

The category R(T) contains a natural interpretation U of the underlying language L(S):

— X^{(U)} = {x | x = x}, where x is some variable of type X.

— c^{(U)} = {x | x = c}: {· | ⊤} → X^{(U)}, for each constant in the underlying language.

— f^{(U)} = {x̄, y) | f(x̄) = y}, for each function symbol f: X̄ → Y in \underline{funct}_{S}. We note that this is indeed an arrow in our category by Exercise E.12. Furthermore we use that X̄^{(U)} = X_{1}^{(U)} × ⋯ × X_{n}^{(U)}.

— R^{(U)} = {x̄ | R(x̄)}, which is easily seen to be a subobject of X̄^{(U)}.

An easy induction shows that for terms t(z̄) of type Y,

t(z̄)^{(U)} = {(z̄, y) | t(z̄) = y},

an arrow Z̄^{(U)} → Y^{(U)}; and for regular formulae φ(z̄) that

{z̄ | φ}^{(U)} = {z̄ | φ}.

It follows that U is a model of T: If p ⇒ q is a sequent in T then {(x̄, x̄′) | p(x̄) ∧ x̄ = x̄′} is a monomorphism from {x̄ | p} to {x̄ | q}, so that indeed {x̄ | p}^{(U)} ≤ {x̄ | q}^{(U)}. The model U has the additional property that it is conservative, i.e., for all sequents p ⇒ q,

if U ⊧ p ⇒ q then T ⊢x̄ p ⇒ q.

Indeed, if U is a model of p ⇒ q then in R(T) there is a monomorphism {p(x̄) ∧ x̄ = x̄′}: {x̄ | p} → {x̄ | q}, so by Lemma 6.2(iii), T ⊢x̄ p ⇒ q. For the record:

Proposition 6.4 The canonical interpretation U in the regular category R(T) is a conservative model of T. In particular, the calculus given above is complete with respect to interpretations in (small) regular categories. □

We are now ready to define the functors involved in the equivalence \underline{Mod}(T, C) ≅ RegCat(R(T), C), natural in C.

The functor 𝔐_{C}: RegCat(R(T), C) → \underline{Mod}(T, C) is the functor 𝔐_{U,C} from the end of Section 3, which sends a functor F: R(T) → C to the model F_{T} (U) in C, and a natural transformation α: F ⇒ G to the family

F_{T} (α) = \{α_{X^{(U)}}: F (X^{(U)}) → G(X^{(U)})\}_{X∈\underline{sort}_{S}}.

The functor 𝔉_{C}: \underline{Mod}(T, C) → RegCat(R(T), C) sends a model M of T in C to the functor

𝔉_{C}(M): R(T) → C
{x̄ | p} ↦ {x̄ | p}^{(M)}

{γ}: {x̄ | p} → {ȳ | q} ↦ ‘the unique arrow f: {x̄ | p}^{(M)} → {ȳ | q}^{(M)} such that graph(f) = {(x̄, ȳ) | γ}^{(M)}’.

(The map f in the arrow part exists by Lemma 2.8. Uniqueness of this map ensures that we really got a functor.) Soundness of the calculus and the fact that being a model is defined using the internal logic of C proves that 𝔉_{C}(M) is a regular functor. A morphism between models h: M → N gives rise to a family of maps

h_{{x̄|p}}: {x̄ | p}^{(M)} → {x̄ | p}^{(N)}

7. Epilogue

(see the discussion at the end of Section 3) which is natural because if we have a map {γ}: {x̄ | p} → {ȳ | q} then, since both squares below commute, the outer does as well and that is just the naturality square:

\xymatrix{\{x̄ | p\}^{(M)} \ar@{->>}[d] \ar[r]^{h_{\{x̄|p\}}} & \{x̄ | p\}^{(N)} \ar@{->>}[d] \\ \{ȳ | ∃x̄γ(x̄, ȳ)\}^{(M)} \ar[r]^{h_{\{ȳ|∃x̄γ(x̄,ȳ)\}}} \ar@{^{(}->}[d] & \{ȳ | ∃x̄γ(x̄, ȳ)\}^{(N)} \ar@{^{(}->}[d] \\ \{ȳ | q\}^{(M)} \ar[r]_{h_{\{ȳ|q\}}} & \{ȳ | q\}^{(N)}}

This functor is again natural in C: If F: D → C is a regular functor then

\xymatrix{\underline{Mod}(T, D) \ar[r]^{𝔉_{D}} \ar[d]_{F_{T}} & RegCat(R(T), D) \ar[d]^{F ∘(−)} \\ \underline{Mod}(T, C) \ar[r]_{𝔉_{C}} & RegCat(R(T), C)}

commutes. We conclude with the following theorem:

Theorem 6.5 The functors 𝔐_{C} and 𝔉_{C} induce an equivalence of categories

\underline{Mod}(T, C) ≅ RegCat(R(T), C),

natural in C. Up to equivalence any small regular category C arises this way as the ‘classifying category, of a regular theory since C ≅ R(T_{C}).

Proof. It is straightforward from the explicit definition that both ways round are isomorphic to the identity. The second part follows from Proposition 5.3.

□

7 Epilogue

In these notes we saw a close connection between a fragment of first-order logic and a particular class of categories. The material of these notes is treated more or less detailed (more ‘less detailed’) in [12, 2, 4]. Similar results hold for the following pairs:

geometric (coherent) logic  geometric categories
intuitionistic first–order logic  Heyting categories
classical first–order logic  Boolean categories
higher–order logic  (elementary) toposes
typed λ–calculus  cartesian closed categories
∑-∏-part of Martin-Löf type theories locally cartesian closed categories.

Good references are for geometric logic^{7} [8], for first-order logic [4], for higher–order logic and for the λ–calculus [7], and for Martin Löf type theories the paper [11].

There is a natural Grothendieck topology on a regular category, and the sheafified Yoneda embedding into the sheaf topos over this site preserves and reflects all the regular structure (and more). This explains similar results as in this note for (infinitary) geometric logic and Grothendieck toposes, the classical treatment of which is contained in [9]. The situation for first–order logic and Grothendieck toposes is not as good, but still there are strong results (like completeness, etc), see the references [6, 3, 10]. The existence of classifying toposes for geometric theories is already implicit in the thesis of M. Hakim [5]. She showed among other things that the Zariski topos classifies local rings, and the associated étale topos classifies henselian local rings.

Finally, there is a completely different approach to categorical logic, based on sketches. Roughly speaking, a sketch is a category equipped with two classes of diagrams. A model of such a sketch is a functor into some category sending the first class of arrows to limit-diagrams, and the second to colimitdiagrams. Thus, a sketch is something like a theory, and restrictions on the class of diagrams allowed (finite, or finite and only limit-diagrams, …) specify in which language this theory is formulated. Here one could start reading in [2, 1].

Exercises

E.1 Let C be a category with finite limits and \xymatrix{E \ar@{^{(}->}[r] & X \ar[r]^{p_{1}} \ar[r]_{p_{2}} & Y} an equaliser

diagram. For an arbitrary object Z we get the equaliser E′ of the two parallel arrows \xymatrix{X × Z \ar[r]^{p_{1}×id_{Z}} \ar[r]_{p_{2}×id_{Z}} & Y × Z}. Show that E′ = π^{−1}E for π the projection X ×

7Geometric logic is obtained by replacing regular formulae by those built from atomic formulae, the logical constants ⊥ and ⊤, the binary operations ∧ and ∨ and existential quantification ∃.

Y → X.

E.2 Show that the pullback X ×_{Z} Y of f: X → Z and g: Y → Z can be constructed as the pullback of f × g along the diagonal Δ_{Z} as in

\xymatrix{X ×_{Z} Y \ar@{^{(}->}[r] \ar[d] & X × Y \ar[d]^{f×g} \\ Z \ar@{^{(}->}[r]_{Δ_{Z}} & Z × Z.}

(Here Δ_{Z} is the unique map ⟨id_{Z}, id_{Z}⟩.)

E.3 Prove that the graph of an arrow f: X → Y in C gives a total and functional relation on (subobject of) X × Y.

E.4 Show that for an arrow f: X → Y the monomorphism graph(f) ↪ X × Y is the equaliser of the two parallel arrows fπ_{1}, π_{2}: X × Y ⇉ Y.

E.5 Prove that the category of groups is regular. Can you do the same for the category of rings?

E.6 An abelian group G is torsion-free if for all natural numbers n ≥ 1 and all elements g ∈ G, n·g = 0 implies g = 0. Show that the category tfAb of torsion-free abelian groups (which is a full sub-category of the category of abelian groups) is regular.

E.7 Show that Top, the category of topological spaces, has all finite limits and all coequalisers. Given an example of a regular epimorphism that is not stable under pullbacks. Conclude that Top is not regular.

E.8 Let C be a (small) regular category, D a (small) category. Show that the functor category [D, C] is regular.

E.9 Let C be a regular category. Prove that the slice category C/C is again regular for each object C in C.

E.10 Complete in the proof of Lemma 6.1 the description of equalisers.

E.11 Provide the proof of Lemma 6.2.

E.12 Verify that if f: X̄ → Y is a function symbol in some language then {(x̄, y) | f(x̄) = y} is a morphism in R(T) from {x̄ | x̄ = x̄} to {y | y = y}. (Here T is some fixed theory formulated in the underlying language.)

E.13 Define a category R′(T) similar as R(T), but using as objects formulae– in–contexts instead of equivalence classes thereof. Prove that R′(T) is equivalent to R(T). Can you use for arrows as well formulae–in–contexts instead of equivalence classes?

In the next couple of exercises we develop some forcing semantics for regular logic. We fix the internal logic L(S_{C}) of a regular category C. For a sort X, a generalised element at stage U is an arrow α: U → X. For a formula φ(x) with free variable x: X and a generalised element α we say that U forces φ(α) (in symbols: U ⊩ φ(α)) if α factors through {x | φ}^{(C)}, i.e., if ∃_{α}(U) ≤ {x | φ}^{(C)} in Sub(X). This definition extends immediately to formulae with more free variables. For f an arrow U′ → U we write α↾f for the generalised element α ∘ f at stage U′.

E.14 Prove the following two properties of the forcing relation:

(i) (Monotonicity.) If U ⊩ φ(α) then for any f: U′ → U, also U′ ⊩ φ(α↾f). (ii) (Local character.) If f: U′ ↠ U is a regular epimorphism and U′ ⊩ φ(α↾f),

then U ⊩ φ(α). [Hint: Show first that {x | φ}^{(C)} ↪ X pulled back along α ∘ f is an isomorphism and deduce then that {x | φ}^{(C)} ↪ X pulled back along α is already an isomorphism.]

E.15 Show that the forcing relation in a regular category obeys the following rules:

(i) U ⊩ ⊤ always holds. (ii) U ⊩ φ(α) ∧ ψ(α) if and only if U ⊩ φ(α) and U ⊩ ψ(α). (iii) U ⊩ ∃yφ(y, α) if and only if there exists a regular epimorphism p: V ↠ U and

a generalised element β: V → Y such that V ⊩ φ(β, α↾p). (iv) Suppose that t_{1} and t_{2} are terms of type Y with free variable x. Show that

U ⊩ t_{1}(α) = t_{2}(α) if and only if t_{1}^{(C)}α = t_{2}^{(C)}α: U → X ⇉ Y.

E.16 Extend the forcing relation to sequents φ ⇒ ψ by U ⊩ φ(α) ⇒ ψ(α) if for all arrows f: U′ → U, if U′ ⊩ φ(α↾f) then U′ ⊩ ψ(α↾f).

(i) Show that C ⊧ φ(x) if and only if for all U and all generalised elements α: U → X, U ⊩ φ(α).

(ii) Conclude that for a sequent φ(x) ⇒ ψ(x), C ⊧ φ ⇒ ψ iff for all U in C and all α: U → X, if U ⊩ φ(α) then U ⊩ ψ(α).

REFERENCES

References

[1] M. Barr and C. Wells. Category Theory for Computing Science. Prentice Hall, New York 1990.

[2] F. Borceux. Handbook of Categorical Algebra. Vol. 1, 2 and 3. Cambridge University Press, Cambridge 1994.

[3] C. Butz and P. T. Johnstone. Classifying toposes for first-order theories. Ann. Pure Appl. Logic, 91:33-58, 1998.

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

[5] M. Hakim. Topos Anneles et Schemas Relatifs. Springer–Verlag, Berlin 1972.

[6] P. Johnstone. Open maps of toposes. Manuscripta Math. 31:1980, no. 1-3, 217–247.

[7] J. Lambek and P. J. Scott. Introduction to Higher Order Categorical Logic. Cambridge University Press, Cambridge 1986.

[8] S. Mac Lane and I. Moerdijk. Sheaves in Geometry and Logic. Springer– Verlag, New York 1992.

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

[10] E. Palmgren. Constructive sheaf semantics. Math. Logic Quart. 43:1997, no. 3, 321–327.

[11] R. A. G. Seely. Locally Cartesian closed categories and type theory. Math. Proc. Cambridge Philos. Soc. 95:1984, no. 1, 33–48.

[12] J. van Oosten. Basic Category Theory. BRICS Lecture Series, LS-95-1, January 1995.

Recent BRICS Lecture Series Publications

LS-98-2 Carsten Butz. Regular Categories and Regular Logic. October

1998. LS-98-1 Ulrich Kohlenbach. Proof Interpretations. June 1998.

LS-97-1 Jan Chomicki and David Toman. Temporal Logic in Information Systems. November 1997. viii+42 pp. Full version appears in Chomicki and Saake, editors, Logics for Database and Information Systems, 3:31–70, Kluwer Academic Publishers, 1998.

LS-96-6 Torben Braüner. Introduction to Linear Logic. December 1996. iiiv+55 pp.

LS-96-5 Devdatt P. Dubhashi. What Can’t You Do With LP? December 1996. viii+23 pp.

LS-96-4 Sven Skyum. A Non-Linear Lower Bound for Monotone Circuit Size. December 1996. viii+14 pp.

LS-96-3 Kristoffer H. Rose. Explicit Substitution – Tutorial & Survey. September 1996. v+150 pp.

LS-96-2 Susanne Albers. Competitive Online Algorithms. September 1996. iix+57 pp.

LS-96-1 Lars Arge. External-Memory Algorithms with Applications in Geographic Information Systems. September 1996. iix+53 pp.

LS-95-5 Devdatt P. Dubhashi. Complexity of Logical Theories. September 1995. x+46 pp.

LS-95-4 Dany Breslauer and Devdatt P. Dubhashi. Combinatorics for Computer Scientists. August 1995. viii+184 pp.

LS-95-3 Michael I. Schwartzbach. Polymorphic Type Inference. June 1995. viii+24 pp.

LS-95-2 Sven Skyum. Introduction to Parallel Algorithms. June 1995. viii+17 pp. Second Edition.

LS-95-1 Jaap van Oosten. Basic Category Theory. January 1995. vi+75 pp.