Lindström’s theorem,
both syntax and semantics free
Daniel Găină∗1 and Tomasz Kowalski†2
1
Institute of Mathematics for Industry, Kyushu University, Japan
Department of Mathematics and Statistics, La Trobe University, Australia
2
Department of Logic, Institute of Philosophy, Jagiellonian University, Poland
2

Abstract
Lindström’s theorem characterises first-order logic in terms of its essential model theoretic
properties. One cannot gain expressive power extending first-order logic without losing atleast one of compactness or downward Löwenheim-Skolem property. We cast this result inan abstract framework of institution theory, which does not assume any internal structure
either for sentences or for models, so it is more general than the notion of abstract logic
usually used in proofs of Lindström’s theorem, indeed, it can be said that institutional model
theory is both syntax and semantics free. Our approach takes advantage of the methods ofinstitutional model theory to provide a structured proof of Lindström’s theorem at a level ofabstraction applicable to any logical system that is strong enough to describe its own conceptof isomorphism, and its own concept of elementary equivalence. We apply our results to somelogical systems formalised as institutions and widely used in computer science practice.

1

Introduction

Traditionally, abstract model theory is understood as abstracting from the internal
structure of sentences. As noted by Barwise in [2], one of its tasks is to determine
the relationship between gaining expressive power in extending first-order logic andlosing some of its important properties. A paramount result in this direction is Lindström’s theorem, which characterises first-order logic among its extensions by two
major properties: the downward Lowenheim-Skolem Property and compactness. In
any proper extension of first-order logic at least one of the two fails.
To make the notion of a proper extension general enough, one is forced to abstract(at least) from what the sentences are. But abstract model theory itself is not a single theory. There are a number of abstract frameworks that can serve the purpose,including the one originally proposed in [2]. Another framework, particularly attractive to the authors, is institution theory, initiated by Goguen and Burstall in [13].
∗ E-mail address: daniel@imi.kyushu-u.ac.jp† E-mail address: T.Kowalski@latrobe.edu.au

1

In institution theory one studies meta-theoretic properties of logical systems withoutcommitment to the internal structure of either sentences or models. Working in thisframework can be cumbersome, unintuitive, and heavily laden with non-standard notation, but for this price one gets structured, modular proofs applicable to a wide
variety of logical systems without need of adaptation. Since the hypotheses are kept
as general as possible and introduced only when they are needed, the results are notobstructed by the irrelevant details of concrete logical systems, and allows one toobserve and exploit the causality relations between logical properties.
Institutions. The theory of institutions arose as a reaction to the explosion of logics
used in computer science that took place about four decades ago. These systems
typically shared a number of properties, which however had to be proved for eachof them separately. Goguen and Burstall proposed in [13] an abstract frameworkin which results could be developed at a general level and specialized to particularsystems avoiding the need of repeating the same arguments each time the logicalcontext is updated or changed in any way. An institution is a meta-structure thatputs together syntax, semantics, and the satisfaction relation between them, without
specifying any particulars. Goguen and Burstall’s goal was achieved at least in thearea of formal specification, verification and development of software systems [31,14]. An institutional framework is at the core of the mathematical foundations ofalmost all algebraic specification approaches to these. Three examples are CASL [1],CafeOBJ [9], and CITP [11, 12]. Institution theory is also friendly to formalised
mathematics, perhaps because of its origins in computer science. The reader will
have ample opportunities to verify that by looking at our proofs.
Our contribution. The main contribution of the present work is that we prove
Lindström’s theorem in a way that is independent of any concrete syntactic structure(syntax free) and independent of any concrete semantics (semantics free). It canbe said that this completes Lindström’s own work, which was syntax free (abstract
logics), but not semantics free (usual first-order structures). It is also the first study ofLindström’s theorem in the framework of institutions, in the spirit of abstract model
theory as we see it. Here are a few direct consequences of our approach.
We achieve a modular, structured proof of the characterisation of first-order logics
in terms of compactness and downward Löwenheim-Skolem property at a very generallevel of abstraction, which clearly reveals implications between logical properties andavoids inessential technical assumptions such as the Relativisation and Elimination
properties of Ebbinghaus, Flum and Thomas [10], or the Relativisation and Quantifier
properties of Chang, Keisler [3]. The results apply directly to a wide range of logicalsystems used in mathematical logic and computer science.
In particular, our results apply to many-sorted first-order logic (with equality)
which, despite contrary appearances, is a non-trivial generalisation of the single-sorted
version of first-order logic. For example, interpolation property holds in single-sorted
first-order logic without any restrictions, but for the many-sorted case interpolation
only holds under additional assumptions. The assumptions may be mild, yet findinga most general criterion ensuring that interpolation property holds when formulated
in terms of pushouts, was put forward as an open problem by Tarlecki in [33]. The
solution (only one of the pushout morphisms needs to be injective on sorts) was
given in [23]. Another example is completeness, which is developed at an institutionindependent level, but it is applicable to many-sorted first-order logics under the2

assumption that the carrier sets of the models consist of non-empty sets [29, 22, 20].
The absence of this assumption creates challenges for proving completeness that haveno straightforward solutions. Therefore, it is worth mentioning that the institutionindependent version of Lindström’s Theorem developed in the present contribution isapplicable to many-sorted first-order logic in which models may interpret some sorts asempty sets. Also, the classical proof of Lindström’s Theorem is tailored to signatures
which consists only of relation symbols and constants. This is no loss of generality,
since functions can be simulated with relations and some additional axioms. While
this argument is valid for first-order logic, it fails when dealing only with algebraic
signatures, which is the case of the OBJ family of algebraic specification languages
such as CafeOBJ [9] or Maude [5]. In addition, the ordering relation among sorts, afeature of both CafeOBJ and Maude, increases the complexity level of many-sorted
first-order logic. Fortunately, the development of the results at the appropriated levelof abstraction and the modularization principles that guided our study allowed us tocover also the case of order-sorted algebra [15, 25] with minimal effort.
Compactness. The conditions necessary for the development of ultraproduct method
were made clear by Diaconescu [6] in an abstract framework provided by an institution
satisfying some assumptions easy to verify in concrete examples of logical systems.
Institution-independent compactness is obtained as an application of ultraproductmethod. In the process, it was demonstrated that category-based multi-signatureframework characteristic of institution theory leads to greater generality and structured proofs. Institution independent compactness is obtained as a consequence ofcompleteness in [29], using a generalization of Henkin’s method from classical model
theory, and [22], using model-theoretic forcing.
Downward Löwenheim-Skolem Theorem. A method for proving downwardLöwenheim-Skolem theorem within an arbitrary institution satisfying certain properties is based on forcing and it was developed in [16]. The results are applicableto logics in which the semantics is restricted to models with non-empty carrier sets
and the syntax is restricted to countable languages. These restrictions were overcomein [18], which employs a novel technique for proving a more refined version of thetheorem.
Fraı̈ssé-Hintikka Theorem. This result, stating that elementary equivalence canbe characterised in terms of finite Ehrenfeucht-Fraı̈ssé games, was generalized to an
institution independent setting by the present authors [21], using an argument notcalling on quantifier rank or normal forms of sentences. The first part of the present
article is largely a preparation for an application of this abstract version of Fraı̈sséHintikka Theorem to the abstract internal characterisation of elementary equivalence,
carried out in Section 4. This characterisation, in turn, is the key to a modular
approach to Lindström’s theorem.

2

Institutions

We recall the notion of an institution, originally from [13].
Definition 1 (Institution). An institution I = (SigI , SenI , ModI , |=I ) consists of:
1. A category SigI , whose objects are called signatures.
32. A functor SenI : SigI → Set, providing for each signature Σ a set whose elements are called (Σ-)sentences.
3. A functor ModI : SigI → Catop , providing for each signature Σ a category whose
objects are called (Σ-)models and whose arrows are called (Σ-)homomorphisms.
4. A family of relations |=I = {|=IΣ }Σ∈|SigI | , where |=IΣ ⊆ |ModI (Σ)| × SenI (Σ) is
called (Σ-)satisfaction for all signatures Σ ∈ |SigI |, such that the following
satisfaction condition holds:
A0 |=IΣ0 SenI (χ)(e) iff ModI (χ)(A0 ) |=IΣ e
for all χ : Σ → Σ0 ∈ SigI , A0 ∈ |ModI (Σ0 )| and e ∈ SenI (Σ).
Note that the notion of valuation does not exist in institutions. Instead, in institution theory all variables are treated as constants, and thus there are no open
formulas. Quantification has to be defined accordingly – we will go into some details
later, as the need arises.
In concrete examples, the category of signatures SigI provides the vocabularies over which the sentences are built and the morphisms in SigI , called signaturemorphisms, represent a change of notation. Signature morphisms act covariantly on
sentences, and contravariantly on models. More concretely, given a signature morphism χ : Σ → Σ0 the sentences over the signature Σ are mapped to the sentences
over the signature Σ0 by the function SenI (χ) : SenI (Σ) → SenI (Σ0 ). The Σ0 -models
are ‘reduced’ to the signature Σ by the functor ModI (χ) : ModI (Σ0 ) → ModI (Σ).
We denote the reduct functor ModI (χ) by  χ and the function SenI (χ) by χ. If
A = A0  χ we say that A is the χ-reduct of A0 , and A0 is a χ-expansion of A.
When there is no danger of confusion, we omit the superscript I from the notationsof the institution components: for example, SigI may be simply denoted by Sig. The
notation surrounding the satisfaction relation is standard. Namely, for all signatures
Σ, sets of Σ-sentences Γ and E, we have
1. For all Σ-models A, (A |= E) iff (A |= e for all e ∈ E);
2. Γ |= E iff for all Σ-models A, we have A |= Γ implies A |= E;
3. Γ |=| E iff Γ |= E and E |= Γ.
Assumption 1. Since institutional setting is very abstract, we will explicitly mention
an assumption that in another context would be completely trivial: isomorphic models
are elementarily equivalent.
We do not know of any concrete institutions that do not satisfy the assumption
above, but an artificial example may illustrate why the assumption is necessary at
the institutional level of abstraction. It may happen that the set of sentences is richenough to speak about non-structural properties of models: say, distinguish between
models whose elements are blue, and models whose elements are green. Sentences
are not assumed to have any particular internal structure, so we can add them byfiat. Since isomorphism only detects structural properties, blue and green models
may be isomorphic but not satify the same sentences. Admittedly the example ispathological, but the definition of an institution does not preclude it.
42.1

ExamplesWe give a few typical examples of institutions in algebraic specification literature. We
will give quite some details, especially in the first example, in order to illustrate a few
common features of institutions, which are absent in other logical systems.
Example 2 (First-order logic (FOL)). The first presentation of first-order logic as
an institution is due to Goguen and Burstall [13].
Signatures. Signatures are of the form (S, F, P ), where S is a set of sorts, F ={Far →s }(ar ,s)∈S ∗ ×S is a (S ∗ ×S-indexed ) set of operation symbols, and P = {Par }ar ∈S ∗is a (S ∗ -indexed ) set of relation symbols. If ar = ε then an element of Far →s iscalled a constant symbol. Generally, ar ranges over arities, which are understoodhere as strings of sorts, so an arity gives the number of arguments
together with theirUsorts. We overload the notation and let F and P also denote (ar ,s)∈S ∗ ×S Far →s andU
ar ∈S ∗ Par , respectively. Therefore, we may write σ ∈ Far →s or (σ : ar → s) ∈ F ;both have the same meaning, which is: σ is an operation symbol of type ar → s. A
first-order signature with no relation symbols is called algebraic signature.
A signature morphism χ : Σ → Σ0 , where Σ = (S, F, P ) and Σ0 = (S 0 , F 0 , P 0 ), isa triple χ = (χst , χop , χrl ) of maps:
1. χst : S → S 0 ,0∗
2. χop = {χopar →s : Far →s → Fχst (ar )→χst (s) | ar ∈ S , s ∈ S},
0∗
3. χrl = {χrlar : Par → Pχst (ar ) | ar ∈ S }.
rl
When there is no danger of confusion, we may let χ denote either of χst , χopar →s , χar .

Models. Given a signature Σ = (S, F, P ), a Σ-model is a triple
A = ({As }s∈S , {σ A }(ar ,s)∈S ∗ ×S,σ∈Far →s , {π A }ar ∈S ∗ ,π∈Par )interpreting each sort s as a set As , each operation symbol σ ∈ Far →s as a function
σ A : Aar → As (where Aar stands for As1 × . . . × Asn if ar = s1 . . . sn ), and eachrelation symbol π ∈ Par as a relation π A ⊆ Aar . Morphisms between models are theusual Σ-homomorphisms, i.e., S-sorted functions that preserve the structure. The
models over an algebraic signature are called algebras.
For any signature morphism χ : Σ → Σ0 , where Σ = (S, F, P ) and Σ0 = (S 0 , F 0 , P 0 ),the model functor Mod(χ) : Mod(Σ0 ) → Mod(Σ) is defined as follows:
1. The reduct A0  χ of a Σ0 -model A0 is a defined by (A0  χ )s = A0χ(s) for each sort00s ∈ S, and xA χ = χ(x)A , for each operation symbol x ∈ F or relation symbolx ∈ P . Note that, unlike the single-sorted case, the reduct functor modifies theuniverses of models. For the universe of A0  χ is {A0χ(s) }s∈S , which means thatthe sorts outside the image of S are discarded. Otherwise, the notion of reduct
is standard.
2. The reduct h0  χ of a homomorphism h0 is defined by (h0  χ )s = h0χ(s) for all
sorts s ∈ S.

