Fraı̈ssé-Hintikka Theorem in institutions
Daniel Găină∗1 and Tomasz Kowalski†2
1

2

Institute of Mathematics for Industry, Kyushu University, Japan
Department of Mathematics and Statistics, La Trobe University, Australia

Abstract
We generalize the characterization of elementary equivalence by Ehrenfeucht-Fraı̈ssé games
to arbitrary institutions whose sentences are finitary. These include many-sorted first-orderlogic, higher-order logic with types, as well as a number of other logics arising in connection
to specification languages. The gain for the classical case is that the characterization isproved directly for all signatures, including infinite ones.

1

Introduction

A classical model theorist or logician is dimly aware that in applications it is convenient to have sorts (say, the boolean sort, lists, and the natural numbers), possibly
some higher-order ingredients (say, a collection of subsets of N), and perhaps partial
functions (square root, for example), but he dismisses these things as trivial nuisances, which, with some effort and perhaps a little cleverness, can be simulated in
the classical one sorted first-order setting. An applied logician replies that althoughsimulations are fine in principle, they are not always reasonable in practice, and ‘practice’ includes the ordinary work of a mathematician. Reverse mathematics is a casein point. Roughly, one considers there extensions of Peano Arithmetic obtained byadding some collections of subsets of N. The resulting structures, although called
second-order arithmetics, are in fact two-sorted first-order. Example 8 below gives
more details about these two-sorted structures.
The two authors represent these two parties (no prizes for guessing whom which),so this article is also an exercise in reconciliation. One result of this is that the reader
familiar with institution theory will find parts of what we say trivial, and the reader
familiar with classical model theory will also find parts of what we say trivial. We
hope these will not be the same parts.
Institutions. Institution theory arose in response to practical considerations; specifically, as a reaction to a proliferation of algebraic specification languages which did
essentially the same in different ways, so the same theorems had to be proved for∗ E-mail address: daniel@imi.kyushu-u.ac.jp† E-mail address: T.Kowalski@latrobe.edu.au1each, over and over. Tired of this, Goguen and Burstall in [12] introduced institutions, an abstract framework for reasoning about properties of logical systems from ameta-perspective. Isolating the essence of a logical system in the abstract satisfaction
relation, whose essence in turn is that truth is invariant under change of notation,and leaving the details open, institutions achieve an appropriate level of generality
for the development of abstract model theory, independent of the specific nature of
the underlying logic.
Intuitively, an institution can be likened to a high-level programming language: itcomes with a syntax, a semantics, and a satisfaction relation linking the two. As wewill see later in detail, first-order logic can be presented as an institution: its syntax
is what you expect, its semantics is the class of all models in the usual sense, andthe satisfaction relation is Tarski’s satisfiability. Many other logical systems can beso presented: partial algebras, higher-order logics, intuitionistic logic, modal logics,
many-valued logics, in fact any logical framework with a satisfaction relation canbe presented as an institution. Institutions may be quite unlike one another, butthey share some theorems: these that can be proved independently of any assumptions specific to a particular institution. Proving classical theorems in an institution
independent way has been a theme in institution theory from its early days, starting from meta-level theorems about algebraic specification languages. A large bodyof institution independent proofs of classical theorems exists: interpolation and related properties of Beth definability and Robinson joint consistency were studied
in [6, 27, 21, 13, 16], ultraproducts and saturated models in [5, 11], model theoretic forcing in [19, 14, 17], elementary chains in [20], quasivarieties and free models
in [30, 32, 7, 18], and proof theory in [8, 4, 19, 15]. For a monograph on institution
theory, we refer the reader to [9].
However, a classical result in model theory stating that elementary equivalence
can be characterized in terms of finite Ehrenfeucht-Fraı̈ssé games has so far not been
given an institution independent treatment. The present article fills this gap.
Although the above characterization is commonly called Fraı̈ssé-Hintikka Theorem, we will follow [26] in using the name for something more technical (Theorem 34),of which the game characterization is a corollary (Corollary 35). Since finite games arequite intuitive and easy to describe, Fraı̈ssé-Hintikka Theorem gives a better handle
on elementary equivalence than Keisler-Shelah Theorem characterizing elementaryequivalence via ultrapowers. A typical example given to illustrate this point is thefollowing. Let N ⊕ Z be the linear sum of N and Z as ordered sets: a copy of Z
on top of a copy of N. It is a nontrivial exercise to find an ultrapower of N ⊕ Z
isomorphic to an ultrapower of N, whereas the fact that the ‘existential’ player has
a winning strategy in all finite games is just staring one in the face: for a fixed k,choose the response high enough in N (2k+1 should suffice) so that you could survive
k further steps. Numerous celebrated results were proved using Ehrenfeucht-Fraı̈ssé
games: see, e.g., [33] for a quick introduction and survey of three examples importantin theoretical computer science.
One of the things required for an institution independent proof of Fraı̈ssé-Hintikka
Theorem is a description of Ehrenfeucht-Fraı̈ssé games at an abstract level. We give a
suitable description, revealing in the process that a naive generalization of the games
for elementary equivalence from single first-order logic to many-sorted first-order logic
and higher-order logic setting runs into problems related to infinite signatures.

2Notational conventions. The notation we use is standard in institution theory,
but since institution theory is nonstandard in logic, we give a few warnings below.
Generally, institution theory assumes categorical background, so if any piece of notation seems unclear, an interpretation from category theory (if there is one) will beright. Thus, |C| stands for the set of objects of C; the collection of all signatures andsignature morphisms, in particular, forms a category. Composition of morphisms andfunctors is denoted using the symbol ‘;’ and is considered in diagrammatic order. The
word ‘arity’ in institution theory is used to denote a finite string over the alphabet
whose letters are the sorts. So, against etymology, arities formally are not numbers.
However, the set of finite strings over a set S is denoted by the standard S ∗ . We will
still say e.g., ‘a ternary relation’ informally with the usual meaning.

2

Preliminaries

We said that institutions focus on the satisfaction relation, leaving other details open.
We did not say details of what. We will do it now. Crucial to the concept of institution
is a notion of signature, which is more or less what it is in model theory, but whereas
in model theory signatures are grudgingly acknowledged and ignored as much as they
can be, in institution theory they come to the forefront.
Definition 1 (Institution). An institution I = (SigI , SenI , ModI , |=I ) consists of:
1. A category SigI , whose objects are called signatures.
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Σ ⊆ |Mod(Σ)|×SenI (Σ) is called(Σ-)satisfaction for all signatures Σ ∈ |Sig|, such that the following satisfaction
condition holds:
A0 |=Σ0 Sen(ϕ)(e) iff Mod(ϕ)(A0 ) |=Σ e
for all ϕ : Σ → Σ0 ∈ SigI , A0 ∈ |Mod(Σ0 )| and e ∈ Sen(Σ).
Note that the notion of valuation is conspicuously absent from institutions. Indeed,
in institution theory all variables are (treated as) constants, and thus there are no
open formulas. Quantification has to be defined accordingly, and it takes some work.
See Section 3.2.
In concrete examples, the category of signatures Sig provides the vocabularies overwhich the sentences are built and the morphisms in SigI , which we will simply callsignature morphisms, represent a change of notation. Signature morphisms act covariantly on sentences, and contravariantly on models. More concretely, given a signaturemorphism ϕ : Σ → Σ0 the sentences over the signature Σ are mapped to the sentences
over the signature Σ0 by the function Sen(ϕ) : Sen(Σ) → Sen(Σ0 ). The Σ0 -models are‘reduced’ to the signature Σ by the functor Mod(ϕ) : Mod(Σ0 ) → Mod(Σ). We denote
the reduct functor Mod(ϕ) by  ϕ and the function Sen(ϕ) by ϕ. If A = A0  ϕ we saythat A is the ϕ-reduct of A0 , and A0 is a ϕ-expansion of A.
3

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 |= Γ.

2.1

