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

(7 ) Of which we give the proof here, since this fact was not made explicit in [18].

## PRE-INSTITUTIONS

(i) ∀Σ ∈ Sig, ∀M ∈ Mod(Σ), ∀E ∈ Pre(ΣT ): M ∈ (MT )R ∧ (M ER ⇒ MT E ), (ii) ∀Σ ∈ Sig, ∀M ∈ Mod(Σ): M ∈ (MT )R ∧ (MT )R ⊆ Mod(Th(M )).The conditions in the previous proposition also ensure full adequacy of the inverse transformation, as shown by the following Proposition 3.7. If R : I → I is an inverse of T : I → I such that M ∈ (MT )R holds for every model M in I, then (i) R is fully adequate, (ii) R ◦ T is fully adequate.

Finally, the following result shows the contravariant inheritance of (two forms of) compactness by suitable pre-institution transformations.

** Theorem 3.8 (Compactness).**

Let T : I → I be a fully adequate pre-institution transformation, with I, I as in Deﬁnition 2.3.

(i) I compact ⇒ I compact.

(ii) (I consequence-compact ∧ T quasi-ﬁnitary) ⇒ I consequence-compact.

4. Compact transformations. Roughly, a notion of compact transformation is obtained by taking a notion of compactness as introduced for pre-institutions, and “stretching it along the arrow”. Thus, compactness (for satisfaction) of a transformation relates satisﬁability of a translated presentation to satisﬁability of the translation of every ﬁnite subpresentation. Similarly, consequencecompactness of a transformation relates consequence from a translated presentation to consequence from the translation of some ﬁnite subpresentation. More precisely, we propose the following Definition 4.1 (Transformation compactness). Let T : I → I be a preinstitution transformation, with I, I as in Deﬁnition 2.3.

(i) T is compact iﬀ ∀Σ ∈ Sig, ∀E ∈ Pre(Σ): (∀F ⊆ E: F ﬁnite ⇒ FT satisﬁable) ⇒ ET satisﬁable.

(ii) T is consequence-compact iﬀ ∀Σ ∈ Sig, ∀E ∈ Pre(Σ), ∀ϕ ∈ Sen (ΣT ):

ϕ ⇒ ∃F ⊆ E : F ﬁnite ∧ FT ET ϕ.

A number of relationships link compactness of (fully) adequate transformations to compactness of their source and target pre-institutions. These relationships are collected in the following theorem, which subsumes and reﬁnes Theorem 3.8.

** Theorem 4.2 (Transformation compactness).**

Let T : I → I be an adequate pre-institution transformation, with I, I as in Deﬁnition 2.3.

(i) T compact ⇔ I compact.

80 A. SALIBRA AND G. SCOLLO (ii) (T fully adequate ∧ I compact) ⇒ T compact.

(iii) (T quasi-ﬁnitary ∧ T consequence-compact) ⇒ I consequence-compact.

(iv) (T fully adequate ∧ I consequence-compact) ⇒ T consequence-compact.

P r o o f. (i) (⇒) Let E be a ﬁnitely satisﬁable Σ-presentation in I, thus for every ﬁnite F ⊆ E there is a Σ-model MF such that MF F ; then the non-empty FT by the satisfaction invariant, thus compactness of T entails that (MF )T ET is satisﬁable, whence satisﬁability of E follows from the adequacy of T.

(⇐) Let E be a Σ-presentation in I, with FT satisﬁable for every ﬁnite F ⊆ E; then adequacy of T entails F satisﬁable for every ﬁnite F ⊆ E, whence E satisﬁable follows from compactness of I, and therefore ET is satisﬁable, by the satisfaction invariant.

(ii) Immediate consequence of (i) and Theorem 3.8(i).

(iii) Let Σ ∈ Sig, ϕ ∈ Sen(Σ), and E ∈ Pre(Σ), with E ϕ. Let F be a set consisting of one representative per equivalence class in (ϕT − TautT (Σ))/ ≡I ;