5

One important example of Σ-model is the first-order Σ-structure of (ground) termsTΣ that interprets each relation as the empty set. Algebraists will recognise it as theabsolutely free algebra of terms.
Sentences. We fix a countably infinite set of variable names {xi | i ∈ ω}. A
first-order variable for a signature Σ = (S, F, P ) is a triple (xi , s, Σ), where xi is thename of the variable, and s ∈ S is the sort of the variable. The last component Σof (xi , s, Σ) ensures that the variable (xi , s, Σ) is different from any constant of thesignature Σ. The set of Σ-sentences is given by the following grammar:
e ::= t = t0 | π(t1 , . . . , tn ) | ¬e | ∧E | ∀X · e0
where (a) t = t0 is an equation with t, t0 ∈ TΣ,s and s ∈ S, (b) π(t1 , . . . , tn ) isa relational atom with π ∈ Ps1 ...sn , ti ∈ TΣ,si and si ∈ S for all i ∈ {1, . . . , n},(c) E is a finite set of Σ-sentences, (d) X is a finite set of variables for Σ, and(e) e0 is a Σ[X]-sentence, where Σ[X] = (S, F [X], P ) and F [X] is obtained by adding
the variables in X as constants to F . Let χ : Σ → Σ0 be a signature morphism.
The translation of a variable (xi , s, Σ) for Σ along χ is (xi , χ(s), Σ0 ). The function
SenFOL (χ) : SenFOL (Σ) → SenFOL (Σ0 ) translates sentences symbolwise.
Satisfaction relation. Satisfaction is the usual tarskian satisfaction based on thenatural interpretations of ground terms t as elements tA in models A. For example,
A
A |= t1 = t2 iff tA
1 = t2 .
When there is no danger of confusion, we identify a first-order variable only by
its name and sort. For example, we write (xi : s) instead of (xi , s, Σ) when it is clear
from the context that (xi : s) is a variable for Σ. In case of single-sorted signatures
Σ, the second component s of a variable (x : s) for Σ can be dropped as well. With
this convention, for any inclusion of signatures ι : Σ ,→ Σ0 the corresponding function
Sen(ι) : Sen(Σ) → Sen(Σ0 ) is also an inclusion.
Example 3 (Order-sorted algebra (OSA)). There are several non-equivalent axiomatizations of OSA in the literature including the ones proposed by Goguen and
Meseguer [15] and by Poigné [30]. The version we consider here originates in [25],and it enjoys better mathematical properties than the ones enumerated before. See[26] for a comparison.
Signatures. An order-sorted (algebraic) signature is a triple Σ = (S, ≤, F ) with(S, ≤) a poset and (S, F ) a many-sorted algebraic signature. The set S/≡≤ of connected components of (S, ≤) is the quotient of S under the equivalence relation ≡≤generated by ≤. The equivalence ≡≤ can be extended to strings of elements from S
in the usual way. We say that Σ is sensible if for any function symbols (σ : w →s), (σ : w0 → s0 ) ∈ F we have w ≡≤ w0 implies s ≡≤ s0 . Any term over a sensibleorder-sorted signature has a unique connected component. The notion of sensible signature is a minimal syntactic requirement to avoid excessive ambiguity [26]. A partial
ordering (S, ≤) is filtered if for all s1 , s2 ∈ S, there is some s ∈ S such that s1 ≤ s
and s2 ≤ s. A partial ordering (S, ≤) is locally filtered if every connected componentof it is filtered. An order-sorted signature Σ = (S, ≤, F ) is locally filtered if (S, ≤) islocally filtered. One can obtain locally filtered signatures by adding top elements toeach connected component. Hereafter, we assume that all order-sorted signatures are
sensible and locally filtered.
6For the sake of simplicity, we let [S] denote S/≡≤ , and [s] denote s/≡≤ forall sorts s ∈ S. For any connected components [s1 ], . . . , [sn ], [sn+1 ] ∈ [S], we let[σ] : [s1 ] . . . [sn ] → [sn+1 ] denote the set {σ : s01 . . . s0n → s0n+1 | s0i ∈ [si ] and 1 ≤i ≤ n + 1} of ‘subsort polymorphic’ operators with name σ for those components.
An order-sorted signature morphism χ : (S, ≤, F ) → (S 0 , ≤0 , F 0 ) is an algebraic signature morphism χ : (S, F ) → (S 0 , F 0 ) such that the function χ : (S, ≤) → (S 0 , ≤0 )is monotonic and χ maps the function symbols in each subsort polymorphic family[σ] : [s1 ] . . . [sn ] → [sn+1 ] to a subset of the set [χ(σ)] : [χ(s1 )] . . . [χ(sn )] → [χ(sn+1 )].
Models. Let Σ = (S, ≤, F ) be an order-sorted signature. An order-sorted algebra A
over Σ is an (S, F )-algebra such that• As ⊆ As0 if s ≤ s0 , and• (σ : w → s)A (a) = (σ : w0 → s0 )A (a) for all function symbols (σ : w → s) ∈ F
and (σ : w0 → s0 ) ∈ ([σ] : [w] → [s]) and any element a ∈ Aw ∩ Aw0 .
According to [25], sensibility ensures the existence of the initial order-sorted algebraof terms TΣ , which is defined as follows:• c ∈ TΣ,s for all constants c :→ s ∈ F ,• σ(t1 , . . . , tn ) ∈ TΣ,s for all (σ : s1 . . . sn → s) ∈ F , i ∈ {1, . . . , n} and ti ∈ TΣ,si ,• t ∈ TΣ,s for all (s0 ≤ s) ∈ (S, ≤) and t ∈ TΣ,s0 , and• for each (σ : s1 . . . , sn → s) ∈ F , the function σ TΣ : TΣ,s1 × · · · × TΣ,sn → TΣ,sis defined by σ TΣ (t1 , . . . , tn ) = σ(t1 , . . . , tn ) for all i ∈ {1, . . . , n} and ti ∈ TΣ,si .
The homomorphisms h : A → B over Σ are many-sorted algebraic homomorphisms
such that hs (a) = hs0 (a) for all sorts s, s0 ∈ S with [s] = [s0 ] and all elements a ∈ As ∩As0 . Every isomorphism is clearly bijective. However, unless the underlying signature
is locally filtered, it is easy to exhibit signatures where some bijective homomorphisms
fail to be isomorphisms [14, Example 10.2.17]. Local filtration is also used in theconstruction of quotient order-sorted algebras.
Sentences. The set of atomic sentences over a signature consists of equations t = t0 ,where the sorts of both t and t0 belong to the same connected component. The set of
all sentences over a signature is constructed from equations by iteration of Boolean
connectives and quantification.
Satisfaction relation. The satisfaction of equations is based on the natural interpretation of terms in order-sorted algebras. The satisfaction of all sentences is definedby induction on the structure of sentences as for first-order logic.
Example 4 (Higher-order logic with Henkin semantics (HNK)). Higher-order logic
with Henkin semantics has been introduced and studied in [4] and [24]. In this article
we consider a simplified version close to the “higher-order algebra” of [27] which does
not consider λ-abstraction.
→−
For any set S of sorts, let S be the set of S-types defined as the least set such that
→
−
→
−
→
−
S ⊆ S and s1 → s2 ∈ S when s1 , s2 ∈ S . A HNK-signature is a tuple (S, F ), where− . A signature
S is a set of sorts and F is a family of sets of constants F = {Fs }s∈→S
7

morphism χ : (S, F ) → (S 0 , F 0 ) consists of a function χst : S → S 0 and a family of
→
−
→
−
0
− where χtype : S → S 0
functions between operation symbols {χops : Fs → Fχtype (s) }s∈→S→−
is the natural extension of χst to S . For every signature (S, F ), a (S, F )-model interprets each (a) sort s ∈ S as a set, and (b) function symbol σ ∈ Fs as an element of As ,→−where for all types s1 , s2 ∈ S , As1 →s2 ⊆ [As1 → As2 ] = {f function | f : As1 → As2 }.
→−An (S, F )-model morphism h : A → B interprets each type s ∈ S as a function
hs : As → Bs such that h(σ A ) = σ B , for all function symbols σ ∈ Fs , and thefollowing diagram commutes
As1

f

hs1


Bs1

/ As2
hs2

hs1 →s2 (f )


/ Bs2

→
−
for all types s1 , s2 ∈ S and functions f ∈ As1 →s2 .
The set of terms TΣ over a signature Σ = (S, F ) is defined inductively: (a) σ ∈ TΣ,s→−for all types s ∈ S and all function symbols σ ∈ Fs , and (b) t1 t2 ∈ TΣ,s2 for all types→−
s1 → s2 ∈ S and all terms t1 ∈ TΣ,s1 →s2 and t2 ∈ TΣ,s1 . The set of atomic sentences
over Σ consists of all equations of the form t1 = t2 , where t1 and t2 are terms of
the same type. Full sentences are constructed from equations by iteration of Boolean
connectives and quantification over variables of any type.
The satisfaction of equations t1 = t2 is based on the natural interpretations of theAterms t1 and t2 as functions tA
1 and t2 in higher-order models A. As for first-orderAlogic, we have A |= t1 = t2 iff tA=
t.
1
2 The satisfaction of all sentences is defined byinduction on the structure of sentences as in the case of first-order logic.
Example 5 (HNK0 ). This institution is obtained from HNK by restricting the types
in a signature to types that have depths less than some cardinal number, finite or ω,
fixed for the signature.
Signatures. The signatures are of the form (S, F, κ), where (S, F ) is a higher-ordersignature and κ is a cardinal with 0 < κ ≤ ω such that all the depths of the types of→−− , where S κ
the function symbols in F are strictly less than κ, that is, F = {Fs }s∈→Sκis the set of all types of depth strictly less than κ.
The signature morphisms χ : (S, F, κ) → (S 0 , F 0 , κ0 ) consists of a higher-ordersignature morphism χ : (S, F ) → (S 0 , F 0 ) such that κ ≤ κ0 .
Models. The (S, F, κ)-models are (S, F )-models which interpret only the types in→−S κ . This means that a (S, F, κ)-model A interprets (a) each sort s ∈ S as a set As ,→−(b) each type s1 → s2 ∈ S κ as As1 →s2 ⊆ [As1 → As2 ], and (c) each function symbol→−σ ∈ Fs , where s ∈ S κ , as an element of As .
Sentences. The (S, F, κ)-sentences consists of all sentences in SenHNK (S, F ) formed
with terms of types that have the depth strictly less than κ.
Satisfaction relation. Satisfaction is the restriction of |=HNK to HNK0 sentences.
Notice that HNK0 is a generalisation of HNK, since working in an HNK signature(S, F ) is exactly the same as working in an HNK0 signature (S, F, ω).
8

Example 6 (Subinstitutions). Let I = (Sig, Sen, Mod, |=) be an institution and Sig0 ⊆Sig a subcategory of signature morphisms. We overload the notation and let• Sen : Sig0 → Set be the restriction of Sen : Sig → Set to Sig0 ,• Mod : Sig0 → Set be the restriction of Mod : Sig → Set to Sig0 , and• |= denote also {|=Σ }Σ∈|Sig0 | .
Then I 0 = (Sig0 , Sen, Mod, |=) is also an institution.
Example 7 (Institution of presentations). In any institution I = (Sig, Sen, Mod, |=),a presentation is a pair (Σ, E) consisting of a signature Σ ∈ |Sig| and a set of Σsentences E. A presentation morphism ϕ : (Σ, E) → (Σ0 , E 0 ) is a signature morphism
ϕ : Σ → Σ0 such that E 0 |=Σ0 ϕ(E). Note that presentation morphisms are closed
under composition. The institution of presentations over I, denoted by I pres is defined
as follows:• Sigpres is the category of presentations over I,• Senpres (Σ, E) = Sen(Σ),• Modpres (Σ, E) is the full subcategory of Mod(Σ) of models satisfying E, and• A |=pres(Σ,E) e iff A |=Σ e, for each (Σ, E)-model A and Σ-sentence e.
For the sake of simplicity, we drop the superscript pres from the following notations: Senpres , Modpres and |=pres . A presentation (Σ, E) is typically an axiomatisation of a theory, with E the set of axioms. We give three examples below.
Example 8 (Subsystems of second-order arithmetic). A concrete example of presentation in FOL is second-order arithmetic Z2 = (ΣZ2 , TZ2 ), where• ΣZ2 is the first-order signature with sorts Nat and Set, function symbols 0 :→Nat, s : Nat → Nat, + : Nat Nat → Nat and × : Nat Nat → Nat, andmembership relation ∈ : Nat Set. The number variables are usually denotedby lower case letters x, y, . . . , while set variables are usually denoted by upper
case letters A, B, . . . .
• The axioms TZ2 are the usual Peano axioms, together with– the induction axiom∀A : Set · 0 ∈ A ∧ ∀x : Nat · (x ∈ A ⇒ s x ∈ A) ⇒ ∀x : Nat · x ∈ A– universal closures of the comprehension scheme∃A : Set · ∀x : Nat · (x ∈ A ⇔ ρ[x])for any sentence ρ[x] over ΣZ2 [x]. One important requirement is that A
does not occur in ρ[x], since if A could occur in ρ[x], then the formulax 6∈ A would produce an inconsistent comprehension axiom ∃A : Set · ∀x :Nat · (x ∈ A ⇔ x 6∈ A).
9