ExamplesWe give a few examples of institutions frequently occurring in algebraic specification
literature.
Example 2 (First-order logic (FOL) [12]).
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 is calleda constant symbol. Generally, ar ranges over arities, which are understood here as
strings of sorts; in other words an arity gives the number of arguments
together withU
their sorts. We overload the notation and let F and P also denote (ar,s)∈S ∗ ×S Far→sU
and 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 number of usual tricks, such as adding constants, but also, importantly, quantification, are viewed as expansions of the signature, so moving between signatures iscommon. To make such transitions smooth, the notion of a signature morphism isintroduced. Formally, a signature morphism ϕ : Σ → Σ0 , where Σ = (S, F, P ) andΣ0 = (S 0 , F 0 , P 0 ), is a triple ϕ = (ϕst , ϕop , ϕrl ) of maps:• ϕst : S → S 0 ,0∗• ϕop = {ϕopar→s : Far→s → Fϕst (ar)→ϕst (s) | ar ∈ S , s ∈ S},0∗• ϕrl = {ϕrlar : Par → Pϕst (ar) | ar ∈ S }.
rl
When there is no danger of confusion, we may let ϕ denote either of ϕst , ϕop
ar→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. 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:4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 . Since the models are many-sorted it is useful to have a terminologicaldistinction between carrier sets As of individual sorts, and the universe {As }s∈Sof the entire model. With this distinction at hand, note that the reduct functor
does not modify carrier sets of the sorts, but it can modify the universes ofmodels. For the universe of A0  ϕ is {A0ϕ(s) }s∈S , which means that the 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.
One important example of Σ-model is the absolutely free first-order Σ-structure ofterms TΣ that interprets each relation as the empty set.
Sentences. The set of Σ-sentences is given by the following grammar:e ::=t =s t0 | π(t1 , . . . , tn ) | ¬e | ∧E | ∃X · e0

where (i ) t =s t0 is an equation with t, t0 ∈ TΣ,s and s ∈ S, (ii ) π(t1 , . . . , tn ) is arelational atom with π ∈ Ps1 ...sn , ti ∈ TΣ,si and si ∈ S, (iii ) E is a finite set of
Σ-sentences, (iv ) X is a finite set of variables for Σ, (v ) ∃X · is just an abbreviationfor ∃χ · such that χ : Σ ,→ Σ[X] is an inclusion, Σ[X] = (S, F [X], P ), and F [X] isthe family of operation symbols obtained by adding the variables in X as constants to
F , (vi ) e0 is a Σ[X]-sentence. For any signature morphism ϕ : Σ → Σ0 the function
SenFOL (ϕ) : SenFOL (Σ) → SenFOL (Σ0 ) translates sentences symbolwise. In Section 3.2
we will give more details about quantification as a signature morphism, and sets ofvariables for a given signature.
Satisfaction relation. Satisfaction is the usual first-order satisfaction and it isdefined using the natural interpretations of ground terms t as elements tA in models
A
A. For example, A |= t1 =s t2 iff tA
1 = t2 .
Example 3 (Finitary first-order logic (FOLf )). This institution is obtained from
FOL by restricting the semantics to models with finite carrier sets. More concretely,
FOLf = (SigFOL , SenFOL , ModFOLf , |=FOL ), where ModFOLf is a subfunctor of ModFOL(i.e. ModFOLf (Σ) ⊆ ModFOL (Σ) for all Σ ∈ |SigFOL |) such that for all first-ordersignatures Σ = (S, F, P ) we have: A ∈ |ModFOLf (Σ)| iff A ∈ |ModFOL (Σ)| and As isfinite for all sorts s ∈ S.
Example 4 (Partial algebra (PA)). Here we consider the institution PA as employedby the specification language CASL [1].
A partial algebraic signature is a tuple (S, T F, P F ) such that (S, T F ∪ P F ) isan algebraic signature. Then T F is the set of total operations and P F is the set ofpartial operations. A morphism of PA signatures ϕ : (S, T F, P F ) → (S, T F 0 , P F 0 ) is
just a morphism of algebraic signatures (S, T F ∪ P F ) → (S, T F 0 ∪ P F 0 ) such thatϕ(T F ) ⊆ T F 0 and ϕ(P F ) ⊆ P F 0 .
A partial algebra A for a PA signature (S, T F, P F ) is just like an ordinary algebra
but interpreting the operations of P F as partial rather than total functions, whichmeans that σ A might be undefined for some arguments. A partial algebra homomorphism h : A → B is a family of (total) functions {hs : As → Bs }s∈S indexed by the5set of sorts S of the signature such that hs (σ A (a)) = σ B (hs (a)) for each operation
symbol σ : ar → s and each string of arguments a ∈ Aar for which σ A (a) is defined.
s
The sentences have three kinds of atoms: definedness def( ), strong equality = andeexistence equality =. The definedness def(t) of a term t holds in a partial algebrasA when the interpretation tA of t is defined. The strong equality t1 = t2 holds whenboth terms are undefined or both of them are defined and are equal. The existenceeequality t1 = t2 holds when both terms are defined and are equal. The sentences areformed from these atoms by means of Boolean connectives and quantification overtotal (first-order) variables. Note that each definedness atom def(t) is semanticallyesequivalent with t = t and any strong equality t1 = t2 is semantically equivalent withe(def(t1 ) ∨ def(t2 )) ⇒ t1 = t2 .
Example 5 (Higher-order logic (HOL)). This is a simplified version of higher-orderlogic which does not consider λ-abstraction. One could say HOL is λ-calculus without
λ, but nobody does. Probably because HOL is not calculus.
For any set S of sorts, let Type(S) be the set of S-types defined as the least set
such that S ⊆ Type(S) and s1 → s2 ∈ Type(S) when s1 , s2 ∈ Type(S). A HOLsignature is a tuple (S, F ), where S is a set of sorts and F is a family of sets ofconstants F = {Fs }s∈Type(S) . A signature morphism ϕ : (S, F ) → (S 0 , F 0 ) consists of afunction ϕst : S → S 0 and a family of functions between operation symbols {ϕops : Fs →Fϕ0 type (s) }s∈Type(S) where ϕtype : Type(S) → Type(S 0 ) is the natural extension of ϕst
to Type(S). For every signature (S, F ), a (S, F )-model A interprets each(a) sort s ∈ S as a set As , and(b) function symbol σ ∈ Fs as an element of As , where for all types s1 , s2 ∈ Type(S),As1 →s2 = [As1 → As2 ] = {f function | f : As1 → As2 }.
An (S, F )-model morphism h : A → B interprets each type s ∈ Type(S) as a function
hs : As → Bs such that h(σ A ) = σ B , for all function symbols σ ∈ F , and the following
diagram commutes
As1

f

hs1


Bs1

/ As2
hs2

hs1 →s2 (f )


/ Bs
2

for all types s1 , s2 ∈ Type(S) and functions f ∈ As1 →s2 .
An (S, F )-equation is an equation of the form t1 = t2 , where t1 and t2 are termsof the same type. Sentences are constructed from equations by iteration of Boolean
connectives and higher-order quantification over sets of variables of any type (which
is defined similarly to the first-order quantification).
Example 6 (Higher-order logic with Henkin semantics (HNK)). This institution extends HOL by relaxing the condition As1 →s2 = [As1 → As2 ] to As1 →s2 ⊆ [As1 → As2 ].
HNK has been introduced and studied in [3] and [24]. Again, we consider a simplified
version close to the “higher-order algebra” of [28] without λ-abstraction.
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 of6Σ-sentences E. A presentation morphism ϕ : (Σ, E) → (Σ0 , E 0 ) is a signaturemorphism ϕ : Σ → Σ0 such that E 0 |=Σ0 ϕ(E). Note that presentation morphisms
are closed under composition. The institution of presentations over I, denoted by
Ipres = (Sigpres , Senpres , Modpres , |=pres ) is defined as follows:• Sigpres is the category of presentations of 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.
Institutions of presentations include presentations of FOL (HNK, PA) with a particular set of axioms, but also, importantly, theories over FOL (HNK, PA).
Example 8 (Subsystems of second-order arithmetic). A concrete example of presentation is second-order arithmetic Z2 . It is defined over a first-order signatureΣ = (S, F, P ), with sorts Nat and Set, function symbols 0 :→ Nat, s : Nat → Nat+ : Nat Nat → Nat and × : Nat Nat → Nat, and membership relation ∈: Nat Set.
The number variables are usually denoted by lower case letters x, y, . . . , while set
variables are usually denoted by upper case letters X, Y, . . . . The axioms Γ of Z2 are
the usual Peano axioms, together with
• the induction axiom ∀X · 0 ∈ X ∧ ∀x · (x ∈ X ⇒ s x ∈ X) ⇒ ∀x · x ∈ X , and• universal closures of the comprehension scheme ∃X · ∀x · (x ∈ X ⇔ ρ[x]), forany sentence ρ over the signature Σ[x], such that X does not occur in ρ.1
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 [29]. Clearly, any subsystem of Z2 is a presentation over FOL.