thus F is ﬁnite, since T is quasi-ﬁnitary. Then ET F, since ET ϕT, which follows from Proposition 3.3(ii) and adequacy of T. Moreover, consequence-compactness of T entails that for each ψ ∈ F there is a ﬁnite Fψ ⊆ E such that (Fψ )T ψ, thus ψ∈F ((Fψ )T ) F, whence ( ψ∈F Fψ )T F follows from Proposition 3.3(iii) and adequacy of T.

Let then F = ψ∈F Fψ. Since ϕT ≡I TautT (Σ) ∪ F, and FT TautT (Σ) by Proposition 3.4 and adequacy of T, we infer FT ϕT, whence F ϕ follows from Proposition 3.3(i). Since F ⊆ E and F is ﬁnite, we conclude that I is consequence-compact.

(iv) Let Σ ∈ Sig, ψ ∈ Sen (ΣT ), and E ∈ Pre(Σ), with ET ψ. Since T is ψ. Since I is consequencefully adequate, Proposition 3.3(iv) entails ϕ∈E ϕT compact, there is a ﬁnite F ⊆ ϕ∈E ϕT such that F ψ. Now, for each ξ ∈ F pick a ϕξ ∈ E such that ξ ∈ (ϕξ )T. Then F ⊆ ξ∈F (ϕξ )T. Let F = {ϕξ | ξ ∈ F }. Clearly, F ⊆ E and F ﬁnite, and F ⊆ ϕξ ∈F (ϕξ )T, hence ϕξ ∈F (ϕξ )T ψ.

Then, by adequacy of T, Proposition 3.3(iii) entails FT ψ.

Corollary 4.3. Theorem 3.8(ii) is an immediate consequence of Theorem 4.2(iii) and (iv).

** Theorem 4.2 thus reﬁnes Theorem 3.**

8 in that it splits the backward inheritance, or “reduction” of compactness, “in two halves”: a “source half”, whereby the source pre-institution inherits compactness from the transformation, and a “target half”, whereby the transformation inherits compactness from the target pre-institution.

The reﬁnement is informative, in that it gives appropriate place to the hypotheses that appear in Theorem 3.8, viz.: 1) the target half of the reduction to full adequacy, for both notions of compactness, and 2) the source half of the reduction to adequacy, for both notions of compactness, and to quasi-ﬁnitarity for consequence-compactness.

## PRE-INSTITUTIONS

** The reﬁnement will prove useful in Theorem 6.6, precisely, in Lemma 6.6.12therein.**

5. Abstract sentences, expansion adequacy. We are going to introduce a notion of abstract pre-institution that seems consistent with the abstract modeltheoretic purpose proposed in [11], that we quoted in Section 2 above. Abstraction, in the sense of the following deﬁnition, essentially applies to logically equivalent sentences, in the sense that no distinction is drawn between sentences that have exactly the same models.

Definition 5.1 (Abstract pre-institution). A pre-institution I = (Sig, Sen, Mod, ) has abstract sentences, or is abstract, iﬀ it meets the following requirement: ∀Σ ∈ Sig, ∀ϕ, ψ ∈ Sen(Σ): Mod(ϕ) = Mod(ψ) ⇒ ϕ = ψ.

Abstraction can be applied to every pre-institution that has the ps property by the obvious quotient construction. To each ps pre-institution an abstract form of it corresponds, thus. This is formalized as follows.

**Definition 5.2. For each ps pre-institution I = (Sig, Sen, Mod, ), the abstract pre-institution I = (Sig, Sen, Mod, ) is deﬁned as having the same category of signatures and model functor, and:**

(i) ∀Σ ∈ Sig: Sen (Σ) = {[ϕ]≡I | ϕ ∈ Sen(Σ)}, (ii) ∀τ : Σ1 → Σ2 ∈ Sig, ∀ϕ ∈ Sen(Σ1 ): Sen (τ )[ϕ]≡I = [Sen(τ )ϕ]≡I, (iii) ∀Σ ∈ Sig, ∀ϕ ∈ Sen(Σ), ∀M ∈ Mod(Σ): M [ϕ]≡I ⇔ M ϕ.

Clearly, satisfaction in I is well deﬁned; indeed, satisfaction is invariant under the correspondence established by the previous deﬁnition. This entails that the abstraction made by the quotient as in Deﬁnition 5.2 gives no loss of information about models, in the sense that elementary equivalence of models is invariant as well.

