«COMPACTNESS AND ¨ LOWENHEIM–SKOLEM PROPERTIES IN CATEGORIES OF PRE-INSTITUTIONS ANTONINO SALIBRA University of Pisa, Dip. Informatica Corso Italia ...»
ALGEBRAIC METHODS IN LOGIC AND IN COMPUTER SCIENCE
BANACH CENTER PUBLICATIONS, VOLUME 28
INSTITUTE OF MATHEMATICS
POLISH ACADEMY OF SCIENCES
IN CATEGORIES OF PRE-INSTITUTIONS
ANTONINO SALIBRAUniversity of Pisa, Dip. Informatica Corso Italia 40, I-56125 Pisa, Italy E-mail: SALIBRA@DI.UNIPI.IT
GIUSEPPE SCOLLOUniversity of Twente, Fac. Informatica P. O. Box 217, NL-7500AE Enschede, The Netherlands E-mail: SCOLLO@CS.UTWENTE.NL Abstract. The
model-theoretic concepts of compactness and L¨wenheim–Skolem o properties are investigated in the “softer” framework of pre-institutions . Two compactness results are presented in this paper: a more informative reformulation of the compactness theorem for pre-institution transformations, and a theorem on natural equivalences with an abstract form of the ﬁrst-order pre-institution. These results rely on notions of compact transformation, which are introduced as arrow-oriented generalizations of the classical, object-oriented notions of compactness. Furthermore, a notion of cardinal pre-institution is introduced, and a L¨wenheim– o Skolem preservation theorem for cardinal pre-institutions is presented.
1. Introduction. In  we introduced the notion of pre-institution as an abstract notion of logical system, together with a notion of pre-institution transformation, which enables the transfer of logical reasoning, model-theoretic results and computing tools from one pre-institution to another.
The original target of our investigation was the notion of institution, which was introduced in  as a vehicle for the application of abstract model theory 1991 Mathematics Subject Classiﬁcation: 03C95, 03B10, 18B99, 03G99, 68Q65.
This work was produced while the second author was on temporary leave at LIENS, DMI, ´ Ecole Normale Sup´rieure, 45 Rue d’Ulm, F-75230 Paris Cedex 05, France.
e The paper is in ﬁnal form and no version of it will be published elsewhere.
 68 A. SALIBRA AND G. SCOLLO to computer science. Motivation for the choice of that target was the experience gained in , relating to the translation of a number of logics into equational type logic [13, 12]. We detected a striking commonality over the diﬀerenttranslations, concerning representation of models, translation of sentences, and structure of completeness proofs. The search for a more general framework, where that commonality could be factored out, was just as natural. For such an aim, the category of institutions seemed to oﬀer the obvious framework to work with. Two facts, however, indicated that this choice was not entirely obvious.