3

Institution independent concepts

In this section, we introduce some concepts necessary to prove our abstract results.

3.1

Internal logic

The following institutional notions dealing with the semantics of Boolean connectives
and quantifiers were defined in [31].
Definition 9 (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;
1 If X could occur in ρ, then the formula x 6∈ X would produce an inconsistent comprehension
axiom ∃X · ∀x · (x ∈ X ⇔ x 6∈ X).

7

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 ∀χ · .
One should notice a peculiar treatment of quantifiers here, because it is one of distinctive characteristics of institution theory. 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 in institutions. Namely,let χ : Σ → Σ[x] be a signature morphism that adds the variable x as a new constantto Σ. The sentence ∀x · e0 is an abbreviation of ∀χ · e0 and the third clause in Definition 9 ensures that we consider all χ-expansions of A. Thus, the classical notion ofvaluation is incorporated into expansions. Variables do not belong to the language:
they can be imagined as coming from some external pool, but technically variables
are just special constants. Succinctly, one can say that variables in institutions arearbitrary constants, and so the usual messy caveats about avoiding accidental bindingof free variables are not needed. We devote Section 3.2 below to precise institutional
treatment of quantifiers.
Sentence building operators such as Boolean connectives and quantifiers are partof the metalanguage and they are used to construct sentences which belong to theinternal language of individual institutions using the universal semantics presented
above. One can also define ∨ , ∃χ · using the classical definitions. For example,∃χ · e0 := ¬∀χ · ¬e0 and > := ∧∅.
In this article, we consider conjunctions only over finite sets of sentences. The
concept of quantification we use is very general, and it can cover second order quantification in classical model theory. The universal quantifier ∀X · is regarded as anabbreviation for ∀χ · , where χ : Σ ,→ Σ[X] is an inclusion of signatures and Σ[X]denotes the extension of Σ with the variables from X as constants.
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 9.
Dealing with 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.

3.2

Quantification space

Quantification comes with some subtle issues related to the translation of quantified
sentences along signature morphisms. We alluded to that in Section 3.1; now we will
make it precise. Let us begin by a motivating example. Consider a first-order signature Σ and a Σ-sentence ∀x · ρ. In institutional model theory, ∀x · ρ is an abbreviation
8

ΣO 0

ϕ[χ]

/ Σ01
O

χ

Σ

ΣO 0
χ

χ(ϕ)

ϕ

ϕ[χ]

/ Σ1

Σ

/ Σ01 ψ[χ(ϕ)]/ Σ02
O
O
χ(ϕ)

ϕ

/ Σ1

ψ

χ(ϕ)(ψ)/ Σ2

Figure 1: Quantification pushoutsfor ∀χ · ρ, where χ : Σ ,→ Σ[x] is an inclusion of signatures, Σ[x] is the signature obtained from Σ by adding the variable x as a constant, and ρ is a sentence over Σ[x].
Clearly, ∀χ · ρ is not a sentence over Σ[x] because the domain of χ is not Σ[x] but
Σ. If we want a counterpart of ∀x · ρ in Σ[x] we need to translate it along χ, and to
do that, we need to rename x. The need to rename x can happen for essentially any
χϕsignature morphism ϕ, not only for χ. Diagramatically, we have Σ[x] ←- Σ → Σ1 , anda variable x1 for Σ1 . This implies that there are two further signature morphisms:
1. χ(ϕ) : Σ1 ,→ Σ1 [x1 ], which adds the variable x1 to Σ1 , and2. ϕ[χ] : Σ[x] → Σ1 [x1 ], which extends ϕ by maping x to x1 .
χ

ϕ

χ(ϕ)

ϕ[χ]

making {Σ[x] ←- Σ → Σ1 , Σ[x] → Σ1 [x1 ] ←- Σ1 } a pushout of signatures, whichwith Σ[x] = Σ0 and Σ1 [x1 ] = Σ01 is precisely the left-hand side diagram in Figure 1.
The renaming procedure can be iterated. In terms of diagrams: composing suchpushouts horizontally produces such pushouts again. Now for the definition.
Definition 10 (Quantification space [10]). Given a category Sig, a subclass of arrows
Q ⊆ Sig is called a quantification space if,χϕ

1. for any signature morphisms Σ → Σ0 ∈ Q and Σ → Σ1 ∈ Sig there is a
designated pushout depicted on the left in Figure 1 such that χ(ϕ) ∈ Q, and2. the horizontal composition of such designated pushouts is again a designatedpushout:(a) χ(1Σ ) = χ, 1Σ [χ] = 1Σ0 , and(b) for all pushouts such as the ones depicted on the right in Figure 1 we haveϕ[χ]; ψ[χ(ϕ)] = (ϕ; ψ)[χ] and χ(ϕ)(ψ) = χ(ϕ; ψ).
In concrete examples of institutions, the quantification space is fixed and thetranslation of a quantified sentence ∃χ · ρ ∈ Sen(Σ) along ϕ is ∃χ(ϕ) · ϕ[χ](ρ). The
second condition in Definition 10 is required by the functoriality of the translations.
3.2.1

ExamplesWe give some examples of quantification spaces for the institutions defined above. To
this end, we fix a countably infinite set {xi | i ∈ N} of variable names.
Example 11 (QFOL ). A FOL variable for a signature Σ = (S, F, P ) is a triple (xi , s, Σ),
where (a) i ∈ N and xi is the name of the variable, and (b) s ∈ S is the sort of9the variable. In FOL, the quantification space QFOL consists of signature extensions
with a finite number of variables χ : Σ ,→ Σ[X], where Σ is a first-order signatureand X = {Xs }s∈S is a finite set of variables for Σ. Given a signature morphism
ϕ : Σ → Σ1 in FOL, where Σ1 = (S1 , F1 , P1 ), then• χ(ϕ) : Σ1 ,→ Σ1 [X ϕ ] is an inclusion, where X ϕ = {(xi , ϕ(s), Σ1 ) | (xi , s, Σ) ∈ X},• ϕ[χ] is the extension of ϕ that maps each (xi , s, Σ) to (xi , ϕ(s), Σ1 ).
Example 12 (QPA ). A PA variable for a signature Σ = (S, T F, P F ) is a triple(xi , s, Σ), where (a) i ∈ N and xi is the name of the variable, and (b) s ∈ S is the sortof the variable. The quantification space QPA consists of signature extensions with afinite number of variables χ : Σ ,→ Σ[X], where Σ is a PA signature, X = {Xs }s∈S
is a finite set of variables for Σ, and Σ[X] = (S, T F ∪ X, P F ). The translation ofvariables along signature morphisms is defined as in the case of FOL.
Example 13 (QHNK ). A HNK variable for a signature Σ = (S, F ) is a triple (xi , s, Σ),
where (a) i ∈ N and xi is the name of the variable, and (b) s ∈ Type(S) is thetype of the variable. The quantification space QHNK consists of signature extensions
with a finite number of variables χ : Σ ,→ Σ[X], where Σ is a HNK signature, X ={Xs }s∈Type(S) is a finite set of variables for Σ such that Σ[X] = (S, F ∪ X). The
translation of variables along signature morphisms is defined as in the case of FOL.

4

Fraı̈ssé-Hintikka Theorem

In this section we prove an institution independent version of Fraı̈ssé-Hintikka Theorem .
Definition 14 (Unnested terms and unnested first-order atomic sentences). For any
first-order signature Σ = (S, F, P ), the set of unnested terms TΣu is defined as follows:u
for all constants (c :→ s) ∈ F , and1. c ∈ TΣ,su
2. σ(c1 , . . . , cn ) ∈ TΣ,sfor all operation symbols (σ : s1 . . . sn → s) ∈ F and all
constants (c1 :→ s1 ), . . . , (cn :→ sn ) ∈ F .

An unnested atomic Σ-sentence is any atomic Σ-sentence of the form:u
1. t = c, where s ∈ S, t ∈ TΣ,sand (c → s) ∈ F , or

2. π(c1 , . . . , cn ), where (π : s1 . . . sn ) ∈ P and (ci :→ si ) ∈ F .
Note that the translation of any unnested atomic sentence along a first-ordersignature morphism is also atomic and unnested. This means that the institutions
described in the following example are well-defined.
Example 15 (Unnested first-order logic (FOLu )). The following institutions are obtained from first-order logic by restricting the syntax:
1. FOL0 , the restriction of FOL to unnested atomic sentences, and
2. FOLu , the restriction of FOL to sentences obtained from the sentences in FOL0
by applying Boolean connectives and quantification over QFOL .
10

Similarly, one can define PA0 , PAu and HNK0 , HNKu .
Definition 16 (Equally strong institutions, I ∼ I0 ). Let I = (Sig, Sen, Mod, |=) and
I0 = (Sig, Sen0 , Mod, |=0 ) be two institutions that share Mod : Sig → Catop .
1. I0 is at least as strong as I, in symbols I . I0 , iff for every signature Σ ∈ |Sig|
and every sentence ρ ∈ Sen(Σ) there exists a sentence ρ0 ∈ Sen0 (Σ) such that
|Mod(Σ, ρ)| = |Mod(Σ, ρ0 )|.
2. I and I0 are equally strong, in symbols I ∼ I0 , iff I . I0 and I0 . I.
Lemma 17. We have FOLu ∼ FOL, PAu ∼ PA and HNKu ∼ HNK.
Proof. We focus on first-order case as the other two cases are analogous.
It suffices to show that any first-order atomic sentence is semantically equivalent
to a sentence obtained from the sentences in FOL0 by applying Boolean connectives
and quantification over finite sets of variables. There are two cases to consider.
1. For equations we proceed by induction on the structure of the terms. The basecase c1 = c2 , where (c1 :→ s), (c2 :→ s) ∈ F , is ensured by the fact that c1 = c2 isunnested.
For the induction step, we prove the statement for σ(t1 , . . . , tn ) = t assuming that
it holds for all equations constructed from terms that have a depth less or equal
than the maximum depth of the terms t1 , . . . , tn , t:1

σ(t1 , . . . , tn ) = t |=| ∀x1 , . . . , xn , x ·n^(ti = xi ) ∧ (t = x) ⇒

i=1

2
3

σ(x1 , . . . , xn ) = x
there exist ρi , ρ ∈ SenFOLu (Σ[x1 , . . . , xn , x]) such thatti = xi |=| ρi and t = x |=| ρn^ρi ∧ ρ ⇒ σ(x1 , . . . , xn ) = xσ(t1 , . . . , tn ) = t |=| ∀x1 , . . . , xn , x ·by induction
hypothesis

i=1

2. For relations π(t1 , . . . , tn ):1π(t1 , . . . , tn ) |=| ∀x1 . . . xn ·n^(ti = xi ) ⇒ π(x1 , . . . , xn )i=1

2

there exist ρi ∈ SenFOLu (Σ[x1 , . . . , xn ]) such that ρi |=| t = xi

3π(t1 , . . . , tn ) |=| ∀x1 . . . xn ·n^by the proofabove

ρi ⇒ π(x1 , . . . , xn )i=1

Definition 18 (Institution with structured syntax). An institution of the form I =(Sig, Sen, Mod, |=) has a structured syntax if it is equipped with (a) a subfunctor
Senb : Sig → Set of Sen : Sig → Set (i.e. Senb (Σ) ⊆ Sen(Σ) for all signaturesΣ ∈ |Sig|), and (b) a quantification space Q ⊆ Sig such that
1. I is semantically closed under Boolean connectives and quantification over thesignature morphisms in Q, and11

2. I ∼ Iu , where Iu is obtained from I by restricting the syntax to sentences
obtained from the sentences of Ib = (Sig, Senb , Mod, |=) by applying Boolean
connectives and quantification over Q.
An example of institution with structured syntax, or, as we will also say, syntactically structured institution, is FOL.
Example 19. FOL is a syntactically structured institution, where
1. Ib is FOL0 , the restriction of FOL to unnested atomic sentences, and
2. Q is QFOL , the quantification space defined in Example 11.
By Lemma 17, PA and HNK are also syntactically structured.
Lemma 20. Let I = (Sig, Sen, Mod, |=) be a syntactically structured institution as
described in Definition 18. Then Ipres = (Sigpres , Senpres , Modpres , |=pres ) is a syntactically structured institution with the following parameters:
1. the sentence functor Senpres: Sigpres → Set is defined by Senpres(Σ, E) =bb
Senb (Σ) for all presentations (Σ, E) ∈ |Sigpres |, and2. the quantification space Qpres consists of all presentation morphisms χ : (Σ, E) →(Σ0 , χ(E)) with χ : Σ → Σ0 ∈ Q.
the
Proof. Let Iu = (Sig, Senu , Mod, |=) be as described in Definition 18, and Ipresuinstitution obtained from Ipres by restricting the syntax to the sentences obtained
from the sentences of Ipres= (Sigpres , Senpres, Modpres , |=pres ) by applying Boolean
b
b
pres
pres
connectives and quantification over Q. I
is semantically closed under Boolean
connectives, as I is semantically closed under Boolean connectives. We show that:
Ipres ∼ Ipresu123

let (Σ, E) ∈ |Sigpres | and ρ ∈ Sen(Σ)ρ |=Σ γ and γ |=Σ ρ for some γ ∈ Senu (Σ)
presρ |=pres(Σ,E) γ and γ |=(Σ,E) ρ for some γ ∈ Senu (Σ)

4

Ipres ∼ Ipresusince I ∼ Iu
by the definition of |=pressince (Σ, E) ∈ |Sigpres | andρ ∈ Sen(Σ) were arbitrarily chosen

Hence, Ipres is syntactically structured.
A direct consequence of Lemma 17 and Lemma 20 is the following corollary.
Corollary 21. FOLpres ∼ FOLpres, PApres ∼ PApres
and HNKpres ∼ HNKpres.
uuu
Another important class of institutions that fall under the framework developedin the present contribution are the institutions obtained by restricting the semantics
of some standard logical system.
Lemma 22. Let I = (Sig, Sen, Mod, |=) and I0 = (Sig, Sen, Mod0 , |=) be two institutions such that Mod0 is a subfunctor of Mod. If I is syntactically structured then I0 is
syntactically structured as well.
Proof. Assume that I is syntactically structured with the following parameters: (a) the
sentence functor is Senb , and (b) the quantification space is Q. We show that I is syntactically structured with the same parameters. Since I is semantically closed under12

Boolean connectives and quantification over Q, I0 is semantically closed under Boolean
connectives and quantification over Q. Let Iu = (Sig, Senu , Mod, |=) be as describedin Definition 18, and I0u = (Sig, Senu , Mod0 , |=). Then:
1
2
3
4
5
6

let Σ ∈ |Sig| and ρ ∈ Sen(Σ)|Modpres (Σ, ρ)| = |Modpres (Σ, γ)| for some γ ∈ Senu (Σ)|Mod0pres (Σ, ρ)| = |Mod0 (Σ)| ∩ |Modpres (Σ, ρ)||Mod0pres (Σ, γ)| = |Mod0 (Σ)| ∩ |Modpres (Σ, γ)||Mod0pres (Σ, ρ)| = |Mod0pres (Σ, γ)|I0 ∼ I0u

since I ∼ Iu
by the definition of Mod0presby the definition of Mod0presfrom 2, 3 and 4
since Σ and ρ werearbitrarily chosen

Hence, I0 is syntactically structured.
A direct consequence of Lemma 17 and Lemma 22 is the following corollary.
Corollary 23. FOLf and HOL are syntactically structured.
Proof. By noting that FOLf are HOL are obtained by restricting the semantics of FOL
and HNK, respectively.
Ehrenfeucht-Fraı̈ssé games in institutions. We now define an abstract equivalence between models of a syntactically structured institution, based on EhrenfeuchtFraı̈ssé games.
Definition 24 (Trees). Given a syntactically structured institution I as described in
Definition 18, a Q-tree tr is inductively defined as follows:
1. any signature Σ is a Q-tree with the root Σ and height 0;
2. if λ is a nonzero cardinal, {χi : Σ → Σi }i<λ is a family of signature morphisms
from Q and {tri }i<λ is a family of Q-trees of height at most k such that(a) the root of tri is Σi for all i < λ, and(b) the height of trj is k for some j < λ,χithen Σ{( tri }i<λ is a Q-tree with root Σ and height k + 1.
The definition above formalizes trees of finite height and possibly infinitely branchedwith nodes signatures and edges signature morphisms used for quantification.
Definition 25 (Game equivalence). Let I be a syntactically structured institution as
described in Definition 18. The game equivalence between two models A and B overthe same signature Σ is defined via Q-trees tr with the root Σ:[ height(tr) = 0 ] A ≈tr B iff the following property holds:
A |= ρ iff B |= ρ, for all ρ ∈ Senb (Σ).
χi[ height(tr) > 0 ] Let tr = Σ{( tri }i<λ and assume that the relation Ai ≈tri Bi
has been defined for all i < λ and any Σi -models Ai and Bi , where Σi = root(tri ).
Then A ≈tr B iff the following properties hold:13

1. for any i < λ and all χi -expansions Ai of A there exists a χi -expansion Bi of
B such that Ai ≈tri Bi , and
2. for any i < λ and all χi -expansions Bi of B there exists a χi -expansion Ai of
A such that Ai ≈tri Bi .
The definition of game equivalence is stated, of course, with Ehrenfeucht-Fraı̈ssé
games in mind. In the abstract institutional setting, the game Etr (A, B) is parameterized by two models A and B and a Q-tree tr. We think of the models A and
B as game pieces, and of the tree as a gameboard. The play of the game proceeds
in stages, corresponding to the levels of tr; at each stage the play climbs one levelup the tree. The image here is that the pieces (models) move on a board consistingof signature morphisms: each move along a morphism corresponds to picking an element. This image is in stark contrast to the classical image where models themselves
are the board, and moves are choices of elements. Although either image is just a
visualization, we claim that our image agrees better with the inner workings of institutions. After all, “picking an element” must be rendered as a signature morphism(nothing else is there to play that role); a signature morphism is an arrow, and eachmove consists in a piece moving along an arrow.
The play starts at the root, labelled by Σ. At the initial (0th) stage of the play,
the universal quantifier player (∀belard, as tradition has it) picks the structure A
or B and if A and B do not satisfy precisely the same sentences from Senb (Σ) the
existential quantifier player (∃loise, of course) loses immediately. Otherwise the playcontinues, and at the end of stage j, say, it has reached a node labelled by a signatureΣ0 at level j with some expansions A0 and B0 of A and B, such that A0 and B0 satisfy
precisely the same sentences from Senb (Σ0 ). Now, if Σ0 is a leaf node, ∀belard loses.
Otherwise, he picks a signature morphism χi labelling an upward edge of Σ0 and a
χi -expansion A0i of A0 (or a χi -expansion B0i of B0 ; we will stick to A0 for brevity).
∃loise has to respond with a χi -expansion B0i of B0 in such a way that the expansions
A0i and B0i satisfy precisely the same sentences from Senb (Σ0 ). If she cannot do it, sheloses; if she can, the play climbs up the edge χi and continues at the node one level
higher.
As usual, we say that ∃loise has a winning strategy in Etr (A, B), if she can win
regardless of the moves ∀belard makes. We should remark here that our abstract
definition of Ehrenfeucht-Fraı̈ssé games differs from what the reader may expect inthat the Q-tree for the game is given beforehand, generally limiting ∀belard’s choices.
We do not do it to give female players an edge, but because we wish to apply thegames to logics with infinite signatures, for which certain restrictions of the possible
moves are necessary in order to define game sentences (to come shortly).
Definition 26 (Perfect trees). A perfect λ-ary tree, where λ is a cardinal, is a treeof finite height such that (a) every node has λ descendants, and (b) each leaf node isat the same height.
Since every tree of finite height is a subtree of a perfect tree, it suffices to consider
only perfect Q-trees. The lemma below makes it explicit.
Lemma 27. ∃loise has a winning strategy for all games Etr (A, B) with arbitrary QI trees tr if and only if she has a winning strategy for all games Etr (A, B) with perfect
Q-trees tr.
14Σ[x1 , x4 ] Σ[x1 , x5 ] Σ[x1 , x6 ] Σ[x2 , x7 ] Σ[x2 , x8 ] Σ[x2 , x9 ] Σ[x3 , x10 ] Σ[x3 , x11 ] Σ[x3 , x12 ]
χ4

χ5

χ6

χ7

Σ[x1 ]

χ8

χ9

χ10

Σ[x2 ]
χ2

χ1

χ11 χ12
Σ[x3 ]

χ3

Σ
Figure 2: Perfect ternary tree of height 2
Ehrenfeucht-Fraı̈ssé games in first-order logic. We will now instantiate ourabstract description of Ehrenfeucht-Fraı̈ssé games in first-order logic. It will turn outthat in the single-sorted case we get precisely the usual Ehrenfeucht-Fraı̈ssé games,
whereas in many-sorted case we obtain a notion slightly different from the usual one.
Definition 28 (First-order gameboard trees). Let Σ be a FOL signature with a (possibly infinite) set S of sorts. A gameboard QFOL -tree tr with the root Σ is a perfect
λ-ary tree such that (a) λ ≤ card(S), and (b) for each internal node Σ0 the upward
edges of Σ0 are signature morphisms of the form χi : Σ0 ,→ Σ0 [xi ], for all i < λ, suchthat for any i 6= j, xi and xj are variables of different sorts.
Let Σ = (S, F, P ) be a FOL signature such that S = {s1 , s2 , s3 }. A perfect ternary
tree of height 2 is depicted in Figure 2. The labels χ1 , . . . , χ12 are signature extensions
with one variable; the variables x1 , x2 , x3 have sorts s1 , s2 , s3 , respectively; similarly,
the variables x4 , x5 , x6 have sorts s1 , s2 , s3 , respectively.
Let A and B be two first-order structures over the same signature Σ = (S, F, P ).
The unnested Ehrenfeucht-Fraı̈ssé game Ek (A, B) of length k ∈ N, is played in k
steps, as follows. At the jth step of a play, ∀belard takes one of the structures A or
B, say A, and chooses an element a of any sort s of this structure. Then ∃loise chooses
an element of the same sort from B. At the jth step of the play, both players havechosen sequences of elements a1 . . . aj and b1 . . . bj such that ai and bi have the same
sorts si , for all i ∈ {1, . . . , j}. In the argot of institutions, this amounts to choosing jvariables x1 , . . . , xj of sorts s1 , . . . , sj , respectively, and the expansions (A, a1 , . . . , aj )and (B, b1 , . . . , bj ) of A and B to the signature Σ[x1 , . . . , xj ]. Proceeding this way, atthe end of the play, sequences a = a1 . . . ak and b = b1 . . . bk have been chosen. The
play with these choices is a win for ∃loise, if (A, a) ≈Σ[x1 ,x2 ...,xk ] (B, b), that is (A, a)and (B, b) satisfy the same unnested atomic sentences.
What we have just described is an instance of the definition of Ehrenfeucht-Fraı̈ssé
games in institutions, which corresponds to the classical definition of EhrenfeuchtFraı̈ssé games in first-order logic. In other words, Ek (A, B) denotes the game Etr (A, B),
where tr is a gameboard tree of height k with branching λ, where λ = card(S). The
reader can consult [26] for (much) more on games for elementary equivalence in singlesorted first-order logic. In many-sorted case (if you treat sorts seriously, as it is donein most computer science applications), our definition of the game differs from theusual one. To see where the difference lies, here is a simple example.

15

Example 29. Let k ≥ 2 be a natural number. Let a first-order signature Σ = (S, F, P )be: (a) S = {s1 , . . . , sk , s0k }, (b) F = ∅, and (c) P = {(π : s1 . . . sk ), ($ : s1 . . . sk−1 s0k )}.
Next, we define two Σ-models A and B putting:(a) As1 = {a1 , c1 }, As2 = {a2 }, . . . , Ask = {ak }, As0k = {a0k } and
π A = {(a1 , . . . , ak )}, $A = {(a1 , . . . , ak−1 , a0k )}.
(b) Bs1 = {b1 , d1 }, Bs2 = {b2 } . . . , Bsk = {bk }, Bs0k = {b0k } andπ B = {(d1 , b2 , . . . , bk )}, $B = {(b1 , . . . , bk−1 , b0k )}.
Lemma 30. If A and B are the models defined in Example 29 then A ≈c B for all
chains of length at most k, but A 6≈tr B for a perfect gameboard tree of height k.
Proof. For the sake of simplicity, we assume that k = 2, as the generalization to any
natural number k is straightforward.
Firstly, we show that A 6≈tr B, where tr is the perfect 3-ary tree of height 2
depicted in Figure 2 such that (a) the leftmost variable has the sort s1 , (b) the
variable in the middle has the sort s2 , and (c) the rightmost variable has the sort s02 .
Now, suppose ∀belard chooses a1 then ∃loise can chose either b1 or d1 :1. if ∃loise chooses b1 then ∀belard can choose a2 . In this case, the only possible
choice for ∃loise is b2 . Hence, A |= π(a1 , a2 ) but B 6|= π(b1 , b2 )2. if ∃loise chooses d1 then ∀belard can choose a02 . In this case, the only possible
choice for ∃loise is b02 . Hence, A |= $(a1 , a02 ) but B 6|= $(d1 , b02 ).
Secondly, we show that A ≈c B for any chain c of length 2. The interesting cases
are when the variables added are of different sorts. We enumerate the non-trivial
cases below:
1. c := Σ ,→ Σ[x1 ] ,→ Σ[x1 , x2 ], where x1 is of sort s1 and x2 is of sort s2 . All
unnested atoms over Σ[x1 , x2 ] are x1 = x1 , x2 = x2 and π(x1 , x2 ). The identities
x1 = x1 and x2 = x2 are not relevant as they are satisfied by all models. There
are only two expansions of A, (A, a1 , a2 ) and (A, c1 , a2 ), and two expansionsof B, (B, b1 , b2 ) and (B, d1 , b2 ). The game is won by ∃loise, as all choices of∀belard lead to the following expansions:(a) (A, a1 , a2 ) which can be matched by (B, d1 , b2 ), that is A |= π(a1 , a2 ) andB |= π(d1 , b2 ),(b) (A, c1 , a2 ) which can be matched by (B, b1 , b2 ), that is A 6|= π(c1 , a2 ) andB 6|= π(b1 , b2 ), and(c) (B, d1 , b2 ) which can be matched by (A, a1 , a2 ),(d) (B, b1 , b2 ) which can be matched by (A, c1 , a2 ).
2. c := Σ ,→ Σ[x1 ] ,→ Σ[x1 , x02 ], where x1 is of sort s1 and x02 is of sort s02 . As
in the case above, all unnested atoms over Σ[x1 , x2 ] are x1 = x1 , x02 = x02 and$(x1 , x02 ). There are only two expansions of A, (A, a1 , a02 ) and (A, c1 , a02 ), andtwo expansions of B, (B, b1 , b02 ) and (B, d1 , b02 ). The game is won by ∃loise, as
all ∀belard’s choices lead to the following expansions:16

(a) (A, a1 , a02 ) which can be matched by (B, d1 , b02 ), that is A |= $(a1 , a02 ) andB |= π(d1 , b02 ),(b) (A, c1 , a02 ) which can be matched by (B, b1 , b02 ), that is A 6|= π(c1 , a02 ) andB 6|= π(b1 , b02 ), and(c) (B, d1 , b02 ) which can be matched by (A, a1 , a02 ),(d) (B, b1 , b02 ) which can be matched by (A, c1 , a02 ).
The reason for the difference is that some trees that are not perfect (such as chains)limit severely the choices ∀belard can make. Of course, knowing the tree beforehand∃loise can adjust her strategy accordingly. Two more remarks are in order.
1. In single-sorted first-order logic, any gameboard tree tr is a chain, and Etr (A, B)
always coincides with the usual game, so our formulation agrees with the classical formulation.
2. For two first-order structures over a signature with a set of sorts with at least
two elements, the game which is equivalent to the “classically expected game”
is the game over a perfect λ-ary tree, where λ is the cardinal of the set of sorts:
at any point during the game, ∀belard can choose any element of any sort fromthe (many-sorted) universes of two models; in order to make this possible, any
inner node of the gameboard tree needs a λ-ramification such that each childadds (to the parent signature) exactly one variable and the sorts of the added
variables cover all sorts of the signature.
To sum up, we see the perfect gameboard trees as stepping stones from intuition
to formalization. We could formalize the games differently, yet some generalizations
are necessary in dealing with infinite signatures. We chose infinite branching, as we
believe it maintains balance between intuition and formalization.
PA and HNK gameboard trees are defined analogously to first-order logic case.
In HNK, there are infinitely branching gameboard trees for each signature with atleast one sort, since the set of types over such signatures is infinite. Instantiating
the abstract description of Ehrenfeucht-Fraı̈ssé games to these concrete institutions,using only gameboard trees, is straightforward.
Finite trees and game sentences. With finitely branching Q-trees of height k, one
can associate special sentences, usually called game formulas, characterizing winning
strategies in Ehrenfeucht-Fraı̈ssé games up to length k. For single sorted FOL it wasdone by Hintikka in [25]. Note that in single-sorted FOL, gameboard trees are actuallyfinite chains.
As we mentioned a number of times already, in order to define game formulas, weneed to restrict the signatures so that the set of unnested atomic sentences is finite.
Definition 31 (Finitary signatures). Let I be a syntactically structured institution
as described in Definition 18. A signature Σ in I is finitary iff for all Q-chainsc = {χi : Σi → Σi+1 }i<k with k ∈ N and Σ0 = Σ, the set Senb (Σk ) is finite.
In concrete examples, finitary signatures have the set of function and relation
symbols finite, however, the set of sorts of finitary signatures may be infinite as thenext lemma shows.
Lemma 32 (First-order finitary signatures). A first-order signature Σ = (S, F, P ) is
finitary iff both sets F and P are finite.
17

Proof. The forward implication is straightforward. We focus on the converse implication. It suffices to prove that for any finite set of variables X for Σ, the set ofunnested atomic sentences SenFOL0 (Σ) is finite. Since F ∪ X is finite, the set of termsof depth less than or equal to two is finite. Since P is finite, the set of unnested
atomic sentences over Σ[X] is finite too.
In all examples of institutions given in this article, sentences are built from a finite
number of symbols. Therefore, any sentence is included in a signature with a finite
number of symbols.
Definition 33 (Game sentences). Let I = (Sig, Sen, Mod, |=) be a syntactically structured institution as described in Definition 18. For all finite Q-trees tr such thatroot(tr) is finitary, the finite set of sentences Θtr is defined as follows:[ height(tr) = 0 ] In this case, tr consists of a single root node, labelled by Σ, and
 ^
Θtr =
ef (e) | f : Senb (Σ) → {0, 1} ,e∈Senb (Σ)
1where e stands for e and e0 stands for ¬e for all e ∈ Senb (Σ).
χ1χn[ height(tr) > 0 ] Let tr = Σ{( tr1 , . . . , ( trn } be a tree and assume that thefinite set of sentences Θtri has been defined for all i ∈ {1, . . . , n}. Then:• Θtr = {γE1 ∧ . . . ∧ γEn | E1 ⊆ Θtr1 , . . . , En ⊆ Θtrn }, where^_• γ Ei = (∃χi · e) ∧ ∀χi ·Ei for all i ∈ {1, . . . , n}.
e∈Ei

The sentences in Θtr will be referred to as sentences in game-normal form, or
more briefly game-normal sentences.
Theorem 34 (Fraı̈ssé-Hintikka Theorem). Consider a syntactically structured institution I = (Sig, Sen, Mod, |=) with the following parameters: (a) Senb : Sig → Set isthe sentence subfunctor which maps signatures to sets of ‘unnested atomic’ sentences,and (b) Q is the quantification space. Let Σ be a finitary signature in I.
T1) For each Σ-model A and all finite Q-trees tr, there exists a unique sentenceγ(A,tr) ∈ Θtr such that A |= γ(A,tr) .
T2) A ≈tr B iff there exists a unique ρ ∈ Θtr such that A |= ρ and B |= ρ,for all Σ-models A, B and finite Q-trees tr with root Σ.
T3) For all sentences ρ ∈ Sen(Σ), there exist aWfinite chain of signature morphisms
in Q and a subset Γρ ⊆ Θc such that ρ |=| Γρ .
Proof.
T1) We proceed by induction on the structure of tr:[ height(tr) = 0 ] This case is straightforward.

18

χ1

χn

[ height(tr) > 0 ] Let k = height(tr), tr = Σ{( tr1 , . . . , ( trn }, and Σi =root(tri ) for all i ∈ {1, . . . , n}.
By the induction hypothesis, for each i ∈ {1, . . . , n} and any χi -expansion Ai
of A there exists a unique sentence γ(Ai ,tri ) ∈ Θtri such that Ai |= γ(Ai ,tri ) .
• Let Γ(A,tr,i) ⊆ Θtri be the set of sentences consisting of all γ(Ai ,tri ) ∈ Θtri ,where Ai is some χi -expansion of A.
n^• Let γ(A,tr) ={γEi | Ei = Γ(A,tr,i) }.
i=1

It is straightforward to check that A |= γ(A,tr) .
n^
If A |=
γEi ∈ Θtr then we show that Ei = Γ(A,tr,i) for all i ∈ {1, . . . , n}:i=1

let i ∈ {1, . . . , n} and note that γEi = (1^∃χi · e) ∧ ∀χi ·

_

Ei

e∈Ei

Ei ⊆ Γ(A,tr,i)2^since A |= γEi , we have A |=∃χi · ee∈Ei

Γ(A,tr,i) ⊆ Ei
Γ(A,tr,i) = Ei

3
4

since A |= γEi , we have A |= ∀χi ·W

Eifrom 2 and 3

T2) We proceed by induction on the structure of tr.
[ height(tr) = 0 ] This case is straightforward.
χ1

χn[ height(tr) > 0 ] Let k = height(tr), tr = Σ{( tr1 , . . . , ( trn }, and Σi =root(tri ) for all i ∈ {1, . . . , n}.
For the forward implication, assume that A ≈tr B. We show that γ(A,tr) =γ(B,tr) , which is equivalent to Γ(A,tr,i) = Γ(B,tr,i) for all i ∈ {1, . . . , n}:• Γ(A,tr,i) ⊆ Γ(B,tr,i) :
1
2
3
4
5
6

let e ∈ Γ(A,tr,i)Ai |= e for some χi -expansion Ai of A
Ai ≈tri Bi for some χi -expansion of B
Ai |= ρ and Bi |= ρ for some unique ρ ∈ Θtri
ρ=ee ∈ Γ(B,tr,i)by the definition of Γ(A,tr,i)by Definition 25
by the induction hypothesis
by statement T1 above
since Bi |= e and Bi is a
χi -expansion of B

• Γ(B,tr,i) ⊆ Γ(A,tr,i) : similarly as above.
For the converse implication, assume that A |= ρ and B |= ρ for some ρ ∈ Θtr .
n^
By Definition 33, we have ρ =γEi , where Ei ⊆ Θtri for all i ∈ {1, . . . , n}.
i=1• We show that for each i ∈ {1, . . . , n} and any χi -expansion Ai of A there
exists a χi -expansion Bi of B such that Ai ≈tri Bi :1
2
3

let i ∈ {1, . . . , n} and let Ai be a χi -expansion of A
W
A |= ∀χi · Ei
since A |= γEi
WAi |= Ei
since Ai is a χi -expansion of A

19

4
5

Ai |= e for some e ∈ Ei^
B |=∃χi · e0by the semantics ofW

since B |= γEie0 ∈Ei6
7
8

B |= ∃χi · e
Bi |= e for some χi -expansion Bi of B
Ai ≈tri Bi

since e ∈ Ei
by the semantics of ∃by the induction hypothesis, sinceAi |= e and Bi |= e

• Similarly, one can show that for each i ∈ {1, . . . , n} and any χi -expansion Bi
of B there exists a χi -expansion Ai of A such that Ai ≈tri Bi
T3) Since I syntactically structured, it suffices to consider only sentences ρ obtained
from the sentences in Ib by applying Boolean connectives and quantification overthe signature morphisms in Q. We proceed by induction on the structure of ρ:[ For ρ ∈ Senb (Σ) ] Let Γρ ⊆ ΘΣ be the subset of all sentences inWΘΣ which containρ without negation. It is straightforward to show that ρ |=| Γρ .
W
[ For ¬ρ ] By the induction hypothesis, ρ |=| Γρ for some Q-chain c and subsetΓρ ⊆ Θc . Let Γ(¬ρ) = Θc W
\ Γρ be the complement of Γρ in Θc . It is straightforward to show that ¬ρ |=| Γ(¬ρ) .
W[ For ρ1 ∧ ρ2 ] By the induction hypothesis, ρi |=| Γρi for some Q-chainc andWsome subset Γρi ⊆ Θc . It is straightforward to show that ρ1 ∧ρ2 |=| (Γρ1 ∩Γρ2 ).
W[ For ∃χ · ρ, where χ : Σ → Σ1 ] By the induction hypothesis, ρ |=| Γρ for someQ-chain c1 = {χi : Σi → Σi+1 }1≤i<k and subset Γρ ⊆ Θc1 . We define the
Q-chain c = {χi : Σi → Σi+1 }i<k , where Σ0 = Σ and χ0 = χ.
Let Γ(∃χ · ρ) = {γE | E ⊆ Θc1 and E ∩ Γρ 6= ∅}.
W• We show that ∃χ · ρ |= Γ(∃χ · ρ) :
1
2
3
4
5

assume that A |= ∃χ · ρ
A1 |= ρ for some χ-exp. A1 of A
W
A1 |= ΓρA1 |= e for some e ∈ Γρe ∈ Γ(A,c) ∩ Γρ67γ(A,c) = γΓ(A,c) ∈ Γ(∃χ · ρ)W
A |= Γ(∃χ · ρ)

• We show that
1
2
3
4

W

by the semantics of ∃W
since ρ |=| ΓρWby the semantics ofsince Γ(A,c) consists of all sentences inΘc1 satisfied by some expansion of A
by the definition of Γ(∃χ · ρ)
since A |= γ(A,c) and γ(A,c) ∈ Γ(∃χ · ρ)Γ(∃χ · ρ) |= ∃χ · ρ:Wassume that A |= Γ(∃χ · ρ)A |= γE for some E ⊆ Θc1 such thatE ∩ Γρ 6= ∅γE = γ(A,c)Γ(A,c) ∩ Γρ 6= ∅20

by the definition of Γ(∃χ · ρ)by statement T2 above
since Γ(A,c) = E and E ∩ Γρ 6= ∅

5
6
7
8

A1 |= e for some χ-expansion A1 of
A and some e ∈ Γ(A,c) ∩ ΓρW
A1 |= ΓρA1 |= ρA |= ∃χ · ρ

since Γ(A,c) consists of all sentences inΘc1 satisfied by some χ-expansion of A
since e ∈ ΓρWsince Γρ |=| ρ
since A1 is a χ-expansion of A

W
[ For ∀χ · ρ, where χ : Σ → Σ1 ] By the induction hypothesis, ρ |=| Γρ for someQ-chain c1 = {χi : Σi → Σi+1 }1≤i<k and subset Γρ ⊆ Θc1 . We define the
Q-chain c = {χi : Σi → Σi+1 }i<k , where Σ0 = Σ and χ0 = χ.
Let Γ(∀χ · ρ) = {γE | E ⊆ Γρ }.
W• We show that ∀χ · ρ |= Γ(∀χ · ρ) :1
2

assume that A |= ∀χ · ρ
Γ(A,c) ⊆ Γρ

2.3
2.4
2.5
2.6

let e ∈ Γ(A,c)
e = γ(A1 ,c1 )for some χ-expansion A1 of A
A1 |= ρW
A1 |= ΓρA1 |= e1 for some e1 ∈ Γρ
e1 = γ(A1 ,c1 )2.7

e = γ(A1 ,c1 ) = e1 ∈ Γρ

2.1
2.2

3
4

by the following proof steps• We show thatsince A |= ∀χ · ρWsince ρ |=| Γρby the semantics ofW

as e1 ∈ Θc1 and A1 satisfies a uniquesentence in Θc1from 2.2, 2.5 and 2.6γ(A,c) = γΓ(A,c) ∈ Γ(∀χ · ρ)W
A |= Γ(∀χ · ρ)Wby the definition of Γ(A,c)

by the definition of Γ(∀χ · ρ)
since A |= γ(A,c) and γ(A,c) ∈ Γ(∀χ · ρ)Γ(∀χ · ρ) |= ∀χ · ρ:

1
2
3

W
assume that A |= Γ(∀χ · ρ)A |= γE for some E ⊆ ΓρW
A |= ∀χ · E

by the definition of Γ(∀χ · ρ)_^∃χ · e) ∧ ∀χ ·Esince γE = (45WA |= ∀χ · ΓρA |= ∀χ · ρ

since E ⊆ ΓρWsince ρ |=| Γρe∈ENotice that Fraı̈ssé-Hintikka Theorem is applicable to any syntactically structured
institution I. Therefore, it has a very wide range of applications. The following characterization of elementary equivalence is a corollary of the Fraı̈ssé-Hintikka Theorem.
Corollary 35 (Fraı̈ssé-Hintikka Theorem concretely). Let I be one of the institutions
FOL, HNK, PA, FOLpres , HNKpres , PApres , FOLf or HOL. Let A and B be two models
over a signature Σ in I. The following are equivalent:
C1) A ≡ B;
C2) ∃loise has a winning strategy for the game Etr (A  Σf , B  Σf ), for all finite subsignatures Σf of Σ and all finite gameboard trees tr with the root Σf .

21C3) A  Σf ≈c B  Σf for all finite sub-signatures Σf of Σ, and all finite chains c withthe root Σf .
Proof. By Lemma 17, FOL, PA and HNK are syntactically structured. By Corollary 21, FOLpres , HNKpres are PApres are syntactically structured. By Corollary 23,
FOLf and HOL are syntactically structured. It follows that Theorem 34 is applicableto the institution I.
[ C1 ⇒ C2 ] Let Σf be a finite sub-signature of Σ and tr a finite gameboard treewith the root Σf . Since A ≡ B, we have A  Σf ≡ B  Σf . By Theorem 34 (T1),
it follows that γ(A,tr) = γ(B,tr) ∈ Θtr . By Theorem 34 (T2), A  Σf ≈tr B  Σf .
Therefore, ∃loise has a winning strategy for the game Etr (A  Σf , B  Σf ).
[ C2 ⇒ C3 ] Every chain is a tree.
[ C3 ⇒ C1 ] We show that A |= ρ implies B |= ρ for all ρ ∈ Sen(Σ):