Subsystems of Z2 are obtained by restricting the formula ρ[x] in certain ways. Thesesystems are central to reverse mathematics. A comprehensive handbook of reverse
mathematics is [32]. Clearly, any subsystem of Z2 is a presentation over FOL.
Example 9 (Relation Algebras). Another example of presentation in first-order logic
is RA = (ΣRA , TRA ), which consists of the axioms of relation algebras. The signatureΣRA has one sort, say Rel (not of relations, however, but of algebra elements), no
relation symbols, and the following function symbols:
1. Boolean operations: the constants 0 for bottom, 1 for top, the unary − for thecomplement, and the binary ◦ and + for lattice meet and join 1 , and
2. operations of monoids with involution: the constant id for the identity, the unary
˘ for converse (involution), and the binary ; for composition (multiplication).
Composition ; binds stronger than meet ◦ and join +.
The axioms TRA of relation algebras consist of
A1) axioms defining Boolean algebras,
A2) axioms defining monoids with involution,A3) ∀a, b, c · (a + b) ; c = a ; c + b ; cand∀a, b, c · a ; (b + c) = a ; b + a ; c,A4) ∀a, b · (a + b)˘ = a˘ + b˘, and the triangle laws:
A5) ∀a, b, c · a ; b ◦ c 6= 0 ⇔ a˘ ; c ◦ b 6= 0 ⇔ b ; c˘ ◦ a˘ 6= 0.
Example 10 (Representable Relation Algebras). Yet another example of presentationin first-order logic is given by the axioms of representable relation algebras. The
signature ΣRRA consists of (a) two sorts, Elt for elements, and Rel for relations.2(b) all the function symbols for Boolean algebras and monoids with involution from
Example 9, and (c) a ternary relation λ : Rel Elt Elt denoting relations between
elements. The axioms TRRA consist of (A1) — (A4) defined in Example 9, andR1) ∀x : Elt, y : Elt, a : Rel , b : Rel · λ(a + b, x, y) ⇔ λ(a, x, y) ∨ λ(b, x, y),R2) ∀x : Elt, y : Elt, a : Rel · λ(−a, x, y) ⇔ λ(1, x, y) ∧ ¬λ(a, x, y),R3) ∀x : Elt, y : Elt · λ(id, x, y) ⇔ x = y,R4) ∀x : Elt, y : Elt, a : Rel · λ(a˘, x, y) ⇔ λ(a, y, x),R5) ∀x : Elt, y : Elt, a : Rel , b : Rel · λ(a ; b, x, y) ⇔ ∃z : Elt · λ(a, x, z) ∧ λ(b, z, y),R6) ∀a : Rel · a 6= 0 ⇒ ∃x : Elt, y : Elt · λ(a, x, y).
A representable relation algebra is the reduct to the signature ΣRA of any ΣRRA -model
which satisfies TRRA .
1 We chose rather unusual symbols for lattice operations to avoid confusion with ∧ and ∨ asconjunction and disjunction.
2 Note that here Rel are real relations: the elements of Rel of Example 9 can be thought of asnames for elements of Rel of the present example, so the abstract relation algebras are represented
as concrete algebras of binary relations.

10Relation algebras of Example 9 are just an example of an equational theory infirst-order logic. Representable relation algebras are a little more involved. Any representable relation algebra is isomorphic to a Boolean subalgebra of P(E), where E
is an equivalence relation on some set U , with the non-Boolean operations intepretedby the natural operations on binary relations: composition, converse and identity.
Not all relation algebras are representable, that is, Mod(ΣRRA , TRRA )  ΣRA is a propersubcategory of Mod(ΣRA , TRA ). Monk [28] shows that there exists no finite axiomatisation of representable relation algebras over the signature ΣRA . By Example 10,
there exists a finite axiomatisation of representable relation algebras in an extended
signature with two sorts; it follows, in particular, that representable relation algebras
have a recursive equational axiomatisation. Incidentally, this also demonstrates thenaturalness of the many-sorted approach.

2.2Internal logic

The following institutional notions dealing with the semantics of Boolean connectives
and quantifiers were defined in [33].
Definition 11 (Internal logic). Given a signature Σ in an institution, a Σ-sentence
γ is a semantic
1. negation of a Σ-sentence e if for each Σ-model A,
A |= γ iff A 6|= e,
2. conjunction of a (finite) set of Σ-sentences E if for each Σ-model A,
A |= γ iff A |= e for all e ∈ E,
3. universal χ-quantification of a Σ0 -sentence e0 , where χ : Σ → Σ0 , if for eachΣ-model A,
A |= γ iff A0 |=Σ0 e0 for all χ-expansions A0 of A.
Distinguished negation is usually denoted by ¬ , distinguished conjunction by ∧ , anddistinguished universal χ-quantification by ∀χ · .
As we have already mentioned, quantifiers need a special treatment. Intuitively,
the sentence ∀x · e[x] should hold in A if and only if the open formula e[x] is satisfied by
A on all valuations v into A. This is equivalent to saying that for all expansions (A, a)of A, we have that (A, a) satisfies e[x/a]; and it is the way quantification is rendered ininstitutions. Namely, let χ : Σ → Σ[x] be a signature morphism that adds the variablex as a new constant to Σ. The sentence ∀x · e0 is an abbreviation of ∀χ · e0 and thethird clause in Definition 11 ensures that we consider all χ-expansions of A. Thus,
the classical notion of valuation is incorporated into expansions. Variables belong to
an extended language: one can think of them as names coming from some externalpool and used as needed to name special constants. Incidentally, this approach avoids
the usual caveats about accidental binding of free variables.
11

Sentence building operators (Boolean connectives and quantifiers, but possibly
also infinitary connectives, modalities and suchlike) are part of the metalanguage
and they are used to construct sentences which belong to the internal language ofindividual institutions using (an appropriate extension of) the universal semantics
presented above.
Here we will only consider classical finitary Boolean connectives and quantifiers.
We also use the classical definitions of ∨ , ∃χ · , etc. For example, ∃χ · e0 := ¬∀χ · ¬e0and > := ∧∅. For standard logical operators we adopt the following convention about
their binding strength: ¬ binds stronger than ∧, which binds stronger than ∨, whichbinds stronger than ⇒, which binds stronger than quantifiers; quantifiers ∃ and ∀have the same binding strength.
An institution I is said to be semantically closed under negation (conjunction,
universal quantification, etc.) if every sentence in I has a semantic negation (conjunction, universal quantification, etc.) according to Definition 11.

2.3

Compactness and downward Löwenheim-Skolem property

Here we recall two fundamental model theoretic results on which the proof of Lindström’s theorem rests.
Definition 12 (Compactness). An institution I = (Sig, Sen, Mod, |=) is compact if
for all signatures Σ ∈ |Sig| and all sets of Σ-sentences Γ we have Γ |=Σ γ iff Γf |=Σ γ
for some finite subset Γf ⊆ Γ.
Theorem 13. FOL, OSA and HNK0 are compact.
Institutional proof of compactness of FOL can be found, for example, in [7]. Same
abstract results are applicable to OSA too. For compactness of HNK0 one can easily
adapt the arguments used for HNK in [7].
The downward Löwenheim-Skolem (DLS) property of FOL is the property thateach satisfiable and countable set of sentences has a countable model.3 In orderto state this definition for an arbitrary institution I = (Sig, Sen, Mod, |=) , we willconsider a subfunctor Modc : Sig → Catop of the model functor Mod : Sig → Catop .
Definition 14 (Downward Löwenheim-Skolem property). Let I = (Sig, Sen, Mod, |=)be an institution equipped with a model subfunctor Modc : Sig → Catop of Mod. I has
the DLS property (via Modc ) if for all signatures Σ ∈ |Sig| and all satisfiable andcountable sets of Σ-sentences Γ, there exists a model A ∈ |Modc (Σ)| such that A |= Γ.
Technically, our definition is parameterised by the functor Modc . However, we
do not make it explicit, since whenever an institution I is given, the functor Modc
is implicitly fixed. In the examples of institutions introduced in Section 2.1, Modc
selects countable models among all models: to be precise, Modc is the model functor
which maps signatures to classes of models with countable carrier sets.
Theorem 15 (Downward Löwenheim-Skolem Theorem). FOL, OSA and HNK0 havethe DLS property.
3 In many-sorted setting, we say that a model is countable if the carrier set of each sort is countable.

12

An institutional proof for FOL is given in [18], which is applicable to OSA too.
For HNK0 one can again adapt the arguments used in [18] for HNK.
To compare the expressivity of two institutions that share the same model functor,
we extend the terminology used in [10] to institutional model theory.
Definition 16 (Expressivity). Consider two institutions I = (Sig, Sen, Mod, |=) andJ = (Sig, SenJ , Mod, |=J ) that share the category of signatures and the model functor.
• J is at least as strong as I, in symbols I . J , if for each signature Σ ∈ |Sig|
and any sentence ρ ∈ SenI (Σ) there exists a sentence eρ ∈ SenJ (Σ) such that
A |=I ρ iff A |=J eρ for all Σ-models A.
• J has the same expressive power as I, in symbols I ∼ J , iff I . J and J . I.
To lighten the notation a little, we adopt the following convention: assuming that
I . J as in Definition 16, for all Σ ∈ |Sig|, ρ ∈ SenI (Σ) and γ ∈ SenJ (Σ), we will
write ρ |= γ to mean eρ |=J γ. Now we are ready to define Lindström property.
Definition 17 (Lindström property). Let I = (Sig, Sen, Mod, |=) be an institution
equipped with a model subfunctor Modc : Sig → Catop of Mod such that(a) I is semantically closed under Boolean connectives,(b) I compact, and(c) I has the DLS property of Definition 14.
I has the Lindström property if for all institutions J = (Sig, SenJ , Mod, |=J ) suchthat I . J and J has the properties (a)–(c), we have I ∼ J .
The following lemma will be useful later on to prove our results.
Lemma 18. Let I = (Sig, Sen, Mod, |=) and J = (Sig, SenJ , Mod, |=J ) be two institutions such that I . J and J is compact. For all Σ ∈ |Sig|, T ⊆ SenI (Σ) andγ ∈ SenJ (Σ) such that T |= γ, there exists a finite set Tf ⊆ T such that Tf |= γ.

3Object-level description of isomorphic models

Here we give an object-level characterisation of isomorphic models, in disjoint languages. Intuitively, we want to be able to take two isomorphic models and constructtheir disjoint union in an extended signature that remembers which ingredients (sorts,functions, relations) come from which model.
Definition 19 (Isomorphism structure). An institution I = (Sig, Sen, Mod, |=) isequipped with an isomorphism structure if there exist• a subcategory of signature morphisms SigISO ⊆ Sig,
• a functor ISO : SigISO → Sig,
• two natural transformations iso1 , iso2 : 1SigISO ⇒ ISO,• a set of ISO(Σ)-sentences SΣ for each signature Σ ∈ |SigISO |,
13

ΣO 0

isoi (Σ0 )/ ISO(Σ0 )O

χΣ(ISO(Σ0 ), SΣ0 )O

ISO(χ)

isoi (Σ)/ ISO(Σ)

ISO(χ)(ISO(Σ), SΣ )Figure 1: Isomorphism
satisfying the following properties:
1. For all Σ ∈ |SigISO | and all Σ-models A and B the following are equivalent:(a) A and B are isomorphic,(b) there exists D ∈ |Mod(ISO(Σ), SΣ )| s.t. D  iso1 (Σ) = A and D  iso2 (Σ) = B.
2. For all χ : Σ → Σ0 ∈ SigISO ,(a) the diagram shown to the left in Figure 1 has the following property: forall Σ0 -models A and B, and all ISO(Σ)-models C such that C  iso1 (Σ) =A  χ and C  iso2 (Σ) = B  χ , there exists an ISO(Σ0 )-model D such thatD  iso1 (Σ0 ) = A, D  iso2 (Σ0 ) = B and D  ISO(χ) = C, and(b) the diagram shown to the right in Figure 1 is a presentation morphism.
In the examples that follow, SigISO is the broad subcategory of all signature morphisms injective on sorts, and the functor ISO maps each signature Σ to a signatureISO(Σ) over which there exists a set of sentences SΣ that describes at an object level
the relation of isomorphism between Σ-models.

3.1

Isomorphic first-order models

