# «COMPACTNESS AND ¨ LOWENHEIM–SKOLEM PROPERTIES IN CATEGORIES OF PRE-INSTITUTIONS ANTONINO SALIBRA University of Pisa, Dip. Informatica Corso Italia ...»

Full adequacy of R follows from Proposition 3.7 and Lemma 6.6.5.

Expansion-adequacy of R is shown as follows: ∀τ : Σ1 → Σ2 ∈ SigL, ∀M2 ∈

**ModI (Σ2R ), ∀M1 ∈ ModL (Σ1 ):**

ˆ M2 τR ∈ M1R ⇒ M1 ∈ (M2 τR )T (by Deﬁnition 6.6.2(i)) ⇒ M1 ∈ M2T τ (naturality of model transformation in T and Deﬁnition 6.6.1) ⇒ ∃M2 ∈ ModL (Σ2 ) : M1 = M2 τ ∧ M2 ∈ M2T ⇒ ∃M2 ∈ ModL (Σ2 ) : M1 = M2 τ ∧ M2 ∈ M2R (by Deﬁnition 6.6.2(i)).

Finitarity of R is an immediate consequence of Lemma 6.6.15 and of the construction of the mapping of presentations as in Lemma 6.6.7.

As we mentioned above, Theorem 6.6 does not generalize the recalled lemma from [6] because it only applies to abstract pre-institutions. A proper generalization of the recalled lemma does exist, however, and is as follows.

In the ﬁrst place, the hypothesis that L is abstract plays no rˆle in the proof o of Theorem 6.6, thus it can be removed.

ˆ In the second place, we note that the only place where the abstractness of I is made use of in the proof of Theorem 6.6 is Lemma 6.6.18, which shows the naturality of presentation transformation by R.

ˆ Now, consider the variant of Theorem 6.6 that is obtained by replacing I with ILI, the ﬁrst-order pre-institution with only renamings as signature morphisms— according to Example 2.9, and by relaxing ﬁnitarity of R to quasi-ﬁnitarity. This variant of Theorem 6.6 holds as well, as we are going to argue by a simple proof adaptation, and it is easy to see that it properly generalizes the recalled lemma from [6].

The required proof adaptation is as follows.

Starting from Lemma 6.6.15, the abstract ﬁrst-order sentence ψR is now to be seen as a ﬁrst-order presentation. Then the deﬁnition of ER in Lemma 6.6.17 becomes ER = ψ∈E ψR, which clearly makes R meet quasi-ﬁnitarity. Finally, consider Lemma 6.6.18. ψR is now a ﬁrst-order presentation; more precisely, it is the elementary equivalence class of a ﬁrst-order sentence. So is τR ψR, since τR is a ﬁrst-order signature isomorphism. And obviously, so is (τ ψ)R as well. Since the presentations τR ψR and (τ ψ)R have exactly the same models, by a proof analogous to that of Lemma 6.6.18, and since both presentations are elementary equivalence classes of a ﬁrst-order sentence, they must consist of the same sentences, i.e. they coincide. The identity τR ER = (τ E )R then follows from the elementwise construction of ER.

## PRE-INSTITUTIONS

7. Cardinal pre-institutions and L¨wenheim–Skolem properties. To o begin with, we note that the properties expressed in the L¨wenheim–Skolem theoo rems (both Downward and Upward, see e.g. [4]) refer to the cardinality of models;

moreover, the cardinality of symbol sets (generalized by signatures, in our context) play a rˆle in generalizations of these theorems, such as the L¨wenheim–Skolem– o o Tarski theorem.

In pre-institutions, models as well as signatures are viewed as “points” in the general case, that is, abstraction is made from any internal structure they may have. The treatment of (general forms of) the L¨wenheim–Skolem properties thus o requires the following concept.