56assume that A |= ρ
ρ = χ(ρf ) for some finite signature Σf ,
Σf -sentence ρf and inclusion χ : Σf ,→ ΣA  χ |= ρfW
ρf |=| E for some Q-chain c and subset
E ⊆ Θc .
W
A  χ |= EW
B  χ |= E78B  χ |= ρf
B |= ρ

12
3
4

ρ is composed of a finite number ofsymbolsby the satisfaction condition
by Theorem 34 (T3)by 3 and 4
by Theorem 34 (T1 & T2), sinceA  χ ≈c B  χWsince ρf |=| Eby the satisfaction condition

Similarly, one can assume A |= ρ and then show B |= ρ for all ρ ∈ Sen(Σ).
An analogous corollary holds for FOLpres
and HOLpres , too. Subsystems of secondf
order arithmetic, mentioned in Example 8, are instances of FOLpres .

5

Conclusions

Perhaps the classical hard-liner who insists that higher-order logic with Henkin semantics is nothing but a variant of first-order logic, still wonders what we have achievedin this article, apart from fancy terminology and notation. We believe the gain is
manifold.
First and foremost, we provided a general proof of Fraı̈ssé-Hintikka Theorem in theframework of institutions applicable to a wide range of logical systems. In addition
to the applications given above, Theorem 34 applies also to the class of constructorbased logics which are obtained from some base logic by restricting the semantics tomodels reachable by some constructor operators [2]. This is an immediate corollaryof the fact that Lemma 22 holds for these. Constructor-based logics are used in thearea of formal methods [23, 22].