Of course, FOL is expressive enough to support an object-level description of isomorphic first-order models. We will show that FOL has an isomorphism structure as
described in Definition 19.
Definition 20 (Disjoint union of first-order signatures). For any first-order signature
Σ, the disjoint union Σ ] Σ is defined as follows:Let Σ1 and Σ2 be two copies of Σ obtained by adding a superscript to the symbols
in Σ; if x is a sort, function or relation symbol in Σ then x1 is a sort, function or
relation symbol in Σ1 and x2 is a sort, function or relation symbol in Σ2 .
Then Σ1 ∪ Σ2 = Σ ] Σ. There are many equivalent ways to define a disjoint unionof two signatures. Any of them can be used in the following developments.
Proposition 21 (Object-level characterisation of isomorphic first-order models).
FOL is equipped with the following isomorphism structure:• SigISO ⊆ SigFOL is the broad subcategory of all first-order signature morphisms
injective on sorts.
14• For each Σ = (S, F, P ), the signature ISO(Σ) is obtained from Σ1 ∪ Σ2 describedin Definition 20 by adding a new relation symbol hs : s1 s2 for each sort s ∈ S,
in symbols, ISO(Σ) := (S 1 ∪ S 2 , F 1 ∪ F 2 ∪ {hs : s1 s2 | for all s ∈ S}).
The morphism isoi : Σ → ISO(Σ) maps each symbol x from Σ to xi , for alli ∈ {1, 2}. The set SΣ , which says that h := {hs }s∈S is an isomorphism, consistsof the following sentences:
A1) h is an injective function: for all s ∈ S,(a) ∀x : s1 · ∃y : s2 · hs (x, y), and(b) ∀x1 : s1 , y1 : s2 , x2 : s1 , y2 : s2 · hs (x1 , y1 ) ∧ hs (x2 , y2 ) ⇒(x1 = x2 ⇔ y1 = y2 ).
A2) h is surjective: ∀y : s2 · ∃x : s1 · hs (x, y), for all s ∈ S.
A3) h preserves the structure:(a) for all (σ : s1 . . . sn → s) ∈ F ,Vn∀x1 : s11 , y1 : s21 , . . . , xn : s1n , yn : s2n · i=1 hsi (xi , yi ) ⇒hs (σ 1 (x1 , . . . , xn ), σ 2 (y1 , . . . , yn )).
(b) for all (π : s1 . . . sn ) ∈ P ,Vn∀x1 : s11 , y1 : s21 , . . . , xn : s1n , yn : s2n · i=1 hsi (xi , yi ) ⇒(π 1 (x1 , . . . , xn ) ⇔ π 2 (y1 , . . . , yn )).
• Let χ : Σ → Σ0 be a signature morphism injective on sorts, where Σ = (S, F, P )and Σ0 = (S 0 , F 0 , P 0 ). Then ISO(χ) : ISO(Σ) → ISO(Σ0 ) maps
– xi to χ(x)i , where x is any sort, function or relation symbol in Σ andi ∈ {1, 2},– hs to hχ(s) , for all sorts s ∈ S.
Proof. For each signature morphism χ : Σ → Σ0 ∈ SigISO and any i ∈ {1, 2}, we haveisoi (Σ0 )(χ(x)) = χ(x)i = ISO(χ)(xi ) = ISO(χ)(isoi (Σ)(x)) for all sorts, function or
relation symbols x in Σ. Therefore, the following diagram is commutative.
ΣO 0

isoi (Σ0 )χΣ/ ISO(Σ0 )O
ISO(χ)

isoi (Σ)/ ISO(Σ)

It follows that isoi : 1SigISO ⇒ ISO is a natural transformation, for all i ∈ {1, 2}.
1. It is straightforward to show that two first-order models A and B over the same
signature Σ are isomorphic iff there exists C ∈ |Mod(ISO(Σ), SΣ )| such thatC  iso1 (Σ) = A and C  iso2 (Σ) = B.
2. For all signature morphisms χ : Σ → Σ0 ∈ SigISO , since ISO(χ)(SΣ ) ⊆ SΣ0 ,ISO(χ) : (ISO(Σ), SΣ ) → (ISO(Σ0 ), SΣ0 ) is a presentation morphism.
Now, let A, B ∈ |Mod(Σ0 )| and C ∈ |Mod(ISO(Σ))| such that A  χ = C  iso1 (Σ)
and B  χ = C  iso2 (Σ) . Let D be the ISO(Σ0 )-structure defined as follows:15

(a) D interprets each symbol in (Σ0 )1 as A and each symbol in (Σ0 )2 as B.
(b) For all sorts s0 ∈ χ(S), D interprets hs0 as hsC , where s = χ−1 (s0 ).
Since χ is injective on sorts, hsD0 is well-defined for all sorts s0 ∈ χ(S).
(c) For all sorts s0 ∈ S 0 \ χ(S), hsD0 is the empty set.
By (a), we get D  iso1 (Σ0 ) = A and D  iso2 (Σ0 ) = B.
(i) Since A  χ = C  iso1 (Σ) , C interprets each symbol in Σ1 as A  χ .
(ii) Since B  χ = C  iso2 (Σ) , C interprets each symbol in Σ2 as B  χ .
D(iii) By (b), hsC = hχ(s)for all sorts s ∈ S.

By (i), (ii) and (iii), we get D  ISO(χ) = C.
The injectivity on sorts required for SigISO is necessary for satisfying the condition(2a) of Definition 19. Also, it is useful to specify hs as a relation rather than function. The reason is again the modularization of isomorphism structures expressed by
Definition 19 (2a).

3.2Isomorphic order-sorted algebras

We show that OSA is equipped with an isomorphism structure. We use superscripts
to define the disjoint union of order-sorted signatures.
Proposition 22 (Object-level characterisation of isomorphic order-sorted algebras).
OSA is equipped with the following isomorphic structure:
1. SigISO ⊆ SigOSA is the broad subcategory of all order-sorted signature morphisms
injective on sorts.
2. For each OSA signature Σ = (S, ≤, F ),ISO(Σ) :=(S 1 ∪ S 2 ∪ {Bool }, F 1 ∪ F 2 ∪ {true :→ Bool } ∪{hs : s1 s2 → Bool | s ∈ S} ).

The signature morphism isoi : Σ → ISO(Σ) maps each sort or function symbol x
from Σ to xi , where i ∈ {1, 2}. The set SΣ , which says that h := {hs }s∈S is an
isomorphism, consists of the following sentences:
A1) h is an injective function:(a) for all sorts s ∈ S,
∀x : s1 · ∃y : s2 · hs (x, y) = true.
(b) for all s1 , s2 ∈ S such that s1 ≡≤ s2 ,∀x1 : s11 , y1 : s21 , x2 : s12 , y2 : s22 · hs1 (x1 , y1 ) = true ∧ hs2 (x2 , y2 ) = true ⇒(x1 = x2 ⇔ y1 = y2 ).
A2) h is surjective: ∀y : s2 · ∃x : s1 · hs (x, y) = true, for all sorts s ∈ S.

16A3) h preserves the structure: for all (σ : s1 . . . sn → s) ∈ F ,Vn∀x1 : s11 , y1 : s21 , . . . , xn : s1n , yn : s2n · i=1 hsi (xi , yi ) = true ⇒(hs (σ 1 (x1 , . . . , xn ), σ 2 (y1 , . . . , yn )) = true.
Proposition 22 is a straightforward generalization of Proposition 21 to the ordersorted case.

3.3

Isomorphic higher-order models

Here we show that HNK0 is equipped with an isomorphism structure. The disjoint
union of higher-order signatures is defined as for first-order signatures, using superscripts.
Proposition 23 (Object-level characterisation of isomorphic higher-order models).
HNK0 is equipped with the following isomorphism structure:0• SigISO ⊆ SigHNK is the broad subcategory of all signature morphisms injective
on sorts.
• For each HNK0 signature Σ = (S, F, κ),ISO(Σ) :=(S 1 ∪ S 2 ∪ {Bool }, F 1 ∪ F 2 ∪ {true : Bool } ∪→−{hs : s1 → s2 → Bool | s ∈ S κ }, 2 + κ ).

The signature morphism isoi : Σ → ISO(Σ) maps each sort or function symbol− isx from Σ to xi , where i ∈ {1, 2}. The set SΣ , which says that h := {hs }s∈→Sκan isomorphism, consists of the following sentences:→−
A1) h is an injective function: for all types s ∈ S κ ,(a) ∀x : s1 · ∃y : s2 · hs x y = true, and(b) ∀x1 : s1 , x2 : s1 , y1 : s2 , y2 : s2 · hs x1 y1 = true ∧ hs x2 y2 = true ⇒(x1 = x2 ⇔ y1 = y2 ).
→−A2) h is surjective: ∀y : s2 · ∃x : s1 · hs x y = true, for all types s ∈ S κ .
A3) h preserves the structure:(a) for all σ : s ∈ F ,hs σ 1 σ 2 = true.
→−(b) for all types s1 → s2 ∈ S κ ,2
1
1∀f : s1 → s2 , g : s1 → s22 , x : s1 , y : s21 · hs1 →s2 f g = true ∧hs1 x y = true ⇒ hs2 (f x)(g y) = true.
• Let χ : Σ → Σ0 be a signature morphism, where Σ = (S, F, κ) and Σ0 = (S 0 , F 0 , κ0 ).
The signature morphism ISO(χ) : ISO(Σ) → ISO(Σ0 ) maps
– xi to χ(x)i , where x is any sort or function symbol in Σ and i ∈ {1, 2},→−– hs to hχ(s) , for all types s ∈ S κ , and– it is the identity on the rest of the symbols.
The proof of Proposition 23 is conceptually the same as the proof of Proposition 21.
17

ΣO 0

elei (Σ0 )/ ELE(Σ0 )O

χΣ

(ELE(Σ0 ), EΣ0 )O

ELE(χ)

elei (Σ)/ ELE(Σ)

ELE(χ)(ELE(Σ), EΣ )Figure 2: Elementary equivalence

4

Object-level description of elementary equivalence

Our next goal is to obtain an object-level characterisation of elementary equivalence.
In analogy to the previous section, we will define two crucial properties and then showthat three benchmark examples of logics, formalised as institutions, have them. To
this end we will apply the institution independent version of Fraı̈ssé-Hintikka Theorem
from [21]. This section is a main stepping stone in our proof of Lindström’s theorem.
Definition 24 (Elementary equivalence structure). An institution I of the form
(Sig, Sen, Mod, |=) is equipped with an elementary equivalence structure if there exist• two subcategories of signature morphisms SigFIN ⊆ SigELE ⊆ Sig,
• a functor ELE : SigELE → Sig,
• two natural transformations ele1 , ele2 : 1SigELE ⇒ ELE,
• a set of sentences EΣ over ELE(Σ), for each signature Σ ∈ |SigFIN |,satisfying the following properties:
1. For all Σ ∈ |SigFIN | and all Σ-models A and B the following are equivalent:(a) A and B are elementarily equivalent,(b) there exists C ∈ |Mod(ELE(Σ), EΣ )| s.t. C  ele1 (Σ) = A and C  ele2 (Σ) = B.
2. For all signature morphisms χ : Σ → Σ0 ∈ SigELE , the diagram shown to the left
in Figure 2 has the following property:
for all Σ0 -models A and B, and all ELE(Σ)-models C such that C  ele1 (Σ) = A  χ
and C  ele2 (Σ) = B  χ , there exists an ELE(Σ0 )-model D such that D  ele1 (Σ0 ) =A, D  ele2 (Σ0 ) = B and D  ELE(χ) = C.
3. For all signature morphisms χ : Σ → Σ0 ∈ SigFIN , the diagram shown to theright in Figure 2 is a presentation morphism.
In the examples of institutions considered here, SigELE is the broad subcategory of
all signature morphisms injective on sorts and SigFIN is the subcategory of signaturemorphisms injective on sorts whose objects consist of a finite number of symbols. Then
ELE maps each signature Σ to a signature ELE(Σ) such that if Σ is finite there exists
a set of sentences EΣ over ELE(Σ) which describes the relation of finite isomorphism
between Σ-models. By an application of Fraı̈ssé-Hintikka Theorem, EΣ describes
18

ELE(Σ0 )O

bf(Σ0 )

ELE(χ)

ELE(Σ)/ BF(Σ0 )
O
BF(χ)

bf(Σ)

/ BF(Σ)bf(Σ0 )

(ELE(Σ0 ), EΣ0 )O/ (BF(Σ0 ), BΣ0 )O

ELE(χ)BF(χ)(ELE(Σ), EΣ )bf(Σ)/ (BF(Σ), BΣ )Figure 3: Back-and-forth equivalenceelementary equivalence between Σ-models. The description involves counting thenumber of times partial isomorphisms can be extended, so ELE(Σ) will typically havea sort Nat of natural numbers.
We will also need a stronger structure describing back-and-forth equivalence. Elementary equivalence is too weak to force isomorphism, but two countable models are back-and-forth equivalent iff they are isomorphic. Definition 25 provides aninstitution-independent infrastructure that enables an object-level description of backand-forth equivalence.
Definition 25 (Back-and-forth equivalence structure). An institution I of the form
(Sig, Sen, Mod, |=) is equipped with a back-and-forth equivalence structure if it isequipped with an elementary equivalence structure and, in addition, there exist:• a model functor Modc : Sig → Catop , which is a subfunctor of Mod,• a functor BF : SigELE → Sig,
• a natural transformation bf : ELE ⇒ BF,• a countable set of BF(Σ)-sentences BΣ , for all signatures Σ ∈ |SigFIN |,satisfying the following properties:
1. For any signature Σ ∈ |SigFIN |,(a) for all models A ∈ |Mod(ELE(Σ), EΣ )| and all finite subsets T ⊆ BΣ there
exists a bf(Σ)-expansion B of A such that B |= T, and(b) for all A ∈ |Modc (BF(Σ), BΣ )| we have A  ele (Σ);bf(Σ) ∼= A  ele (Σ);bf(Σ) .
1