** Fact 5.3.**

Let I be a ps pre-institution, with I the corresponding abstract pre-institution according to Deﬁnition 5.2. Then for all models M1, M2 in I (as well as in I): M1 ≡I M2 ⇔ M1 ≡I M2.

As an example, we deﬁne the abstract, ﬁrst-order pre-institution, which is relevant to the theorem presented in the next section. The ﬁrst-order pre-institution is deﬁned according to Example 2.9, except that all ﬁrst-order signature morphisms are taken, not just the renamings.

** Example 5.4 (Abstract ﬁrst-order pre-institution).**

Let I = (SigI, SenI, ModI, I ) be the ﬁrst-order pre-institution, with all ﬁrst-order signature morphisms in SigI. The abstract ﬁrst-order pre-institution I = (SigI, SenI, ModI, I ) ˆ ˆ ˆ ˆ is deﬁned by SigI = SigI, ModI = ModI, and ˆ ˆ

(iii) ∀Σ ∈ SigI, ∀ϕ ∈ SenI (Σ), ∀M ∈ ModI (Σ): M [ϕ]≡I ⇔ M ϕ.

ˆ I I Further, for notational convenience, we extend the use of propositional connectives

**to the abstract sentences of I by the following convention:**

¬[ϕ]≡I = [¬ϕ]≡I, [ϕ]≡I ∧ [ψ]≡I = [ϕ ∧ ψ]≡I, [ϕ]≡I ∨ [ψ]≡I = [ϕ ∨ ψ]≡I.

As one should expect from Deﬁnition 2.12, turning sentences into abstract ones has the eﬀect of turning quasi-ﬁnitary pre-institution transformations into ﬁnitary ones.

** Fact 5.5.**

If T : I → I is a quasi-ﬁnitary pre-institution transformation, with I, I as in Deﬁnition 2.3, then T : I → I deﬁned by (i) ∀Σ ∈ Sig: ΣT = ΣT, (ii) ∀Σ ∈ Sig, ∀E ∈ Pre(Σ): ET = {[ϕ]≡I | ϕ ∈ ET }, (iii) ∀Σ ∈ Sig, ∀M ∈ Mod(Σ): MT = MT is a ﬁnitary pre-institution transformation.

The identiﬁcation of sentences up to logical equivalence has some technical convenience, which will surface in the proof of the theorem presented in the next section. In the formulation of that theorem, yet another property of pre-institution transformations is needed, which mirrors the notion of adequacy, but applied to model expansions rather than to models.

Definition 5.6 (Expansion adequacy). Let T : I → I be a pre-institution

**transformation, with I, I as in Deﬁnition 2.3. T is expansion-adequate iﬀ ∀τ :**

**Σ1 → Σ2 ∈ Sig, ∀M1 ∈ Mod(Σ1 ), ∀M2 ∈ Mod (Σ2T ):**

M2 τT ∈ M1T ⇒ ∃M2 ∈ Mod(Σ2 ) : M2 τ = M1 ∧ M2 ∈ M2T.

In other words, T is expansion-adequate whenever every τT -expansion of a transform of any given model is a transform of a τ -expansion of that model, for all signature morphisms τ in the source pre-institution.

6. Equivalence with the abstract, ﬁrst-order pre-institution. We start with a couple of general deﬁnitions and propositions, relating to discernibility of models that are transforms of the same model, along a given pre-institution transformation.

Definition 6.1. Let T : I → I be a pre-institution transformation, with I, I as in Deﬁnition 2.3. T is ≡I -limited iﬀ ∀Σ ∈ Sig, ∀ϕ ∈ Sen(Σ), ∀M ∈ Mod(Σ), ∀M1, M2 ∈ MT : M1 ϕT ⇔ M2 ϕT.

Definition 6.2. Let T : I → I be a pre-institution transformation, with I, I

**as in Deﬁnition 2.3. T is ≡I -limited iﬀ ∀Σ ∈ Sig, ∀M ∈ Mod(Σ), ∀M1, M2 ∈ MT :**

M 1 ≡I M 2.