22

Secondly, our proof is what institution theorists call “structured”. Such a proof
reveals bare connections between the relevant properties, stripped of accidental paraphernalia. For example, our proof does not employ the machinery of quantifier rank
and normal forms. It also applies straightforwardly to cases with empty sorts, withwhich the classical proof would struggle.
Thirdly, our proof applies directly to arbitrary signatures. The classical proof does
the job, too, but in a roundabout way (via finite reducts).
Finally, we believe immodestly that by elucidating the fine structure of gamesin the institutional framework we have made game methods available to institution
theorists.

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] M. Bidoit, R. Hennicker, and A. Kurz. Observational logic, constructor-based
logic, and their duality. Theor. Comput. Sci., 3(298), 2003.
[3] A. Church. A Formulation of the Simple Theory of Types. J. Symb. Log.,
5(2):56–68, 1940.
[4] M. Codescu and D. Găină. Birkhoff completeness in institutions. Logica Universalis, 2(2):277–309, 2008.
[5] R. Diaconescu. Institution-independent Ultraproducts. Fundamenta Informaticæ, 55(3-4):321–348, 2003.
[6] R. Diaconescu. An Institution-independent proof of Craig Interpolation Theorem. Studia Logica, 77(1):59–79, 2004.
[7] R. Diaconescu. Elementary Diagrams in Institutions. J. Log. Comput., 14(5):651–
674, 2004.
[8] R. Diaconescu. Proof systems for institutional logic. Journal of Logic and Computation, 16(3):339–357, 2006.
[9] R. Diaconescu. Institution-independent Model Theory. Studies in Universal Logic.
Birkhäuser, Basel, 1 edition, 2008.
[10] R. Diaconescu. Quasi-varieties and initial semantics for hybridized institutions.
Journal of Logic and Computation, 26(3):855–891, 2016.
[11] R. Diaconescu and M. Petria. Saturated models in institutions. Arch. Math.
Log., 49(6):693–723, 2010.
[12] 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.