2

2. For all signature morphisms χ : Σ → Σ0 ∈ SigELE , the diagram shown to theleft in Figure 3 has the following property: for all ELE(Σ0 )-models A, and all
BF(Σ)-models B such that B  bf(Σ) = A  ELE(χ) , there exists a BF(Σ0 )-model Csuch that C  bf(Σ0 ) = A, C  BF(χ) = A.
3. For all signature morphisms χ : Σ → Σ0 ∈ SigFIN , the diagram shown to the rightin Figure 3 is a commutative square of presentation morphisms.
In our examples, the signature BF(Σ) is obtained from ELE(Σ) by adding a new
constant c of sort Nat. The set BΣ is obtained from EΣ by adding a countably infinite
set of sentences which collectively say that c is a nonstandard number, which has
19

an infinite number of predecessors. Note that (1a) above says that BΣ is finitely
satisfiable, so compactness (if it holds) will yield a BF(Σ)-model of BΣ . Since theelements of sort Nat count the number of times partial isomorphisms can be extended,in any model C of BΣ , a certain partial isomorphism between Σ-models living inside
C will be extendable infinitely many times, giving back-and-forth equivalence. Then(1b) says that for a countable C, these Σ-models inside C (i.e. reducts of C) will beisomorphic.

4.1

Elementarily equivalent first-order models

We are now ready to give an object level characterisation of elementarily equivalent
first-order models.
Definition 26 (Partial isomorphism). Let A and B be two first-order models overa signature Σ = (S, F, P ). A partial isomorphism p : A 9 B is an injective partial
many-sorted function {ps : As 9 Bs }s∈S that is
1. a homomorphism, in the following sense:(a) for all σ : s1 . . . sn → sn+1 ∈ F and a1 ∈ dom(p)s1 , . . . , an+1 ∈ dom(p)sn+1 ,σ A (a1 , . . . , an ) = an+1 iff σ B (ps1 (a1 ), . . . , psn (an )) = psn+1 (an+1 );(b) for all π : s1 . . . sn ∈ P and a1 ∈ dom(p)s1 , . . . , an ∈ dom(p)sn , we have
(a1 , . . . , an ) ∈ π A iff (ps1 (a1 ), . . . , psn (an )) ∈ π B ; and2. the domain of p includes the interpretation of all constants, which means that{cA | c :→ s ∈ F } ⊆ dom(p).
Our definition of partial isomorphism is slightly different from [10] since it requiresthat the interpretation of all constants to be included in the domain.
Example 27 (Unnested isomorphism). An unnested isomorphism is a partial isomorphism p : A 9 B such that dom(p) = {cA | c :→ s ∈ F }.
By Fraı̈ssé-Hintikka Theorem, elementary equivalence between two first-order models amounts to the existence of extensions of certain partial isomorphisms. We will
now define tools needed for an object-level description of these extensions in first-orderlogic. The definition of finitely isomorphic first-order models over single-sorted signatures, which can be found, for example, in [10], can be easily adapted to many-sorted
first-order models with possibly empty domains.
Definition 28 (Finitely isomorphic first-order models). Two first-order models A andB over the same signature Σ = (S, F, P ) are finitely isomorphic, in symbols, A ∼=f B,
if there exists a family F = {Fk }k∈ω of non-empty sets of partial isomorphisms from
A to B such that for all k ∈ ω and all p ∈ Fk+1 the following two properties hold:
1. (Forth property) For all s ∈ S and all a ∈ As there exists q ∈ Fk such thatdom(p) ∪ {a} ⊆ dom(q) and q(x) = p(x) for all x ∈ dom(p).
2. (Back property) For all s ∈ S and all b ∈ Bs , there exists q ∈ Fk such that
range(p) ∪ {b} ⊆ range(q) and q(x) = p(x) for all x ∈ dom(p).
20

Intuitively, the back and forth properties can be expressed as follows: a partial
isomorphism in Fk+1 can be extended k + 1 times; the corresponding extensions lie
in Fk , Fk−1 , . . . , F1 , and F0 , respectively. If {Fk }k∈ω has the the back and forthproperties, we write {Fk }k∈ω : A ∼=f B. Next, we recall Fraı̈ssé-Hintikka Theorem
in many-sorted first-order logic. See [21] for details, including the connection to
Ehrenfeucht-Fraı̈ssé games in an institutional setting.
Theorem 29 (Fraı̈ssé-Hintikka Theorem in FOL). Let A and B be two first-ordermodels over a signature Σ with a finite number of function and relation symbols.
Then the following are equivalent:
1. A and B are elementarily equivalent.
2. A and B are finitely isomorphic.
Based on Theorem 29, we give an object-level characterisation of elementary equivalence in first-order logic.
Proposition 30 (Object-level characterisation of elementarily equivalence in FOL).
FOL is equipped with the following elementary equivalence structure:• SigELE ⊆ SigFOL is the broad subcategory of all signature morphisms injective on
sorts.
• SigFIN ⊆ SigFOL is the subcategory of signature morphisms injective on sorts
whose objects are finite first-order signatures.
• For each Σ ∈ |SigFOL |, the signature ELE(Σ) is obtained from Σ1 ∪ Σ2 describedin Definition 20 by adding the following new symbols:– a sort Nat, together with a binary relation < : Nat Nat and a predecessor
function pre : Nat → Nat,– a sort Par for the names of partial functions, together with a binary relation
F : Nat Par for finitely extendable partial isomorphisms, and– a ternary relation symbol app s : Par s1 s2 for each sort s ∈ S, for graphsof partial functions.
In symbols, ELE(Σ) := ( S 1 ∪S 2 ∪{Nat, Par }, F 1 ∪F 2 ∪{pre : Nat → Nat}, P 1 ∪P 2 ∪ { < : Nat Nat, F : Nat Par } ∪ {app s : Par s1 s2 | s ∈ S}).
• For each finite first-order signature Σ, the set EΣ , which says that two first-ordermodels over Σ are finitely isomorphic, consists of the following sentences:
A1) p is a partial injective function: for each sort s ∈ S,
∀p : Par , x1 : s1 , x2 : s1 , y1 : s2 , y2 : s2 · app s (p, x1 , y1 ) ∧ app s (p, x2 , y2 ) ⇒(x1 = x2 ⇔ y1 = y2 ).
A2) p preserves and reflects functions: for each (σ : s1 . . . sn → sn+1 ) ∈ F ,
n+1
^
1
2
1
2
∀p : Par , x1 : s1 , y1 : s1 , . . . , xn+1 : sn+1 , yn+1 : sn+1 ·app si (p, xi , yi )i=1

⇒ (σ 1 (x1 , . . . , xn ) = xn+1 ⇔ σ 2 (y1 , . . . , yn ) = yn+1 ).
21A3) p preserves and reflects relations: for each (π : s1 . . . sn ∈ P ),
n
^
1
2
1
2
∀p : Par , x1 : s1 , y1 : s1 , . . . , xn : sn , yn : sn ·app si (p, xi , yi ) ⇒i=1(π 1 (x1 , . . . , xn ) ⇔ π 2 (y1 , . . . , yn )).
A4) dom(p) includes the interpretation of all constants: for each c :→ s ∈ F ,∀p : Par · app s (p, c1 , c2 ).
A5) < is irreflexive: ∀k : Nat · ¬(k < k).
< is transitive: ∀k1 : Nat, k2 : Nat, k3 : Nat · k1 < k2 ∧ k2 < k3 ⇒ k1 < k3 .
< is a totally defined: ∀k1 : Nat, k2 : Nat · k1 < k2 ∨ k1 = k2 ∨ k2 < k1 .
Every element except the first (if it exists) has a predecessor:∀k1 : Nat · (∃k2 : Nat · k2 < k1 ) ⇒ (pre k1 < k1 )∧¬∃k2 : Nat · (pre k1 < k2 ∧ k2 < k1 ).
Every element has a successor: ∀k1 : Nat · ∃k2 : N at · k1 = pre k2 .
A6) p has the back and forth properties:∀k : Nat, p : Par · forth(k, p) ∧ back(k, p), where– forth(k, p) is the formula ^(pre k < k) ∧ F(k, p) ⇒∀xs : s1 · ∃qs : Par , ys : s2 · (qs extends p)s∈S∧ app s (qs , xs , ys ) ∧ F(pre k, qs ),– back(k, p) is the formula ^(pre k < k) ∧ F(k, p) ⇒∀ys : s2 · ∃qs : Par , xs : s1 · (qs extends p)s∈S∧ app s (qs , xs , ys ) ∧ F(pre k, qs ),– g^extends f is the formula∀xs : s1 , ys : s2 · app s (f, xs , ys ) ⇒ app s (g, xs , ys ).
s∈SA7) For all natural numbers k, the set of partial isomorphisms that can beextended k times is not empty: ∀k : Nat · ∃p : Par · F(k, p).
• Let χ : Σ → Σ0 be a first-order signature morphism injective on sorts. The
signature morphism ELE(χ) : ELE(Σ) → ELE(Σ0 ) maps
– xi to χ(x)i , where x is any sort, function or relation symbol in Σ andi ∈ {1, 2},– app s : Par s1 s2 to app χ(s) : Par χ(s)1 χ(s)2 for all sorts s in Σ, and– it is the identity on the rest of the symbols.
Proof. Let Σ = (S, F, P ) be a first-order signature. Since S is finite, the sentenceat (A6) is well-defined. Since F and P are finite, by Fraı̈ssé-Hintikka Theorem,
finitely isomorphic relation yield to elementary equivalence. The set EΣ of first-ordersentences over ELE(Σ) defined above is finite, as a consequence of the finiteness of Σ.
1. Let A and B be two models over a finite signature Σ = (S, F, P ). We show that
A and B are elementarily equivalent iff there exists C ∈ |ModFOL (ELE(Σ), EΣ )|such that C  ele1 (Σ) = A and C  ele2 (Σ) = B.
22

“⇒” Assume that A and B are elementarily equivalent. By Theorem 29, we
have {Fk }k∈ω : A ∼=f B for some family {Fk }k∈ω of non-empty sets of partial
isomorphisms from A to B. Let C be the first-order model over ELE(Σ) whichinterprets(a) all symbols in Σ1 as A, all symbols in Σ2 as B,(b) the sort Nat as ω,(c) the sort Par as the set of all partial isomorphisms p : A 9 B,(d) app C
s := {(p, a, b) | p : A 9 B, a ∈ As , b ∈ Bs s.t. p(a) = b} for all s ∈ S,(e) FC := {(k, p) | k ∈ ω and p ∈ Fk }.
It is straightforward to check that C |= EΣ .
“⇐” Let C ∈ |ModFOL (ELE(Σ), EΣ )| such that C  ele1 (Σ) = A and C  ele2 (Σ) = B.
By (A5), (CNat , <C ) is a discrete linear ordering with no top element. Therefore,
there exists an infinite sequence
c0 <C c1 <C c2 <C . . .
such that pre C ck+1 = ck for all k ∈ ω. By (A1)–(A4), each cp ∈ CPar can be
regarded as a partial isomorphism from A to B in the following way: cp : A 9 B
such that cp (a) = b iff (cp , a, b) ∈ app C
s for all s ∈ S, a ∈ As and b ∈ Bs . For
all k ∈ ω, let Fk := {cp ∈ CPar | FC (ck , cp )}, which is not empty due to (A7).
By (A6), the family {Fk }k∈ω has the back and forth properties required by
Definition 28. Therefore, {Fk }k∈ω : A ∼=f B. By Theorem 29, A and B are
elementarily equivalent.
2. For any first-order signature morphism injective on sorts χ : Σ → Σ0 , we haveisoi (Σ0 )(χ(x)) = χ(x)i = ELE(χ)(xi ) = ELE(χ)(elei (Σ)(x)) for all sorts, function or relation symbols x from Σ. Therefore, the following diagram is commutative.
elei (Σ0 )/ ELE(Σ0 )
ΣO 0
O
χ

Σ

ELE(χ)

elei (Σ)/ ELE(Σ)

Let A, B ∈ |Mod(Σ0 )| and C ∈ |Mod(ELE(Σ))| such that A  χ = C  ele1 (Σ) andB  χ = C  ele2 (Σ) . Let D be the ELE(Σ0 )-structure, which interprets(a) each symbol in (Σ0 )1 as A and each symbol in (Σ0 )2 as B,(b) the sort Nat as CNat , the relation symbol < as <C , and the function symbol
pre as pre C ,(c) the sort Par as CPar , and the relation symbol F as FC ,0(d) the relation symbol app s0 as app C
χ−1 (s0 ) for all sorts s ∈ χ(S), and(e) the relation symbol app s0 as the empty set for all sorts s0 ∈ S 0 \ χ(S).

230Since χ is injective on sorts, app D
s0 is well-defined for all s ∈ χ(S).