In the ﬁrst place, the way in which the expressiveness results in  were obtained led us to observe that pointwise translation of sentences and models is not always easy to work with. More generally, we need to translate presentations (i.e. sets of sentences) to presentations, and to associate a class of models in the target logic with each model of the source logic. The notion of institution morphism proposed in  thus deserves generalization.
In the second place, we observed that not every feature of the institution concept had some rˆle to play in the trial applications of our interest. The softness o of the satisfaction condition, in particular, does not seem to have been weighed on suﬃciently accurate scales.
The putting together of the two facts that occurred to our observation motivated thus the introduction of the less restrictive, albeit structurally weaker notion of pre-institution, together with an easier-to-use notion of morphism, which we called pre-institution transformation.
Now, in this paper we investigate a few most relevant concepts of abstract model theory, viz. compactness and L¨wenheim–Skolem properties, in the even o “softer” pre-institutions framework. In particular, we study the inheritance of these properties along pre-institution transformations.
Concerning compactness, the result in  is reﬁned by introducing a notion of compact transformation, whereby the classical concept of compactness of a logical system, once formulated for the soft framework of pre-institutions, is, so to say, “stretched” along the transformation arrow, relating validity in the target to ﬁniteness in the source.
Moreover, we show the contravariant inheritance of a general form of the L¨wenheim–Skolem properties by “suitable” pre-institution transformations. To o this purpose, the notion of pre-institution with cardinal numbers, or cardinal preinstitution, is introduced, since L¨wenheim–Skolem properties make reference to o the cardinality of models (and of symbol sets as well, in the more general forms of those properties).
Both in the case of compactness and in that of L¨wenheim–Skolem properties, o inheritance is “contravariant” in the sense that, if T : I → I is a “suitable” preinstitution transformation and I has the property under consideration, then I has that property as well. The pre-institution transformation is to be “suitable” in the sense that it may have to fulﬁl certain requirements—such as (full) adequacy, ﬁnitarity, etc.—depending on the property under consideration. Essentially, thus,
A central place in the analysis developed in this paper is given to a result on the equivalence with an abstract form of the ﬁrst-order pre-institution, i.e. the pre-institution arising from ﬁrst-order logic. This result generalizes a key lemma in the proof of the ﬁrst Lindstr¨m theorem that is given in .
o The organization of the rest of this paper is as follows. First, for the sake of self-containedness, we recall from  the needed deﬁnitions and facts, in Sections 2 and 3 respectively, but with new arguments and motivations in Section 2, taking the target of the present work into account. In Section 4, notions of compact transformation are introduced, and the compactness theorem from  (recalled in Section 3), is then reﬁned to a more informative theorem, linking compactness of a transformation with compactness of its source and target pre-institutions.
In Section 5, two new concepts are introduced, viz. that of pre-institution with abstract sentences, or abstract pre-institution, and that of expansion-adequate transformation. These concepts, together with the results on compact transformations, play an essential rˆle in the statement and proof of a theorem on the o equivalence with the abstract, ﬁrst-order pre-institution—the main result presented in Section 6. The notion of cardinal pre-institution is then introduced in Section 7, leading to a general form of L¨wenheim–Skolem preservation theorem o for cardinal pre-institutions, as worked out in this section. Finally, connections with related work are discussed in Section 8, and Section 9 closes the paper with an outline of topics for further investigation.
2. Basic notions and notations. A preliminary word about foundations. In this paper we use the term “set” in a rather comprehensive meaning, that generally includes proper classes. Whenever a need arises to exclude proper classes, we talk of “small sets”. Set is thus actually a “metacategory” (1 ), according to .
Definition 2.1. A pre-institution is a 4-tuple I = (Sig, Sen, Mod, ), with:
(i) Sig a category, whose objects are called signatures, (ii) Sen : Sig → Set a functor, sending each signature Σ to the set Sen(Σ) of
Σ-sentences, and each signature morphism τ : Σ → Σ to the mapping Sen(τ ) :
Sen(Σ) → Sen(Σ ) that translates Σ-sentences to Σ -sentences, (iii) Mod : Sigop → Set a functor, sending each signature Σ to the set Mod(Σ) of Σ-models, and each signature morphism τ : Σ → Σ to the τ -reduction function Mod(τ ) : Mod(Σ ) → Mod(Σ), (iv) : |Sig|→ Rel a function (2 ), yielding a binary relation Σ ⊆ Mod(Σ)× Sen(Σ) for each signature Σ, viz. the satisfaction relation between Σ-models and Σ-sentences.
(iii) I preserves satisfaction, or that I has the ps property (or that I is ps, for short), iﬀ I is both rps and eps.
An institution  is thus a pre-institution that preserves satisfaction and where model sets and reduction have categorial structure, that is, an institution rather has a functor Mod : Sigop → Cat, sending each signature Σ to the category Mod(Σ) of Σ-models, and each signature morphism τ : Σ → Σ to the τ -reduction functor Mod(τ ) : Mod(Σ ) → Mod(Σ). It seems interesting to investigate which properties of institutions do actually depend on requirements (†) and/or (‡) of Deﬁnition 2.2, and/or on the categorial structure of model sets and reduction, and which do not, thus holding for pre-institutions as well.
According to the motivation proposed in , we are interested in general tools for lifting results from one pre-institution to another pre-institution. Pointwise translation of sentences and models is not always easy to use for this purpose.
For example, to recover and possibly further extend the results obtained in , we need to translate presentations to presentations, and to associate a set of models (in the target pre-institution) with each model of the source pre-institution. A suitable notion of pre-institution morphism serves this purpose, for which a few preliminaries are needed.
We recall that the powerset functor ℘ : Set → Set sends every set to the collection of its subsets (3 ), and every function f : S → S to the function yielding the f -image of each subset of S. The functor ℘+ is analogously deﬁned, except that the empty set is excluded from the collection ℘+ (S), for all sets S.
In every pre-institution I = (Sig, Sen, Mod, ) we thus deﬁne Pre = ℘ ◦ Sen :
Sig → Set as the corresponding functor that sends each signature Σ to the (3 ) ℘ lives in the elevator of “palais Grothendieck”, thus, lifting its argument up one ﬂoor.
PRE-INSTITUTIONSset Pre(Σ) of Σ-presentations, and each signature morphism τ : Σ → Σ to the mapping Pre(τ ) : Pre(Σ) → Pre(Σ ) that translates Σ-presentations to Σ presentations. For convenience, we often write I = (Sig, Pre, Mod, ) instead of the more customary notation introduced in Deﬁnition 2.1.
It may seem strange that presentation transformation is allowed not to respect the set-theoretic structure of presentations, that is, it need not to be constructed elementwise. Our design principle, in this paper as well as in its predecessor , is that requirements restrict generality, hence there must be suﬃcient evidence of their necessity to set them a priori rather than introducing them as properties a posteriori. As an instance of the classical “Ockham’s razor”, we have adopted the rule: leges non sunt multiplicanda præter necessitatem.
By our own rule we are thus compelled to argue the necessity of the requirements which form Deﬁnition 2.2. Now, requiring functoriality of the signature translation and naturality of the presentation and model transformations is an obvious feature of good structure design by category-theoretic principles. But Definition 2.3 states two further requirements, whose necessity is argued on intuitive grounds as follows.
The intuitive reason for the non-emptiness requirement on MoTΣ (M ) is that the existence of a pre-institution transformation is intended to entail the “representability” of every source model by some target model.
The reason for the requirement expressed by the satisfaction invariant is the soundness of consequence in the image of the transformation with respect to consequence in the source. This fact is apparent from Proposition 3.3(i), or, more precisely, from the fact that its (very simple, almost immediate) proof requires both directions of the double implication by which the satisfaction invariant is formulated.
The next deﬁnition introduces a notion of equivalence between models that reﬂects their indiscernibility by the logical means that is available “inside the pre-institution”, viz. the notion of elementary equivalence. The second part of the deﬁnition formalizes logical equivalence of sentences inside a pre-institution, viz. their indiscernibility by validity in models, which fact justiﬁes the overloading of the equivalence symbol.
Definition 2.4. Let I = (Sig, Pre, Mod, ) be a pre-institution, and Σ a signature in Sig.
1. Any two Σ-models M1, M2 are I-equivalent, written M1 ≡I M2, iﬀ for
every Σ-presentation E:
E ⇔ M2 M1 E.
2. Any two Σ-sentences ϕ, ψ are I-equivalent, written ϕ ≡I ψ, iﬀ for every
Σ-model M :
ϕ⇔M M ψ.
Additional requirements characterize certain classes of pre-institution transformations, and will prove very useful in the rest of this paper.
As we shall see in the next section, adequacy ensures completeness of the transformation with respect to consequence. Full adequacy is just a stronger form of adequacy (clearly, every fully adequate transformation is adequate as well), which proves connected to compactness of pre-institutions, as mentioned in Section 3 and further analysed in Section 4. A useful suﬃcient criterion for full adequacy is as follows.
Let T : I → I be a pre-institution transformation, with I, I as
in Deﬁnition 2.3. If T is adequate and meets the following condition:
∀Σ ∈ Sig, ∀M1, M2 ∈ Mod(Σ) : (M ∈ M1T ∧ M ∈ M2T ) ⇒ M1T = M2T, then T is fully adequate.
A ﬁrst use of our notions of adequacy is found in the following deﬁnition.
Definition 2.7. Let I and I be two pre-institutions.