Definition 7.1. A pre-institution with cardinal numbers, K = (I, #), or cardinal pre-institution for short, is a pre-institution I as in Deﬁnition 2.1 together with a function # that assigns a cardinal number #Σ to each signature Σ, as well as a cardinal number #M to each model M, also called the power of Σ or M respectively, and that meets the following conditions, for all signature morphisms

**τ : Σ1 → Σ2 and Σ2 -models M :**

1. if τ is monic then #Σ1 ≤ #Σ2,

2. if τ is epic then #Σ1 ≥ #Σ2, 3. #M ≥ #M τ.

In abstract model theory, L¨wenheim numbers tell the strength of downward o L¨wenheim–Skolem theorems. The transfer of their deﬁnition to pre-institutions o is straightforward (cf. Def. 6.2.1 in [5]).

Definition 7.2. Let K be a cardinal pre-institution and κ a cardinal. lκ (K) is the least cardinal µ such that every satisﬁable set of sentences of power ≤ κ has a model of power ≤ µ, provided there is such a cardinal; otherwise, lκ (K) = ∞.

def l(K) = l1 (K) is called the L¨wenheim number of K.

o The L¨wenheim number of a cardinal pre-institution is thus the least cardinal o µ such that every satisﬁable sentence has a model of power at most µ, provided such a cardinal exists. Then, not unlike an abstract logic, a cardinal pre-institution K has the L¨wenheim–Skolem property down to λ iﬀ l(K) ≤ λ.

o Hanf numbers are the upward counterpart of L¨wenheim numbers.

o Definition 7.3. Let K be a cardinal pre-institution and κ a cardinal. hκ (K) is the least cardinal µ such that every set of sentences of power ≤ κ has models of arbitrarily large cardinality if it has a model of power ≥ µ, provided there is such a cardinal; otherwise, hκ (K) = ∞.

def h(K) = h1 (K) is called the Hanf number of K.

The Hanf number of a cardinal pre-institution is thus the least cardinal µ such that every sentence satisﬁable by a model of power at least µ has models of arbitrarily larger power, provided such a cardinal exists.

90 A. SALIBRA AND G. SCOLLO A classical result in abstract model theory, viz. the Hanf theorem (1960) (see e.g. Thm. 6.1.4 in [5]), guarantees existence of Hanf numbers for abstract logics under certain “smallness” conditions. The same conditions guarantee existence of L¨wenheim numbers as well, by a similar argument (see e.g. Prop. 2.5.2 in [4]).

o The formulation of analogous conditions for pre-institutions requires the following notion.

Definition 7.4. Let I be a pre-institution as in Deﬁnition 2.1. A renaming in I is an isomorphism : Σ1 Σ2 in Sig. Moreover, we say that any two signatures Σ1, Σ2 ∈ Sig are renaming-equivalent in I, written Σ1 Σ2, iﬀ there exists a Σ2 in Sig. As a matter of notation, if Σ ∈ Sig, [Σ] denotes renaming : Σ1 the renaming-equivalence class that contains Σ.

For cardinal pre-institutions, the following is hardly surprising.

** Lemma 7.5.**

If : Σ1 Σ2 is a renaming in a cardinal pre-institution K as in Deﬁnition 7.1, then #Σ1 = #Σ2, #M2 = #M2, and #M1 = #M1 −1, for all M1 ∈ Mod(Σ1 ) and M2 ∈ Mod(Σ2 ).

P r o o f. Immediate consequence of Deﬁnitions 7.1 and 7.4.

We are now ready to formulate smallness conditions for pre-institutions, that will permit us to lift the Hanf theorem to our framework.

Definition 7.6 (small pre-institution). A pre-institution I is small iﬀ it meets

**the following conditions:**

(i) the renaming equivalence of signatures in I has a small set of equivalence classes, (ii) for every signature Σ in I the set of Σ-sentences is small.

Smallness of a cardinal pre-institution K = (I, #) is just smallness of the underlying pre-institution I, thus independent of the size of signatures or of models that is deﬁned by #.

Finally, the following property is a weaker form of the ps property (see Deﬁnition 2.2), since it requires satisfaction invariance only for renamings; this closely reﬂects the renaming property of general logics, in the sense of [5].

Definition 7.7. Let I be a pre-institution as in Deﬁnition 2.1; I has the

**renaming property iﬀ it meets the following requirement:**

∀ : Σ1 Σ2 ∈ Sig : ∀ϕ ∈ Sen(Σ1 ), ∀M ∈ Mod(Σ2 ) : M ϕ⇔M ϕ.

The lifting of the Hanf theorem to pre-institutions now follows. The set-theoretic axiom of replacement plays a key rˆle, as in the proof of the classical Hanf o theorem.

Proposition 7.8. Let K be a cardinal pre-institution as in Deﬁnition 7.1. If K has the renaming property and is small, then both its L¨wenheim number and o its Hanf number exist.

## PRE-INSTITUTIONS

P r o o f. Let K be a cardinal pre-institution as in the hypothesis. By the axiom**of choice, a small set H of signatures exists such that ∀Σ ∈ Sig: [Σ] ∩ H is a singleton. We note that the renaming property of K has the following consequence:**

Σ1, then a renaming : Σ → Σ1 exists, and by Lemma 7.5 and Deﬁniif Σ tion 7.7 a power-preserving bijection between the models of ϕ and those of ϕ exists, for every ϕ ∈ Sen(Σ). Now, for each Σ ∈ H and ϕ ∈ Sen(Σ), let αϕ be ∞ if ϕ has no model, or otherwise the least cardinal µ such that µ = #M for some model M of ϕ. By the axiom of replacement, the set {αϕ | ϕ ∈ Sen(Σ), Σ ∈ H} is small, thus its least upper bound exists, and this is the L¨wenheim number of o K thanks to the aforementioned consequence of the renaming property of K.

The existence of the Hanf number of K has a similar proof.

For the applicability of our form of the “reduction scheme” to L¨wenheim– o Skolem properties along pre-institution transformations, these need the following property. We say that a transformation on cardinal pre-institutions preserves

**model power if model power never decreases along the transformation. More precisely:**

Definition 7.9. Let T : K → K be a transformation on cardinal pre-institutions K = (I, #), K = (I, # ), with T : I → I as in Deﬁnition 2.3. We say that

**T : K → K preserves model power iﬀ ∀Σ ∈ Sig, ∀M ∈ Mod(Σ), ∀M ∈ MT :**

#M ≤ # M.

** Theorem 7.10.**

Let K, K be cardinal pre-institutions as in Deﬁnition 7.9. If there exists an adequate transformation T : K → K that preserves model power

**and meets the following condition for cardinals µ, ν: ∀Σ ∈ Sig, ∀E ∈ Pre(Σ):**

|E| ≤ µ ⇒ |(ET − TautT (Σ))/≡I | ≤ ν, then lν (K) ≤ lν (K ).

P r o o f. Let Σ ∈ Sig, E ∈ Pre(Σ), with |E| ≤ µ, E satisﬁable. If M E, then MT ET by the satisfaction invariant, and MT is non-empty. Thus ET is satisﬁable, and |(ET − Taut T (Σ))/≡I | ≤ ν by the hypothesis. Now, let E consist of one sentence for each equivalence class in (ET − TautT (Σ))/ ≡I, thus |E | ≤ ν. Clearly, E is satisﬁable iﬀ so is ET −TautT (Σ); moreover, the adequacy of T entails that ET TautT (Σ), by Proposition 3.4. Therefore E is satisﬁable because so is ET ; the fact that |E | ≤ ν further entails that E has a model M with # M ≤ lν (K ). Then, by the construction of E and since ET TautT (Σ), M is a model of ET as well, hence the adequacy of T entails the existence of a model N of E such that M ∈ NT. Since T preserves model power, we infer #N ≤ # M ≤ lν (K ). Thus every satisﬁable E of power at most µ has a model of power at most lν (K ), which is what we had to prove.

92 A. SALIBRA AND G. SCOLLO

8. Related work (9 ). This work shares with [2] the motivation for focussing on the morphisms of institution categories more than on their objects.

Clearly, a reason for this is the interest that institution-independent speciﬁcation [19] and general logics [5, 15] naturally ﬁnd in computer science. It may be source of some surprise, thus, that so far no general agreement has been reached on the most convenient notion of institution morphism. A careful analysis and comparison of several, quite distinct such notions can be found in [2]. To that, we wish to add the following, necessarily quick and preliminary considerations.

In comparison with the notions of institution morphism proposed in [9, 15, 2], our notion is the only one where the three arrows (respectively relating to signatures, sentences, models) are all covariant. Of those three notions, the one which seems closest to ours is that of basic simulation [2], which essentially diﬀers from ours in two respects: 1) it sends sentences to sentences, whereas ours sends presentations to presentations, and 2) model transformation is contravariant, but by a surjective, partial natural transformation. The latter could thus be turned into a covariant, total natural transformation, sending models to sets of models, like in our case. Of course, the model sets ought to be disjoint; this condition, arising from well-deﬁnedness of the model transformation as deﬁned for basic simulations, closely corresponds to the suﬃcient condition for full adequacy given in Lemma 2.6 above—modulo some equivalence of models in the source institution, however.

Although we are more interested in the morphisms than in the objects, the less restrictive deﬁnition of the objects in our framework also contributes to widening the applicability of abstract model-theoretic tools in algebraic speciﬁcation.

Most of the speciﬁcation frameworks studied so far ﬁt the institutions scheme, yet not all of them do. Cases where (at least the eps half of) the satisfaction condition is known to fail include equational type logic with non-standard reduction (as exempliﬁed in Section 5 of [18]) and, most notably, behavioural semantics [3, 16, 17]. These frameworks ﬁt the pre-institutions scheme, as well as the drastically general scheme proposed in [7]—where hardly anything of the abstract model-theoretic approach underlying the theory of institutions can be recognized, however.

9. Future work. We conclude with a list of topics that currently attract our interest, and which seem to deserve further investigation along, and as a test of, the approach presented in this paper.

• Generalization of compactness notions and results to (κ, λ)-compactness [11], which is of interest in the study of inﬁnitary logics.

(9 ) In this paper, we conﬁne ourselves to the comparison proposed in Section 6 of [18].

In future work of ours we intend to oﬀer a more extensive comparison with related work [1], together with an exploration of connections with other topics in the ﬁeld of algebraic logic.

## PRE-INSTITUTIONS

• Investigation of the applicability of the reduction scheme, as generalized here, to other properties such as: Beth deﬁnability, Craig interpolation, Robinson property, Karp property, freeness, initiality, etc.

• Lindstr¨m theorems.

o

• Expressiveness applications.

[1] H. A n d r´ k a, I. N´ m e t i and I. S a i n, Abstract model theoretic approach to algebraic logic, e e manuscript, Mathematical Institute, Budapest, 1984.