It is easy to show that D  ele1 (Σ0 ) = A, D  ele2 (Σ0 ) = B and D  ELE(χ) = C.
Now we strengthen the elementary equivalence structure to a back-and-forth equivalence structure.
Definition 31 (Partially isomorphic first-order models). Two models A and B overthe same signature Σ = (S, F, P ) are partially isomorphic or back-and-forth equivalent if there exists a non-empty set F of partial isomorphisms from A to B such thatfor all partial isomorphism p ∈ F the following two properties hold:
1. (Forth property) For all s ∈ S and all a ∈ As there exists q ∈ F such thatdom(p) ∪ {a} ⊆ dom(q) and p(x) = q(x) for all x ∈ dom(p).
2. (Back property) For all s ∈ S and all b ∈ Bs there exists q ∈ F such that
range(p) ∪ {b} ⊆ range(q) and p(x) = q(x) for all x ∈ dom(p).
The back and forth properties from Definition 31 amount to the existence of apartial isomorphism which has an infinite number of extensions. The following lemmasays that back-and-forth equivalence can be turn into isomorphism provided that theuniverses of the underlying models are countable.
Lemma
32. U
Let A and B be two first-order models over the same signature Σ. If
U∼∼s∈S As ands∈S Bs are countable then A =p B iff A = B.
The proof of Lemma 32 is a straightforward generalization of [10, Lemma 1.5 (d)]to the many-sorted case. The result relies on the fact that the elements of both A and
B are countable. Without the countability assumption only the backward implication
holds.
Proposition 33. FOL is equipped with a back-and-forth equivalence structure, which
extends the elementary equivalence structure described in Proposition 30 as follows:• Modc : SigFOL → Catop is the subfunctor of ModFOL which maps each signatureΣ to the full subcategory of Σ-models with countable carrier sets.
• The signature BF(Σ) extends ELE(Σ) with a new constant c :→ Nat, and thesignature morphism bf(Σ) : ELE(Σ) ,→ BF(Σ) is an inclusion.
• For each finite first-order signature Σ, the set BΣ extends bf(Σ)(EΣ ) with acountably infinite set {pre n+1 c < pre n c | n ∈ ω}, which says that c denotes anonstandard number which has an infinite number of predecessors.
Proof. Let Σ = (S, F, P ) be a first-order signature.
• Let χ : Σ → Σ0 be a signature morphism injective on sorts. Let A be a ELE(Σ0 )model and B a BF(Σ)-model such that A  ELE(χ) = B  bf(Σ) . We define C as
the bf(Σ0 )-expansion of A, which interprets c as B, i.e. cC = cB . Obviously,C  bf(Σ0 ) = A and C  BF(χ) = B.

24

• Let A ∈ |ModFOL (ELE(Σ), EΣ )|, and let {pre n+1 c < pre n c | n < k} be a finite
subset of {pre n+1 c < pre n c | n ∈ ω}, where k ∈ ω. Since (ANat , <A ) has no
upper bound, there exists an element a ∈ ANat with at least k predecessors. Let
B be the bf(Σ)-expansion of A which interprets c as a. It is straightforward toshow that B |= {pre n+1 c < pre n c | n < k}.
• Assume that Σ is finite and let D ∈ |Modc (BF(Σ), BΣ )| be a countable model.
We define the models A = D  ele1 (Σ);BF(Σ) and B = D  ele2 (Σ);BF(Σ) . We showthat A ∼
= B:
1
2
3

4
5
6

4.2

D |= ∃p : Par · F(dc , p),
where dc is the interpretation of c into D
D |= F(dc , dp ) for some dp ∈ DPardp can be regarded as a partial isomorphism from A to B, that is, dp : A 9 B
such that dp (a) = b iff (dp , a, b) ∈ app Dsfor all s ∈ S, a ∈ As and b ∈ Bs
dp : A 9 B can be extended infinitely
many times
A and B are countableA∼=B

since D |= ∀k : Nat · ∃p : Par · F(k, p)
by the definition of satisfactionby EΣ described in Proposition 30

since D |= F(dc , dp ) and dc has an
infinite number of predecessors
since D is countableby Lemma 32 from 4 and 5

Elementarily equivalent order-sorted algebras

The definitions of partial isomorphism, and of finitely isomorphic and partially isomorphic models can be replicated for order-sorted algebras based on the definition oforder-sorted homomorphism. One can straightforwardly check that the institutionindependent version of Fraı̈ssé-Hintikka Theorem from [21] is applicable to OSA too.
Theorem 34 (Fraı̈ssé-Hintikka Theorem in OSA). Let A and B be two order-sorted
algebras over an order-sorted signature Σ with a finite number of function symbols.
Then the following are equivalent:
1. A and B are elementarily equivalent.
2. A and B are finitely isomorphic.
Proposition 35 (Object-level characterisation of elementary equivalence in OSA).
OSA is equipped with the following elementary equivalence structure:• SigELE is the subcategory of order-sorted signature morphisms injective on sorts.
• SigFIN is the subcategory of order-sorted signature morphisms injective on sorts
whose objects are finite order-sorted signatures.
• For each finite signature Σ = (S, ≤, F ),ELE(Σ) :=( S 1 ∪ S 2 ∪ {Bool , Nat, Par }, ≤1 ∪ ≤2 , F 1 ∪ F 2 ∪{true :→ Bool , pre : Nat → Nat, < : Nat Nat → Bool } ∪{app s : Par s1 s2 → Bool | s ∈ S} ∪ {F : Nat Par → Bool } ).

For each finite signature Σ = (S, ≤, F ), the set EΣ , which says that two ordersorted algebras are finitely isomorphic, consists of the following sentences:25A1) p is a partial injective function: for all sorts s1 , s2 ∈ S such that s1 ≡≤ s2 ,∀p : Par , x1 : s11 , y1 : s21 , x2 : s12 , y2 : s22 · (app s1 (p, x1 , y1 ) = true) ∧(app s2 (p, x2 , y2 ) = true) ⇒ (x1 = x2 ⇔ y1 = y2 ).
A2) p preserves and reflects functions: for each (σ : s1 . . . sn → sn+1 ) ∈ F ,
n+1
^
1
2
1
2
∀p : Par , x1 : s1 , y1 : s1 , . . . , xn+1 : sn+1 , yn+1 : sn+1 ·app si (p, xi , yi ) = truei=1

⇒ (σ 1 (x1 , . . . , xn ) = xn+1 ⇔ σ 2 (y1 , . . . , yn ) = yn+1 ).
A3) dom(p) includes the interpretation of all constants: for each (c :→ s) ∈ F ,∀p : Par · app s (p, c1 , c2 ) = true.
A4) < is irreflexive: ∀k : Nat · ¬(k < k = true).
< is transitive:∀k1 : Nat, k2 : Nat, k3 : Nat · (k1 < k2 = true) ∧ (k2 < k3 = true) ⇒(k1 < k3 = true).
< is totally defined:∀k1 : Nat, k2 : Nat · (k1 < k2 = true) ∨ (k1 = k2 ) ∨ (k2 < k1 = true).
Every element except the first (if it exists) has a predecessor:∀k1 : Nat · (∃k2 : Nat · k2 < k1 = true) ⇒ ((pre k1 ) < k1 = true) ∧¬∃k2 : Nat · ((pre k1 ) < k2 = true ∧ k2 < k1 = true).
Every element has a successor: ∀k1 : Nat · ∃k2 : Nat · (pre k2 = k1 ).
A5) p has the back and forth properties:∀k : Nat, p : Par · forth(k, p) ∧ back(k, p), where– forth(k, p) is the formula(pre^k) < k = true ∧ F(k, p) = true ⇒∀xs : s1 · ∃qs : Par , ys : s2 · (qs extends p) ∧s∈Sapp s (qs , xs , ys ) = true ∧ F((pre k), qs ) = true,– back(k, p) is the formula(pre^k) < k = true ∧ F(k, p) = true ⇒∀ys : s2 · ∃qs : Par , xs : s1 · (qs extends p) ∧s∈Sapp s (qs , xs , ys ) = true ∧ F((pre k), qs ) = true,– g^extends f is the formula∀xs : s1 , ys : s2 · app s (f, xs , ys ) = true ⇒ app s (g, xs , ys ) = true.
s∈SA6) For all natural numbers k, the set of partial isomorphisms that can beextended k times is not empty: ∀k : Nat · ∃p : Par · F(k, p) = true.
• For each order-sorted signature morphism χ : Σ → Σ0 , the signature morphism
ELE(χ) : ELE(Σ) → ELE(Σ0 ) maps
– xi to χ(x)i , where x is any sort or function symbol in Σ and i ∈ {1, 2},– (app s : Par s1 s2 → Bool ) to (app χ(s) : Par χ(s)1 χ(s)2 → Bool ) for all
sorts s in Σ, and26

– it is the identity on the rest of the symbols.
Since Σ is finite, S is finite and the sentence at (A5) is well-defined. By Theorem 34, finitely isomorphic relation yield to elementary equivalence provided that theunderlying signature has a finite number of function symbols. Proposition 35 is astraightforward generalization of Proposition 30 to order-sorted case.
Proposition 36. The elementary equivalence structure from Proposition 35 can beextended to a back-and-forth equivalence structure as follows:• Modc : SigOSA → Catop is the subfunctor of ModOSA , which maps each signature
to the category of order-sorted algebras with countable carrier sets.
• The signature BF(Σ) is obtained from ELE(Σ) by adding a new constant c :→ Nat,and bf(Σ) : ELE(Σ) ,→ BF(Σ) is an inclusion.
• For each finite signature Σ, the set BΣ extends bf(Σ)(EΣ ) with a countably
infinite set {(pre n+1 c) < (pre n c) = true | n ∈ ω}.
Proposition 36 is a straightforward generalization of Proposition 33 to the ordersorted case.

4.3

Elementarily equivalent higher-order models

The definitions of partial isomorphism, and of finitely isomorphic and partially isomorphic models can be straightforwardly replicated for HNK0 using types instead ofsorts. Fraı̈ssé-Hintikka Theorem holds in HNK0 too.
Theorem 37 (Fraı̈ssé-Hintikka Theorem in HNK0 ). Let A and B be two higher-ordermodels over a signature Σ with a finite number of function symbols. Then the following
are equivalent:
1. A and B are elementarily equivalent.
2. A and B are finitely isomorphic.
Theorem 37 allows us to give an object-level characterisation of elementarily equivalent higher-order models.
Proposition 38 (Object-level characterisation of elementary equivalence in HNK0 ).
HNK0 is equipped with the following elementary equivalence structure:0• SigELE ⊆ SigHNK is the subcategory of signature morphisms injective on sorts.
0• SigFIN ⊆ SigHNK is the subcategory of signature morphisms injective on sorts
whose objects are finite HNK0 signatures.
• For each finite signature Σ = (S, F, κ),ELE(Σ) := ( S 1 ∪ S 2 ∪ {Bool , Nat, Par }, F 1 ∪ F 2 ∪ {true : Bool } ∪{pre : Nat → Nat, <: Nat → Nat → Bool } ∪{app s : Par → s1 → s2 → Bool | s ∈ S} ∪{F : Nat → Par → Bool } ).
For each finite signature Σ = (S, F, κ), the set EΣ , which says that two higherorder models are finitely isomorphic, consists of the following sentences:27→−A1) p is a partial injective function: for each type s ∈ S κ ,∀p : Par , x1 : s1 , x2 : s1 , y1 : s2 , y2 : s2 · (app s p x1 y1 = true) ∧(app s p x2 y2 = true) ⇒ (x1 = x2 ⇔ y1 = y2 ).
→−A2) p is compatible with functions: for all types s1 → s2 ∈ S κ ,∀p : Par , f : s11 → s12 , g : s21 → s22 , x1 : s11 , y1 : s21 , x2 : s12 , y2 : s22 ·(app s1 →s2 p f g = true) ∧ (app s1 p x1 y1 = true) ∧(app s2 p x2 y2 = true) ⇒ (f x1 = x2 ⇔ g y1 = y2 ).
A3) dom(p) includes the interpretation of all functions symbols:∀p : Par · app s p σ 1 σ 2 = true, for all (σ : s) ∈ F .
A4) < is irreflexive: ∀k : Nat · ¬(< k k = true).
< is transitive:∀k1 : Nat, k2 : Nat, k3 : Nat · (< k1 k2 = true) ∧ (< k2 k3 = true)⇒ (< k1 k3 = true).
< is a totally defined:∀k1 : Nat, k2 : Nat · (< k1 k2 = true) ∨ (k1 = k2 ) ∨ (< k2 k1 = true).
Every element except the first (if it exists) has a predecessor:∀k1 : Nat · (∃k2 : Nat · < k2 k1 = true) ⇒ (< (pre k1 ) k1 = true) ∧¬∃k2 : Nat · (< (pre k1 ) k2 = true ∧ < k2 k1 = true).
Every element has a successor: ∀k1 : Nat · ∃k2 : Nat · (pre k2 = k1 ).
A5) p has the back and forth properties:∀k : Nat, p : Par · forth(k, p) ∧ back(k, p), where– forth(k, p) is the formula< (pre^ k) k = true ∧ F k p = true ⇒∀xs : s1 · ∃qs : Par , ys : s2 · (qs extends p) ∧→−s∈ S κ

app s qs xs ys = true ∧ F (pre k) qs = true,– back(k, p) is the formula< (pre^ k) k = true ∧ F k p = true ⇒∀ys : s2 · ∃qs : Par , xs : s1 · (qs extends p) ∧→−s∈ S κ