23

[13] D. Găină. Interpolation in logics with constructors. Theoretical Computer Science, 474:46–59, 2013.
[14] D. Găină. Forcing, Downward Löwenheim-Skolem and Omitting Types Theorems, Institutionally. Logica Universalis, 8(3-4):469–498, 2014.
[15] D. Găină. Birkhoff style calculi for hybrid logics. Formal Aspects of Computing,29(5):805–832, 2017.
[16] D. Găină. Downward Löwenheim-Skolem Theorem and interpolation in logics
with constructors. Journal of Logic and Computation, 27(6):1717–1752, 2017.
[17] D. Găină. Forcing and Calculi for Hybrid Logics. Journal of the Association for
Computing Machinery, 67(4):1–55, 2020.
[18] D. Găină and K. Futatsugi. Initial semantics in logics with constructors. Journalof Logic and Computation, 25(1):95–116, 2015.
[19] D. Găină and M. Petria. Completeness by forcing. Journal of Logic and Computation, 20(6):1165–1186, 2010.
[20] D. Găină and A. Popescu. An Institution-independent Generalization of Tarski’s
Elementary Chain Theorem. Journal of Logic and Computation, 16(6):713–735,
2006.
[21] D. Găină and A. Popescu. An Institution-Independent Proof of Robinson Consistency Theorem. Studia Logica, 85(1):41–73, 2007.
[22] D. Găină, I. Tutu, 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.
[23] 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.
[24] L. Henkin. Completeness in the theory of types. J. Symb. Log., 15(2):81–91,
1950.
[25] K. J. J. Hintikka. Distributive normal forms in the calculus of predicates. Acta
Philos. Fenn., 6:71, 1953.
[26] W. Hodges. Model theory, volume 42 of Encyclopedia of mathematics and its
applications. Cambridge University Press, 1993.
[27] M. Petria and R. Diaconescu. Abstract Beth definability in institutions. Journalof Symbolic Logic, 71(3):1002–1028, 2006.