Of the two properties introduced above, the latter entails the former, whilst models that are transforms of the same model along a ≡I -limited transformation

## PRE-INSTITUTIONS

T : I → I may well be discernible by sentences of the target pre-institution— albeit not by translations of sentences of the source pre-institution.** Fact 6.3.**

If T : I → I is a ≡I -limited pre-institution transformation, then it is ≡I -limited.

P r o o f. Immediate.

Both of the following facts play a rˆle in the subsequent, main theorem.

o Proposition 6.4. If the pre-institution I is closed under negation, then every fully adequate transformation T : I → I is ≡I -limited.

P r o o f. By contradiction, assume that for some Σ-sentence ϕ and Σ-model M in I there exist M1 and M2, both in MT, such that M1 ϕT and not M2 ϕT. Then not MT ϕT, thus not M ϕ by the satisfaction invariant, that is M ¬ϕ, whence M1 ϕT ∪ (¬ϕ)T, whence by (¬ϕ)T ; therefore M1 full adequacy of T, ∃M1 : M1 ∈ M1T ∧ M1 {ϕ} ∪ {¬ϕ}, i.e. M1 ϕ and not M1 ϕ, which is absurd.

Proposition 6.5. Let T : I → I be a pre-institution transformation. If T is ≡I -limited, then M1T ∩ M2T = {} ⇒ M1 ≡I M2 holds for all models M1, M2 in I.

P r o o f. For all sentences ϕ and models M in I, Deﬁnition 6.1 and the satisfaction invariant entail that ∀M ∈ MT : M ϕ T ⇔ MT ϕT ⇔ M ϕ.

Thus M ∈ M1T ∩ M2T implies that for every sentence ϕ in I: M ϕT ⇔ M1 ϕ ⇔ M2 ϕ, i.e. M1 ≡I M2.

The idea for the following theorem comes from Lemma XII.2.3 of [6], which plays a signiﬁcant rˆle in the proof of the ﬁrst Lindstr¨m theorem as presented o o in [6]. The lemma says the following. Let LI be the ﬁrst-order logical system (in the sense of abstract model theory), and L a compact regular (8 ) logical system such that LI ≤ L. If M1 ≡LI M2 ⇒ M1 ≡L M2 holds for all ﬁrst-order models M1, M2, then L ≤ LI. Now, the following theorem gives a similar result in our abstract framework, but without asking any regularity condition. On the other hand, the theorem is not—properly speaking—a generalization of the recalled lemma, for only one reason: it only applies to abstract pre-institutions. However, as we argue at the end of this section, a slight variant of the theorem holds that is a proper generalization of the recalled lemma.

** Theorem 6.6 (Equivalence with the abstract ﬁrst-order pre-institution).**

Let I be the abstract ﬁrst-order pre-institution, with I=(SigI, SenI, ModI, I ) acˆ ˆ ˆ ˆ cording to Example 5.4, and L = (SigL, SenL, ModL, L ) an abstract pre-instituThis means that L is closed under propositional connectives, permits relativization, and allows elimination of function symbols and constants—see Deﬁnition XII.1.3 in [6] for further details.

84 A. SALIBRA AND G. SCOLLO

P r o o f. Immediate consequence of Lemma 6.6.16 and of the elementwise construction of ER.

** Lemma 6.6.**

18. ∀τ : Σ1 → Σ2 ∈ SigL, ∀E ∈ PreL (Σ2 ): τR ER = (τ E )R, with ER as in Lemma 6.6.17.

We proceed to complete the proof of the theorem, as follows.

ˆ R : L → I according to Deﬁnition 6.6.1, the mapping of models as in Deﬁnition 6.6.2(i) and the mapping of presentations as in Lemma 6.6.17, is a pre-institution transformation, since Lemma 6.6.9 ensures naturality of model transformation, Lemma 6.6.18 ensures naturality of presentation transformation, and Lemma 6.6.17 shows validity of the satisfaction invariant.

88 A. SALIBRA AND G. SCOLLO That R is an inverse of T follows from Proposition 3.5, Lemma 6.6.15, and the construction of the mapping of presentations as in Lemma 6.6.17.