app s qs xs ys = true ∧ F (pre k) qs = true,– g extends
f is the formula^∀xs : s1 , ys : s2 · (app s f xs ys = true ⇒ app s g xs ys = true).
→−s∈ S κ

A6) For all natural numbers k, the set of partial isomorphisms that can beextended k times is not empty: ∀k : Nat · ∃p : Par · F k p = true.
• For each signature morphism χ : Σ → Σ0 in HNK0 , the signature morphism
ELE(χ) : ELE(Σ) → ELE(Σ0 ) maps
– xi to χ(x)i , where x is any sort or function symbol in Σ and i ∈ {1, 2},– (app s : Par → s1 → s2 → Bool ) to (app χ(s) : Par → χ(s)1 → χ(s)2 →Bool ) for all types s in Σ, and28

– it is the identity on the rest of the symbols.
→−
Since Σ is finite, S κ is finite and the sentence at (A5) is well-defined. By Theorem 37, finitely isomorphic relation yield to elementary equivalence provided that theunderlying signature has a finite number of function symbols. The proof of Proposition 38 is conceptually the same as the proof of Proposition 30.
Proposition 39. The elementary equivalence structure from Proposition 38 can beextended to a back-and-forth equivalence structure as follows:00• Modc : SigHNK → Catop is the subfunctor of ModHNK , which maps each HNK0
signature to the category of higher-order models with countable carrier sets.
• The signature BF(Σ) is obtained from ELE(Σ) by adding a new constant c : Nat,and bf(Σ) : ELE(Σ) ,→ BF(Σ) is an inclusion.
• For each finite HNK0 signature Σ, the set BΣ extends bf(Σ)(EΣ ) with a countably
infinite set {< (pre n+1 c)(pre n c) = true | n ∈ ω}.
The proof of Proposition 39 is conceptually the same as the proof of Proposition 33.

5

Lindström’s theorem

We prove an institution independent version of Lindström’s theorem, not relying on
any particular form of syntax or semantics. In this sense our proof is both syntax andsemantics free.
Theorem 40. Let I = (Sig, Sen, Mod, |=) and J = (Sig, SenJ , Mod, |=J ) be two
institutions such that I . J . In addition, we assume that I is semantically closed
under Boolean connectives, and J is compact. If A ≡I B implies A ≡J B for all
signatures Σ ∈ |Sig| and all Σ-models A and B, then I ∼ J .
Proof. The proof is performed in three steps:
S1) Assume that A |=J γ, where Σ ∈ |Sig|, A ∈ |Mod(Σ)| and γ ∈ SenJ (Σ). We
show that there exists e(A,γ) ∈ SenI (Σ) such that A |=I e(A,γ) and e(A,γ) |= γ:1

ThI (A) |= γ
1.1
1.2

assume B |= ThI (A)A ≡I B

1.3
1.4

A ≡J BB |=J γby the following proof steps

as I is semantically closed undernegations and ThI (A) is a complete
theorysince ≡I ⊆ ≡J
since A |=J γ

23E |= γ for some E ⊆ ThI (A) finite
VeA,γ |=| E for some e(A,γ) ∈ SenI (Σ)

4

ThI (A) |= e(A,γ) and e(A,γ) |= γby Lemma 18
since I is semantically closed under
conjunctions
from 2 and 329S2) |Mod(Σ, γ)| =S

D∈|Mod(Σ,γ)| |Mod(Σ, e(D,γ) )| for all signatures Σ and all sen-J

tences γ ∈ Sen (Σ):I(a) If A ∈ |Mod(Σ, γ)|S then A |= e(A,γ) , which means A ∈ |Mod(Σ, e(A,γ) )|,and we get A ∈ D∈|Mod(Σ,γ)| |Mod(Σ, e(D,γ) )|.
S(b) If A ∈ D∈|Mod(Σ,γ)| |Mod(Σ, e(D,γ) )| then A ∈ |Mod(Σ, e(D,γ) )| for someΣ-model D such that D |=J γ. We have A |=I e(D,γ) , and since e(D,γ) |= γ,
we get A |= γ, which means A ∈ |Mod(Σ, γ)|.

S3) For all Σ ∈ |Sig| and all γ ∈ SenJ (Σ),
Sn there exist n ∈ ω and D1 , . . . , Dn ∈|Mod(Σ, γ)| such that |Mod(Σ, γ)| = Si=1 |Mod(Σ, e(Di ,γ) )|.4 Suppose towardsna contradiction that |Mod(Σ, γ)| ) i=1 |Mod(Σ, e(Di ,γ) )| for all n ∈ ω and
D1 , . . . , Dn ∈ |Mod(Σ, γ)|. Then:
1

2
3
4
5
6

{γ} ∪ {¬e(D1 ,γ) , . . . , ¬e(Dn ,γ) } is satisfiable,
for all n ∈ ω and all D1 , . . . , Dn ∈ |Mod(Σ, γ)|{γ} ∪ {¬e(D,γ) | D ∈ |Mod(Σ, γ)|} is satisfiable
there exists a Σ-model A such that A |=J γ and
A |=I ¬e(D,γ) for all D ∈ |Mod(Σ, γ)|
A |=I e(B,γ) for some B ∈ |Mod(Σ, γ)|
A |=I ¬e(B,γ)
contradiction

since
Sn |Mod(Σ, γ)| )i=1 |Mod(Σ, e(Di ,γ) )|since I . J and J is compact
by the definition ofsatisfiability
by S2, since A |=J γfrom 3from 4 and 5Sn

It follows that |Mod(Σ, γ)| =(Di ,γ) )| for some D1 , . . . , Dn ∈Wn i=1 |Mod(Σ, eSn|Mod(Σ, γ)|.
Since
|Mod(Σ,
e
)|
=
(D
,γ)
i
i=1
i=1 |Mod(Σ, e(Di ,γ) )|, we haveWnthat γ |=| i=1 e(Di ,γ) .
The following result provides minimal conditions for the meaning of a sentence todepend on a finite number of symbols.
Theorem 41. Let I = (Sig, Sen, Mod, |=) and J = (Sig, SenJ , Mod, |=J ) be two
institutions such that I . J . Assume moreover that
1. I is equipped with (a) an isomorphism structure as described in Definition 19
such that |SigISO | = |Sig|, and (b) a back-and-forth equivalence structure as described in Definition 25 such that SigELE = SigISO and for all signatures Σ ∈ |Sig|
and all finite subsets T ⊆ SΣ there exists χ : Σ0 → Σ ∈ SigISO such that
Σ0 ∈ |SigFIN | and ISO(χ)(SΣ0 ) |= T;
2. J has the following properties: (a) semantic closure under Boolean connectives,(b) compactness, and (c) DLS property via Modc .5
For all signatures Σ ∈ |Sig| and all sentences γ ∈ SenJ (Σ) there exists a signatureΣ0 ∈ |SigFIN | and a signature morphism χ : Σ0 → Σ ∈ SigISO such that
if A  χ ≡I B  χ then (A |=J γ iff B |=J γ)
4 For example, if γ is not satisfiable then take n = 0, which means that γ |=| ⊥.
5 The parameter Mod is given by the back-and-forth equivalence BF.
c30

for all Σ-models A and B.
Proof. We perform the proof in two steps.
S1) Firstly, we prove that for all signatures Σ ∈ |Sig| and all sentences γ ∈ SenJ (Σ),
there exist Σ0 ∈ |SigFIN | and χ : Σ0 → Σ ∈ SigISO such that
if A  χ ∼= B  χ then (A |=J γ iff B |=J γ)
for all Σ-models A and B. Let Σ ∈ |Sig| and γ ∈ SenJ (Σ). Since J is semanticallyclosed under Boolean connectives, there exists an ISO(Σ)-sentence ρ semanticallyequivalent to iso1 (Σ)(γ) ⇔ iso2 (Σ)(γ). We show that SΣ |= ρ:1
2

let C be an ISO(Σ)-model such that C |=I SΣ
∼ B, where A = C  iso (Σ) and B = C  iso (Σ)
A=3

A |=J γ iff B |=J γ

by Assumption 1, since A and
B are isomorphic

4
5

C |=J iso1 (Σ)(γ) iff C |=J iso2 (Σ)(γ)
C |=J ρby the satisfaction condition

1

2

by Definition 19(1), since
C |=I SΣas ρ is semantically equivalent
to iso1 (Σ)(γ) ⇔ iso2 (Σ)(γ)

By Lemma 18, T |= ρ for some T ⊆ SΣ finite. By the properties of I, there exist
Σ0 ∈ |SigFIN | and χ : Σ0 → Σ ∈ SigISO such that ISO(χ)(SΣ0 ) |= T. It follows that
ISO(χ)(SΣ0 ) |= ρ. Let A and B be two Σ-models such that A  χ ∼= B  χ . Weshow that A |=J γ iff B |=J γ:
1since A  χ and B  χ are isomorphic

3

C  iso1 (Σ0 ) = A  χ and C  iso2 (Σ0 ) = B  χ
for some C ∈ |Mod(ISO(Σ0 ), SΣ0 )|let D be an ISO(χ)-expansion of C suchthat D  iso1 (Σ) = A and D  iso2 (Σ) = B
D |=J ρ4

D |=J iso1 (Σ)(γ) iff D |=J iso2 (Σ)(γ)

since ρ is semantically equivalent toiso1 (Σ)(γ) ⇔ iso2 (Σ)(γ)

5

A |=J γ iff B |=J γ

by the satisfaction condition, sinceD  iso1 (Σ) = A and D  iso2 (Σ) = B

2

ISO(Σ) oO

isoi (Σ)

elei (Σ)χ

ISO(χ)

ISO(Σ0 ) oΣOisoi (Σ0 )Σ0by Definition 19(2a)since D |=I ISO(χ)(SΣ0 ) andISO(χ)(SΣ0 ) |= ρ/ ELE(Σ)O

bf(Σ)

ELE(χ)

elei (Σ0 )/ ELE(Σ0 )/ BF(Σ)O
BF(χ)

bf(Σ0 )

/ BF(Σ0 )S2) Let Σ ∈ |Sig| and γ ∈ SenJ (Σ). By (S1), there exists χ : Σ0 → Σ ∈ SigISO with
Σ0 ∈ |SigFIN | such that the meaning of γ depends only on Σ0 . Suppose towards acontradiction that there exist some Σ-models A and B such that31

A  Σ0 ≡I B  Σ0 , A |=J γ and B |=J ¬γ(1)

We show that BF(χ)(T) ∪ {(ele1 (Σ); bf(Σ))(γ), (ele2 (Σ); bf(Σ))(¬γ)} is satisfiable, for any finite subset T ⊆ BΣ0 :
1
2

3
4
5
6

there exists C ∈ |Mod(ELE(Σ0 ), EΣ0 )| such thatA  χ = C  ele1 (Σ0 ) and B  χ = C  ele2 (Σ0 )there exists an ELE(χ)-expansion D of C suchthat D  ele1 (Σ) = A and D  ele2 (Σ) = B
D |=I ELE(χ)(EΣ0 ), D |=J ele1 (Σ)(γ) andD |=J ele2 (Σ)(¬γ)
M |=I T for some bf(Σ0 )-expansion M of C
there exists a BF(χ)-expansion N of M suchthat N  bf(Σ) = D
N |=I BF(χ)(T), N |=J (ele1 (Σ); bf(Σ))(γ)
and N |=J (ele2 (Σ); bf(Σ))(¬γ)

since A  χ ≡I B  χ
by Definition 24(2), sinceA  χ = C  ele1 (Σ0 ) andB  χ = C  ele2 (Σ0 )by the satisfaction condition, as
A |=J γ, B |=J ¬γ and C |=I EΣ0
by Definition 25(1a), since
C |=I EΣ0 and T ⊆ BΣ0 is finite
by Definition 25(2), sinceD  ELE(χ) = C and M  bf(Σ0 ) = C
by the satisfaction condition,
since N  BF(χ) |=I T,
N  bf(Σ) |=J ele1 (Σ)(γ),
N  bf(Σ) |=J ele2 (Σ)(¬γ)

We show that assumption (1) made above is false:1{(ele1 (Σ); bf(Σ))(γ), (ele2 (Σ); bf(Σ))(¬γ)} ∪BF(χ)(BΣ0 ) is satisfiable

since every finite subset issatisfiable, I . J and J iscompact

2

since I . J and J has the
DLS property

4
5

C |=J {(ele1 (Σ); bf(Σ))(γ), (ele2 (Σ); bf(Σ))(¬γ)}
and C |=I BF(χ)(BΣ0 ) for some C ∈ |Modc (BF(Σ))|
A0  χ ∼= B0  χ , where0
A = C  ele1 (Σ);bf(Σ) and B0 = C  ele2 (Σ);bf(Σ)
A0 |=J γ iff B0 |=J γ
A0 |=J γ and B0 |=J ¬γ

6contradiction

from 4 and 5

3

by Definition 25(1b), sinceC  BF(χ) |=I BΣ0by (S1)from 2, by the satisfaction
condition