24

[28] D. Sannella and A. Tarlecki, editors. Recent Trends in Data Type Specification,
5th Workshop on Abstract Data Types, volume 332 of Lecture Notes in Computer
Science. Springer, 1987.
[29] S. G. Simpson. Subsystems of second order arithmetic. Perspectives in Logic.
Cambridge University Press, Cambridge; Association for Symbolic Logic, Poughkeepsie, NY, second edition, 2009.
[30] A. Tarlecki. On the Existence of Free Models in Abstract Algebraic Institutions.
Theoretical Computer Science, 37:269–304, 1985.
[31] A. Tarlecki. Bits and pieces of the theory of institutions. In K. Drosten, H. Ehrich,
M. Gogolla, and U. W. Lipeck, editors, Proceedings of the 4st Workshop on
Abstract Data Type, 1986. University of Braunschweig, Germany, 1986.
[32] A. Tarlecki. Quasi-varieties in Abstract Algebraic Institutions. Journal of Computer and System Sciences, 33(3):333–360, 1986.
[33] W. Thomas. On the Ehrenfeucht-Fraı̈ssé game in theoretical computer science.
In J. J. Gaudel M.C., editor, TAPSOFT’93: Theory and Practice of Software
Development. CAAP 1993, volume 668 of Lecture Notes in Computer Science.
Springer, Berlin, Heidelberg, 1993.

25