Hence, (A |= γ iff B |= γ) whenever A  χ ≡I B  χ .
The first part of the proof shows, using the isomorphism structure, that there
exists a finite signature Σ0 such that γ cannot distinguish between the models A and
B if they are isomorphic over Σ0 . The second part of the proof shows, using the backand-forth equivalence structure, that isomorphism can be weakened to elementaryequivalence and γ still cannot distinguish between the models A and B. So, γ depends
only on the properties that can be expressed in a finite signature.
Lindström’s theorem is a direct consequence of Theorem 40 and Theorem 41.
Theorem 42 (Lindström’s theorem). Let I = (Sig, Sen, Mod, |=) be an institution
equipped with
1. an isomorphism structure such that |SigISO | = |Sig|,

32

2. a back-and-forth equivalence structure such that SigELE = SigISO and for all signatures Σ ∈ |Sig| and all finite subsets T ⊆ SΣ there exists a signature morphismχ : Σ0 → Σ ∈ SigISO such that Σ0 ∈ |SigFIN | and ISO(χ)(SΣ0 ) |= T.
If I is (a) semantically closed under Boolean connectives, (b) compact and (c) it has
the DLS property, then I has the Lindström property.
Proof. By Theorem 40, it suffices to prove that A ≡I B implies A ≡J B for all
signatures Σ, and all Σ-models A and B. Assume that A ≡I B. Let γ be an
arbitrary but fixed Σ-sentence in J . By Theorem 41, there exist Σ0 ∈ |SigFIN | andχ : Σ0 → Σ ∈ SigISO such that if A  χ ≡I B  χ then (A |=J γ iff B |=J γ). Since
A ≡I B, we have A  χ ≡I B  χ . It follows that A |=J γ iff B |=J γ. Since γ was
arbitrarily chosen, A ≡J B. Since Σ was arbitrarily chosen, I ∼ J . Hence, I has
the Lindström property.
Theorem 42 is applicable to many-sorted first-order logic, partial algebra andhigher-order logic with Henkin semantics as presented in Example 5.
Corollary 43. FOL, OSA and HNK0 have the Lindström property.
Proof. We prove the result only for FOL, as the other cases are similar.
By Theorem 15, FOL has the DLS property. By Theorem 13, FOL is compact.
Therefore, it makes sense to consider an extension of FOL that preserves these properties.
By Proposition 21, FOL is equipped with an isomorphism structure described in
Proposition 21 such that |SigISO | = |SigFOL |. By Proposition 33, FOL is equippedwith a back-and-forth equivalence structure obtained by extending the elementaryequivalence structure described in Proposition 30 such that SigISO = SigELE .
For all first-order signatures Σ and all finite subsets T ⊆ SΣ , there exists a finite
subsignature Σ0 ⊆ Σ which contains all symbols of sorts, functions and relations that
occur in T. Notice that T ⊆ ISO(χ)(SΣ0 ), where χ : Σ0 ,→ Σ is an inclusion. It follows
that ISO(χ)(SΣ0 ) |= T.
By Theorem 42, FOL has the Lindström property.

6

Local Lindström’s theorem

The framework of institutions is essentially a multi-signature environment. Signaturemorphisms are ubiquitous: apart from making the framework easily adaptable tovarious concrete instantiations, they are also crucial internally for quantification. In
the classical environment however, one typically works with a fixed theory in a finite
language. The next definition is geared to this kind of setup. For a single finite
signature Σ, we define a minimal institution wrapping Σ up in enough logic to enablestating and proving Lindström’s theorem for Σ, as it were, locally.
Definition 44. Consider an institution I = (Sig, Sen, Mod, |=) equipped with a backand-forth equivalence structure as described in Definition 25, and a set of sentences
T over a signature Σ ∈ |SigFIN |. Let I(Σ,T) = (Sig(Σ,T) , Senpres , Modpres , |=pres ) be therestriction of I pres to a subcategory Sig(Σ,T) as described in Example 6, where Sig(Σ,T)
is defined as follows:33

1. Its objects are (Σ, T), (ELE(Σ), ET) and (BF(Σ), BT), where(a) ET = ele1 (Σ)(T) ∪ ele2 (Σ)(T) and(b) BT = (ele1 (Σ); bf(Σ))(T) ∪ (ele2 (Σ); bf(Σ))(T).
2. Its arrows are the identities plus the following presentation morphisms:(a) elei (Σ) : (Σ, T) → (ELE(Σ), ET), for all i ∈ {1, 2}, and(b) bf(Σ) : (ELE(Σ), ET) → (BF(Σ), BT).
Theorem 45 (Local Lindström’s theorem). Let I = (Sig, Sen, Mod, |=) be an institution equipped with a back-and-forth equivalence structure as described in Definition 25.
Let (Σ, T) be a presentation such that Σ ∈ |SigFIN | and T is countable.
If I(Σ,T) is (a) semantically closed under Boolean connectives, (b) compact and(c) it has the DLS property, then for all institutions J such that I(Σ,T) . J
and J has the properties (a)–(c), we have that for each sentence in SenJ (Σ)
there exists a sentence in SenI (Σ) satisfied by the same class of models.
Proof. The proof follows the lines of the proof of Theorem 42. It relies on an analogueof Theorem 41, simplified by the assumption that the signature of γ is from SigFIN , so
the isomorphism property is not required. Moreover, the condition |SigELE | = |Sig(Σ,T) |is not required either, and indeed, in general it does not hold, as in our case |SigELE | =(Σ, T). We leave the details to the reader.
Corollary 46. Let (Σ, T) be a first-order presentation such that Σ consists of a finite
number of symbols. FOL(Σ,T) has the local Lindström property, that is:
For all institutions J such that FOL(Σ,T) . J and J is (a) semantically closed
under Boolean connectives, (b) compact, and (c) it has the DLS property, we
have that for each sentence in SenJ (Σ) there exists a first-order Σ-sentencesatisfied by the same class of models.
In particular, FOLRA , FOLRRA and FOLZ2 have the local Lindström property.
In order to define J , the language is extended not only over the signature Σ, butalso over the signatures ELE(Σ) and BF(Σ). This is a simplification because it suffices
to extend the language over three vocabularies and not the entire class. For example,
if one wants to extend the language of Representable Relation Algebra with the Kleene
operator then only three signatures need to be considered. It is problematic to givean extension for all first-order signatures because of the translation of sentences along
signature morphisms.

7

Conclusions

We proved Lindström’s theorem in the framework of institutions, which is both syntax
and semantics free. The result immediately applies to many-sorted first-order logic,
order-sorted algebra and a version of higher-order logic with Henkin semantics. It
is also applicable to other logical systems formalised as institutions such as partial
34

algebra [1], preorder algebra [9], membership algebra [25], and other combinationsof these logics, which underlie algebraic specification languages such as CafeOBJ [9],Maude [5], or CASL [1].
We believe that applications to these systems are especially valuable, as the systems lack the austerity of the single-sorted first-order setting, and technical details
make clear-cut applications of first-order results rather difficult. Expanding on thistheme, in future we plan to cast Lindström’s theorem in the framework of stratified
institutions [8, 19, 17] and apply the result to hybrid logics.

Funding
The work presented in this paper has been partially supported by Japan Society for
the Promotion of Science, grant number 20K03718.

References[1] E. Astesiano, M. Bidoit, H. Kirchner, B. Krieg-Brückner, P. D. Mosses, D. Sannella, and A. Tarlecki. CASL: the Common Algebraic Specification Language.
Theoretical Computer Science, 286(2):153–196, 2002.
[2] J. Barwise. Axioms for abstract model theory. Annals of Mathematical Logic,
7(2-3):221–265, 1974.
[3] C. C. Chang and H. J. Keisler. Model theory, Third Edition, volume 73 of Studies
in Logic and the Foundations of Mathematics. North-Holland, 1992.
[4] A. Church. A Formulation of the Simple Theory of Types. J. Symb. Log.,
5(2):56–68, 1940.
[5] M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martı́-Oliet, J. Meseguer, and C. L.
Talcott, editors. All About Maude - A High-Performance Logical Framework,
How to Specify, Program and Verify Systems in Rewriting Logic, volume 4350 of
Lecture Notes in Computer Science. Springer, 2007.
[6] R. Diaconescu. Institution-independent Ultraproducts. Fundamenta Informaticæ, 55(3-4):321–348, 2003.
[7] R. Diaconescu. Institution-independent Model Theory. Studies in Universal Logic.
Birkhäuser, Basel, 1 edition, 2008.
[8] R. Diaconescu. Implicit Kripke semantics and ultraproducts in stratified institutions. J. Log. Comput., 27(5):1577–1606, 2017.
[9] R. Diaconescu and K. Futatsugi. Logical foundations of CafeOBJ. TheoreticalComputer Science, 285(2):289–318, 2002.
[10] H. Ebbinghaus, J. Flum, and W. Thomas. Mathematical logic (2. ed.). Undergraduate Texts in Mathematics. Springer, 1994.

35

[11] D. Găină, I. Ţuţu, and A. Riesco. Specification and verification of invariant
properties of transition systems. In 25th Asia-Pacific Software Engineering Conference, APSEC 2018, Nara, Japan, December 4-7, 2018, pages 99–108. IEEE,
2018.
[12] D. Găină, M. Zhang, Y. Chiba, and Y. Arimoto. Constructor-based inductive theorem prover. In R. Heckel and S. Milius, editors, Algebra and Coalgebra in Computer Science - 5th International Conference, CALCO 2013, Warsaw, Poland,
September 3-6, 2013. Proceedings, volume 8089 of Lecture Notes in Computer
Science, pages 328–333. Springer, 2013.
[13] J. Goguen and R. Burstall. Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery,
39(1):95–146, January 1992.
[14] J. A. Goguen. Theorem proving and algebra. CoRR, abs/2101.02690, 2021.
[15] J. A. Goguen and J. Meseguer. Order-sorted algebra I: Equational deduction for
multiple inheritance, overloading, exceptions and partial operations. TheoreticalComputer Science, 105(2):217–273, 1992.
[16] D. Găină. Forcing, Downward Löwenheim-Skolem and Omitting Types Theorems, Institutionally. Logica Universalis, 8(3-4):469–498, 2014.
[17] D. Găină. Birkhoff style calculi for hybrid logics. Formal Aspects of Computing,29(5):805–832, 2017.
[18] D. Găină. Downward Löwenheim-Skolem Theorem and interpolation in logics
with constructors. Journal of Logic and Computation, 27(6):1717–1752, 2017.
[19] D. Găină. Foundations of logic programming in hybrid logics with user-defined
sharing. Theoretical Computer Science, 686:1–24, 2017.
[20] D. Găină. Forcing and Calculi for Hybrid Logics. Journal of the Association for
Computing Machinery, 67(4):1–55, 2020.
[21] D. Găină and T. Kowalski. Fraı̈ssé-Hintikka Theorem in institutions. Journal of
Logic and Computation, 30(7):1377–1399, 2020.
[22] D. Găină and M. Petria. Completeness by forcing. Journal of Logic and Computation, 20(6):1165–1186, 2010.
[23] D. Găină and A. Popescu. An Institution-Independent Proof of the Robinson
Consistency Theorem. Studia Logica, 85(1):41–73, 2007.
[24] L. Henkin. Completeness in the theory of types. J. Symb. Log., 15(2):81–91,
1950.
[25] J. Meseguer. Membership algebra as a logical framework for equational specification. In F. Parisi-Presicce, editor, WADT, volume 1376 of Lecture Notes in
Computer Science, pages 18–61. Springer, 1997.

36

[26] J. Meseguer. Order-sorted parameterization and induction. In J. Palsberg, editor,
Semantics and Algebraic Specification, Essays Dedicated to Peter D. Mosses on
the Occasion of His 60th Birthday, volume 5700 of Lecture Notes in Computer
Science, pages 43–80. Springer, 2009.
[27] B. Möller, A. Tarlecki, and M. Wirsing. Algebraic Specifications of Reachable
Higher-Order Algebras. In D. Sannella and A. Tarlecki, editors, ADT, volume
332 of Lecture Notes in Computer Science, pages 154–169. Springer, 1987.
[28] J. Monk. On representable relation algebras. Michigan Mathematics Journal,
11:207–210, 1964.
[29] M. Petria. An Institutional Version of Gödel’s Completeness Theorem. In
T. Mossakowski, U. Montanari, and M. Haveraaen, editors, Algebra and Coalgebra in Computer Science, Second International Conference, CALCO 2007,
Bergen, Norway, August 20-24, 2007, Proceedings, volume 4624 of Lecture Notes
in Computer Science, pages 409–424. Springer, 2007.
[30] A. Poigné. Parametrization for order-sorted algebraic specification. J. Comput.
Syst. Sci., 40(2):229–268, 1990.
[31] D. Sannella and A. Tarlecki. Foundations of Algebraic Specification and Formal Software Development. Monographs in Theoretical Computer Science. An
EATCS Series. Springer, 2012.
[32] S. G. Simpson. Subsystems of second order arithmetic. Perspectives in Logic.
Cambridge University Press, Cambridge; Association for Symbolic Logic, Poughkeepsie, NY, second edition, 2009.
[33] A. Tarlecki. Bits and pieces of the theory of institutions. In D. Pitt, S. Abramsky,
A. Poigné, and D. Rydeheard, editors, Proceedings of a Tutorial and Workshop
on Category Theory and Computer Programming, volume 240 of Lecture Notes
in Computer Science, pages 334–360. Springer, 1986.

37