The Invariance Modality

Abstract

In Gerla (1987), G. Gerla introduced the so-called transformational semantics for predicate modal logic and considered in particular semantic frameworks given by a classical model endowed with a group of automorphisms, where a boxed formula is true iff it holds invariantly (i.e. it remains true whenever an automorphism is applied to the individuals it is talking about). With this interpretation, de dicto modalities collapse, but de re modalities remain quite informative. We handle the axiomatization problem of such modal structures, by employing classic model-theoretic tools (iterated ultrapowers and double chains).

1 Introduction

The distinction between de re and de dicto modalities is a classical topic in the philosophical investigations concerning modal predicate logic. We recall that de dicto modalities are represented by formulae of the kind $\Box \phi$ where $\phi$ is a sentence; in case $\phi$ has free variables, the modality $\Box \phi$ is called a de re modality. Whereas de dicto modalities can be interpreted without referring to some kind of “essential” properties of individuals, the same does not apply to de re modalities: that’s why de re modalities appear to be compromised with some sort of essentialist metaphysics.

However, looking at mathematical contexts, as pointed out in Gerla (1987), de re modalities assume a rather natural interpretation: $\Box \phi (x)$ means that x enjoys the property $\phi$ in a way that is invariant with respect to transformations that might be applied to x. In particular, when transformations are applied inside a given domain, only de re modalities survive and de dicto modalities collapse (i.e. it happens exactly the contrary of what anti-essentialist philosophy would consider to be desirable). To this aim, in Gerla (1987) a suitable invariance logic is introduced and shown to be recursively axiomatizable (via a reduction to two-sorted predicate logic). In this paper, we show that the axiomatization implicitly suggested in Gerla (1987) is complete: we consider both the case where transformations are assumed to be functions and the case where transformations are assumed to be bijections (we use the name of ‘transformation semantics’ for the former case and of ‘invariance semantics’ for the latter).¹

The main results of this paper were already contained in Ghilardi (1990); they were listed in Ghilardi and Meloni (1991) (together with other results in modal predicate logic), but never published. The proofs presented here are a deep revisitation and clarification of the original proofs in Ghilardi (1990). The completeness results in Sect. 6.4 can be obtained also via the saturated/special models technique of Ghilardi (1992); however the technique presented here does not depend on cardinal arithmetics and has the merit of reinterpreting classical model theoretic methods in the specific context of modal logic.

2 Preliminaries

We consider a first order modal language $\mathcal L$ with identity: terms are restricted to be only variables, whereas formulae are built up from atoms using the connectives $\lnot , \bot , \vee , \Box$ and the quantifier $\exists$ (further connectives $\wedge , \rightarrow ,\Diamond$ and the quantifier $\forall$ are defined in the standard way).

We shall use languages expanded with constants (called parameters) to introduce our semantic notions; parameters are taken from a set specified in the context. If we are given a function $\mu$ acting on the set of parameters, we use the notation $\phi [\mu ]$ to mean the formula obtained from $\phi$ by replacing every parameter a occurring in it by $\mu (a)$. When we speak of $\mathcal L$-sentences, $\mathcal L$-formulae, etc. we mean sentences, formulae, etc. without parameters; on the contrary, when we speak of sentences, formulae, etc. parameters are allowed to occur.

We fix for the whole paper an $\mathcal L-theory$ T, i.e. a set of $\mathcal L$-sentences. Our calculus has modus ponens (from $\phi$ and $\phi \rightarrow \psi$ infer $\psi$) and necessitation (from $\phi$ infer $\Box \phi$) as rules; as axioms we take an axiomatic base for first order classical logic with identity, the $\mathcal L$-sentences from T, the S4-axiom schemata

$$\begin{aligned} \Box (\phi \rightarrow \psi )\rightarrow (\Box \phi \rightarrow \Box \psi ), ~~~~~~\Box \phi \rightarrow \phi , ~~~~~~\Box \phi \rightarrow \Box \Box \phi \end{aligned}$$

(6.1)

and the further schema

$$\begin{aligned} \phi \rightarrow \Box \phi \qquad \qquad {(dDC)} \end{aligned}$$

restricted to $\mathcal L$-sentences. Such a schema is called the de dicto collapse schema. We write $\vdash _T \phi$ or $T\vdash \phi$ to mean that $\phi$ has a derivation in this calculus. We assume that our T is consistent, i.e. that $T\not \vdash \bot$.

Notice that our calculus does not give rise to a logic, according to the standard definition of a modal predicate logic Gabbay et al. (2009), Braüner and Ghilardi (2007), because it is not closed under uniform substitution: in fact, the schema (dDC) is not assumed to hold in case $\phi$ contains free variables. In addition, notice also that when we expand the language with parameters, the schema (dDC) does not apply to sentences containing parameters, but only to sentences in the original language $\mathcal L$.²

An immediate consequence of the de dicto collapse schema is that the standard form of the deduction theorem holds:

Proposition 6.1

Let $\psi$ be an $\mathcal L$-sentence and $\phi$ be an arbitrary formula; we have that $T\cup \{\psi \}\vdash \phi$ holds iff $T\vdash \psi \rightarrow \phi$ holds.

As a corollary, we can prove a Lindenbaum Lemma (T is said to be maximal iff either $T\vdash \psi$ or $T\vdash \lnot \psi$ holds for every $\mathcal L$-sentence $\psi$):

Lemma 6.1

Our consistent $\mathcal L$-theory T can be extended to a maximal consistent $\mathcal L$-theory in the same language $\mathcal L$.

2.1 Transformational and Invariance Models

A modal transformational model (or just a transformational model) for $\mathcal L$ is a triple $\mathfrak M=(M,\mathcal {I}, E)$, where $(M, \mathcal {I})$ is a Tarski structure for the first-order language $\mathcal L$ and E is a set of functions from M into M closed under composition and containing the identity function; a modal invariance model (or just an invariance model) is a modal transformation model $\mathfrak M=(M,\mathcal {I}, E)$ such that all functions in E are bijective.

Sentences in the expanded language $\mathcal L\cup M$ (containing a parameter name for each element of M) are evaluated inductively in a modal transformation model $\mathfrak M=(M,\mathcal {I}, E)$ as follows:

• (i) $\mathfrak M\models P(a_1, \dots , a_n)$ iff $(a_1,\dots , a_n)\in \mathcal {I}(P)$ (for every n-ary predicate symbol P from $\mathcal L$);

• (ii) $\mathfrak M\models a_1= a_2$ iff $a_1$ is equal to $a_2$;

• (iii) $\mathfrak M\not \models \bot$;

• (iv) $\mathfrak M\models \lnot \phi$ iff $\mathfrak M\not \models \phi$;

• (v) $\mathfrak M\models \phi _1\vee \phi _2$ iff ($\mathfrak M\models \phi _1$ or $\mathfrak M\models \phi _2$);

• (vi) $\mathfrak M\models \exists x \phi$ iff there is some $a\in M$ s.t. $\mathfrak M\models \phi (a/x)$.

• (vii) $\mathfrak M\models \Box \phi$ iff for all $\mu \in E$, $\mathfrak M\models \phi [\mu ]$.

$\mathfrak M$ is said to be a modal transformation model of the $\mathcal L$-theory T iff we have

• (o) $\mathfrak M\models \phi$ for every $\mathcal L$-sentence $\phi \in T$.

The following soundness property is easily established by induction on the proof witnessing $\vdash _T \phi$:

Proposition 6.2

Take an $\mathcal L$-formula $\phi (x_1, \dots , x_n)$ whose free variables are among $x_1, \dots , x_n$ and suppose that $\vdash _T \phi$; then for every modal transformational model $\mathfrak M=(M,\mathcal {I}, E)$ of T, for every $a_1,\dots , a_n\in M$ we have that $\mathfrak M\models \phi (a_1 \dots , a_n)$.

Notice that we use the notation $\phi (x_1, \dots , x_n)$ to express that $\phi$ contains free variables among $x_1, \dots , x_n$ and the notation $\phi (a_1, \dots , a_n)$ for the formula obtained from $\phi$ by replacing $x_i$ by $a_i$ (for $i=1,\dots , n$). When we use such notation, the $x_1, \dots , x_n$ are assumed to be distinct, whereas the $a_1, \dots , a_n$ may not be distinct. To have a more compact notation, we may use underlined letters for tuples of unspecified length: then $\phi (\underline{a})$ means the sentence obtained from $\phi (\underline{x})$ by replacing componentwise the tuple of variables $\underline{x}$ by the tuple of parameters $\underline{a}$ (the latter is supposed to be of equal length as $\underline{x}$).

In the definition of a modal transformation model, we took E to be just a set of endofunctions. One may wonder whether we can ask more for them: the answer is ‘yes’ in case we suitably enrich out theory T. In fact, if we take as further axioms for T the universal closure of the $\mathcal L$-formulae

$$\begin{aligned} A\rightarrow \Box A \end{aligned}$$

(6.2)

where A is atomic, then because of (o) and (vii), all functions in E are forced to be homomorphisms; to force them to be embeddings (in the standard model-theoretic sense Chang and Keisler 1990), it is sufficient to put in T the universal closure of all the $\mathcal L$-formulae of the kind

$$\begin{aligned} L\rightarrow \Box L \end{aligned}$$

(6.3)

where L is a literal (i.e. an atom or the negation of an atom).

We did not consider function symbols in our language $\mathcal L$ for simplicity; however, an n-ary function symbol h can be represented via an $n+1$-ary predicate symbol $P_h$ via existence and uniqueness axioms; assuming (6.2) for atoms rooted at $P_h$, restricts all $f\in E$ to be h-homomorphisms in the algebraic sense.

In general, a modal collapse axiom

$$\begin{aligned} \theta \rightarrow \Box \theta \end{aligned}$$

(6.4)

expresses the fact that $\theta$ is an invariant with respect to the class of endomorphisms considered in E. More information on connections between the collapse of modalities and model-theoretic notions is available in Gerla and Vaccaro (1984).

3 Classical Models and Ultrapowers

A classical model is a pair $\mathcal M=(M,\models _{\mathcal M})$, where M is a set and $\models _{\mathcal M}$ is a set of sentences in the expanded language $\mathcal L\cup M$ satisfying the condition (o) and the conditions (ii)-(vi) above (we usually write $\models _{\mathcal M} \phi$ as $\mathcal M\models \phi$).

Thus a classical model is in fact nothing but a model (in the classical sense) for our calculus rewritten in (non modal) first-order logic as follows. We let $\mathcal L_{ext}$ be the first order language obtained by expanding $\mathcal L$ by an extra predicate symbol $P_{\Box \phi }$ for every boxed $\mathcal L$-formula $\Box \phi$ (the arity of $P_{\Box \phi }$ is the number of free variables occurring in $\phi$); similarly, we let $T_{ext}$ be the first-order theory having as axioms all the $\mathcal L_{ext}$-formulae $\theta$ such that, replacing in $\theta$ the subformulae of the kind $P_{\Box \phi }(\underline{t})$ by $\Box \phi (\underline{t})$, one obtains an $\mathcal L$-formula provable in T (here $\underline{t}$ is a tuple of variables matching the length of the tuple of free variables of $\phi$). Then a classical model in the above sense is just a first-order $\mathcal L_{ext}$-structure which is a model of $T_{ext}$ according to Tarski semantics. Once we view classical models in this sense, it is clear that we can apply to them standard model-theoretic constructions (we shall be interested in particular into ultrapowers and chain limits).

Given two classical models $\mathcal M=(M,\models _{\mathcal M})$ and $\mathcal N=(N,\models _{\mathcal N})$, an elementary morphism among them is a map $\mu :M\longrightarrow N$ among the support sets satisfying the condition

$$\begin{aligned} \mathcal M\models \phi \qquad \Rightarrow \qquad \mathcal N\models \phi [\mu ] \end{aligned}$$

(6.5)

for all $\mathcal L\cup M$-sentences $\phi$.

A modal morphism among $\mathcal M=(M,\models _{\mathcal M})$ and $\mathcal N=(M,\models _{\mathcal M})$ is a map $\mu :M\longrightarrow N$ among the support sets satisfying the condition

$$\begin{aligned} \mathcal M\models \Box \phi \qquad \Rightarrow \qquad \mathcal N\models \phi [\mu ] \end{aligned}$$

(6.6)

for all $\mathcal L\cup M$-sentences $\phi$. Notice that modal morphisms need not be injective, unlike elementary morphisms.³

It is useful to extend the notion of a modal morphisms to subsets of classical models. Suppose that we are given two classical models $\mathcal M=(M,\models _{\mathcal M})$, $\mathcal N=(N,\models _{\mathcal N})$ and a subset $A\subseteq M$; a partial modal morphism of domain A is a map $\mu :A\longrightarrow N$ satisfying (6.6) for all $\mathcal L\cup A$-sentences $\phi$ (a partial modal morphism is usually indicated as $\mu : A \longrightarrow \mathcal N$, leaving $\mathcal M$ as understood). Modal (partial) morphisms are coloured in red in the diagrams below in the digital version of the book.

Given an ultrafilter D (on any set of indices) and a classical model $\mathcal M$, we can form the ultrapower $\Pi _D \mathcal M$ of $\mathcal M$ (as an $\mathcal L_{ext}$-structure) in the standard way Chang and Keisler (1990); we recall also that we have a canonical elementary morphism $\iota _D: \mathcal M\longrightarrow \Pi _D \mathcal M$.

We shall make extensive use of $\Box$-ultrafilters, which are defined as follows. Take a classical model $\mathcal M$ and consider the set $I_\mathcal M$ formed by the $\mathcal L\cup M$-sentences $\phi$ such that $\mathcal M\models \Box \phi$. A $\Box$-ultrafilter over $\mathcal M$ is any ultrafilter extending the finite intersections closed family given by the subsets of $I_\mathcal M$ of the kind $\downarrow \phi =\{ \psi \in I_\mathcal M\mid T\vdash \psi \rightarrow \phi \}$, varying $\phi$ in $I_\mathcal M$.

The following Lemma explains a typical use of $\Box$-ultrafilters:

Lemma 6.2

Let $\mathcal M=(M,\models _{\mathcal M})$, $\mathcal N=(N,\models _{\mathcal N})$ be classical models and let $A\subseteq M$ be a subset of M. Suppose we are given a partial modal morphism $\nu : A\longrightarrow \mathcal N$ and a $\Box$-ultrafilter D over $\mathcal M$. Then $\nu$ can be extended to a full modal morphism into $\Pi _D \mathcal N$, in the sense that there exists a modal morphism $\bar{\nu }:\mathcal M\longrightarrow \Pi _D \mathcal N$ such that $\bar{\nu }(a)= \iota _D(\nu (a))$ holds for all $a\in A$.

Proof

For every $\phi \in I_\mathcal M$, we define a map $h_\phi : M\longrightarrow N$ in the following way. Let $\underline{b}$ be the parameters from M occurring in $\phi$: suppose that we have $\underline{b}= \underline{a}, \underline{b}'$, where the $\underline{b}'$ are the (distinct) elements from $\underline{b}$ not belonging to A. We have $\mathcal M\models \Box \phi (\underline{a},\underline{b}')$ by definition of $I_\mathcal M$; it follows that $\mathcal M\models \exists \underline{y}\Box \phi (\underline{a},\underline{y})$. Since $T\vdash \exists \underline{y}\Box \phi (\underline{a},\underline{y})\rightarrow \Box \exists \underline{y}\phi (\underline{a},\underline{y})$,⁴ we get that $\mathcal M\models \Box \exists \underline{y}\phi (\underline{a},\underline{y})$ and also that there exist $\underline{c}$ in N such that $\mathcal N\models \phi (\nu (\underline{a}),\underline{c})$, because $\nu$ is modal. We take $h_\phi : M\longrightarrow N$ to be any extension of the partial map sending d to $\nu (d)$ (for all $d\in A$) and the $\underline{b}'$ to the $\underline{c}$. As a consequence of this definition we have

$$\begin{aligned} \mathcal N\models \phi [h_\phi ],\qquad \mathrm{for~all~} \phi \in I_\mathcal M~. \end{aligned}$$

(6.7)

Let us now define $\bar{\nu }: \mathcal M\longrightarrow \Pi _D \mathcal N$ as the map sending $d\in M$ to the equivalence class of the $I_\mathcal M$-indexed tuple $\langle h_\phi (d)\rangle _\phi$. We need to prove that for every $\psi$ with parameters in $\mathcal M$, we have

$$ \mathcal M\models \Box \psi \quad \Rightarrow \quad \Pi _D\mathcal N\models \psi [\bar{\nu }]~~. $$

If $\mathcal M\models \Box \psi$, then $\psi \in I_\mathcal M$ and so, since $\downarrow \psi \in D$, it is sufficient to check that for every $\phi \in \, \downarrow \psi$ we have $\mathcal N\models \psi [h_\phi ]$. Now $\phi \in \, \downarrow \psi$ means that we have $\mathcal M\models \Box \phi$ (i.e. $\phi \in I_\mathcal M$) and $T\vdash \phi \rightarrow \psi$. Since $\mathcal N$ is a classical model of T and (6.7) holds, we get $\mathcal N\models \psi [h_\phi ]$, as wanted. $\dashv$

Corollary 6.1

Let $\mathcal M_0, \mathcal M, \mathcal N$ be classical models; suppose we are given an elementary morphism $\mu : \mathcal M_0 \longrightarrow \mathcal M$, a modal morphism $\nu : \mathcal M_0\longrightarrow \mathcal N$ and a $\Box$-ultrafilter D over $\mathcal M$. Then there exists a modal morphism $\bar{\nu }:\mathcal M\longrightarrow \Pi _D \mathcal N$ such that $\bar{\nu }\circ \mu = \iota _D\circ \nu$.

Proof

This is easily reduced to the previous lemma, considering that, up to an isomorphism, $\mu$ is an inclusion (because it is injective). $\dashv$

Recall the symmetry axiom schemata

$$\begin{aligned} \Diamond \Box \phi \rightarrow \phi ~~ \end{aligned}$$

(6.8)

which axiomatizes the modal logic S5, once added to the S4 axiom schemata (6.1). If our T is an extension of S5 (i.e. if it contains all the examples of the above schema (6.8)), a variant of Lemma 6.2 holds:

Lemma 6.3

Suppose that T is an extension of S5. Let $\mathcal M$, $\mathcal N$ be classical models and $A\subseteq N$ be a subset of N. Suppose we are given a partial modal morphism $\mu : A \longrightarrow \mathcal M$ and a $\Box$-ultrafilter D over $\mathcal M$. Then there exists a modal morphism $\theta :\mathcal M\longrightarrow \Pi _D \mathcal N$ such that $\theta (\mu (a))= \iota _D(a)$ for all $a\in A$.

Proof

Let us preliminarily check that the implication

$$\begin{aligned} \mathcal M\models \exists \underline{y}\Box \phi (\mu (\underline{a}),\underline{y})\quad \Rightarrow \quad \mathcal N\models \exists \underline{y}\phi (\underline{a},\underline{y}) \end{aligned}$$

(6.9)

holds for all $\phi (\underline{a}, \underline{y})$ with parameters $\underline{a}$ from A. To show this, assume that $\mathcal M\models \exists \underline{y}\Box \phi (\mu (\underline{a}),\underline{y})$; then (since $\mu$ is modal—by contraposition of the partial modal morphism definition) we have $\mathcal N\models \Diamond \exists \underline{y}\Box \phi (\underline{a},\underline{y})$ and also $\mathcal N\models \Diamond \Box \exists \underline{y}\phi (\underline{a},\underline{y})$. By the symmetry axiom (6.8), $\mathcal N\models \exists \underline{y}\phi (\underline{a},\underline{y})$ follows.

As a second observation, we notice that $\mu$ is injective: this is because T is an extension of S5 and the necessity of the difference is a theorem in quantified S5 (see Hughes and Cresswell 1968).

Now we can proceed similarly as in the proof of Lemma 6.2. For every $\phi \in I_\mathcal M$, we define a map $h_\phi : M\longrightarrow N$ in the following way. Let $\underline{b}$ be the parameters from M occurring in $\phi$; we can decompose $\underline{b}$ as $\underline{b}= \mu (\underline{a}), \underline{b}'$, where the $\underline{b}'$ are the (distinct) elements from $\underline{b}$ not belonging to $\mu (A)$. We have $\mathcal M\models \Box \phi (\mu (\underline{a}),\underline{b}')$ by definition of $I_\mathcal M$; it follows that $\mathcal M\models \exists \underline{y}\Box \phi (\mu (\underline{a}),\underline{y})$ and consequently $\mathcal N\models \exists \underline{y}\phi (\underline{a},\underline{y})$ by (6.9), so there are $\underline{c}\in N$ such that $\mathcal N\models \phi (\underline{a},\underline{c})$. We take $h_\phi : M\longrightarrow N$ to be any extension of the partial map sending $\mu (d)$ to d (for all $d\in A$) and the $\underline{b}'$ to the $\underline{c}$: this is possible because, as noticed above, $\mu$ is injective. As a consequence of this definition we have

$$\begin{aligned} \mathcal N\models \phi [h_\phi ],\qquad \mathrm{for~all~} \phi \in I_\mathcal M~. \end{aligned}$$

(6.10)

We finally define $\bar{\nu }: \mathcal M\longrightarrow \Pi _D \mathcal N$ as the map sending $d\in M$ to the equivalence class of the $I_\mathcal M$-indexed tuple $\langle h_\phi (d)\rangle _\phi$: the proof now continues as in Lemma 6.2. $\dashv$

Corollary 6.2

Suppose that T is an extension of S5. Let $\mathcal M_0$, $\mathcal M$, $\mathcal N$ be classical models. Suppose we are given a modal morphism $\mu : \mathcal M_0 \longrightarrow \mathcal M$, an elementary morphism $\nu : \mathcal M_0\longrightarrow \mathcal N$ and a $\Box$-ultrafilter D over $\mathcal M$. Then there exists a modal morphism $\theta :\mathcal M\longrightarrow \Pi _D \mathcal N$ such that $\theta \circ \mu = \iota _D\circ \nu$.

4 Strong Completeness Theorems

In this section, we prove our main results, namely that our transformational semantics is axiomatized by the de dicto collapse schema (together with S4 axiom schemata (6.1)) and that the addition of the symmetry axiom schema (6.8) axiomatizes modal invariance models.

Theorem 6.1

For a given sentence $\phi$, we have that if $T\not \vdash \phi$ then there is a transformational model $\mathfrak M$ of T such that $\mathfrak M\not \models \phi$.

Proof

We prove the theorem in the following equivalent form (the equivalence is guaranteed by Proposition 6.1 and by the Lindenbaum Lemma 6.1): if T is maximal consistent, then there is a transformational model for T.

Notice that to show the claim it is sufficient to produce a classical model $\mathcal M=(M,\models _{\mathcal M})$ for T satisfying the following additional condition for every $\mathcal L\cup M$-sentence $\phi$:

• (*) if $\mathcal M\not \models \Box \phi$, then there exists a modal endomorphism $\nu : \mathcal M\longrightarrow \mathcal M$ such that $\mathcal M\not \models \phi [\nu ]$.

In fact, once such a classical model is found, we can turn it into the transformational model $\mathfrak M= (M, \mathcal {I}, E)$, where E is the set of modal endomorphisms of $\mathcal M$ and $\mathcal {I}$ is the interpretation function mapping an n-ary predicate symbol P into the set of n-tuples $(a_1, \dots , a_n)\in M^n$ such that $\mathcal M\models P(a_1, \dots , a_n)$: an easy induction then proves a standard ’truth lemma’, namely that $\mathcal M\models \phi$ holds iff $\mathfrak M\models \phi$ holds for all $\mathcal L\cup M$-sentences $\phi$.

Thus we are left to the task of finding a classical model satisfying $(*)$ above for our maximal consistent T. We shall build $\mathcal M$ as a chain limit of ultrapowers.

We start with a classical model $\mathcal M_0$ having some saturation properties. In fact, we need a weaker variant of $\omega$-saturation, which we are going to explain. An n -ary type for T is a set of formulae $\tau (\underline{x})$ having at most the $\underline{x}$ as free variables (here $\underline{x}=x_1, \dots , x_n$) such that for every finite subset $\tau _0\subseteq \tau$, we have that $T\cup \{\exists \underline{x}\bigwedge \tau _0(\underline{x})\}$ is consistent. An n-ary type $\tau (\underline{x})$ is realized in a classical model $\mathcal M=(M,\models _{\mathcal M})$ iff there is a tuple $\underline{a}\in M^n$ such that we have $\mathcal M\models \theta (\underline{a})$ for every $\theta (\underline{x})\in \tau (\underline{x})$. Since T is maximal consistent, by a simple compactness argument, it is possible to show that there is a classical model $\mathcal M_0$ for T realizing all n-ary types for T (for all n). This $\mathcal M_0$ is the starting model of our chain.

Having already defined the classical model $\mathcal M_i$, we let $\mathcal M_{i+1}$ be $\Pi _{D_i} \mathcal M_i$, where $D_i$ is a $\Box$-ultrafilter of $\mathcal M_i$. Now let us take the limit $\mathcal M$ of the chain given by the $\mathcal M_i$ and the elementary embeddings $\iota _{D_i}$

$$\begin{aligned} \mathcal M_0 \buildrel {\iota _{D_0}}\over \longrightarrow \cdots \buildrel {\iota _{D_{i-1}}}\over \longrightarrow \mathcal M_i \buildrel {\iota _{D_i}}\over \longrightarrow \cdots \end{aligned}$$

(6.11)

We prove that $\mathcal M$ satisfies condition $(*)$. Let $\phi$ be a sentence with parameters from $\mathcal M$ such that $\mathcal M\not \models \Box \phi$. Let the parameters occurring in $\phi$ be $\underline{a}$ and let all of them be from a certain $\mathcal M_i$. We claim that the set of formulae

$$\begin{aligned} \{ \lnot \phi (\underline{x})\}\cup \{\theta (\underline{x})\,\vert \, \mathcal M\models \Box \theta (\underline{a})\} \end{aligned}$$

(6.12)

is a type. Otherwise there are formulae $\theta _1(\underline{x}), \dots , \theta _m(\underline{x})$ such that we have both $\mathcal M\models \bigwedge _{k=1}^m\Box \theta _k(\underline{a})$ and $T\cup \{\exists \underline{x}(\lnot \phi (\underline{x}) \wedge \bigwedge _{k=1}^m\theta _k(\underline{x})\}\vdash \bot$. By the deduction theorem (Proposition 6.1), classical validities, necessitation rule, the converse of the Barcan formula (available in quantified normal systems Hughes and Cresswell 1968) and the distribution axiom (6.1), we get $T\vdash \forall \underline{x}(\bigwedge _{k=1}^m \Box \theta _k(\underline{x}) \rightarrow \Box \phi (\underline{x}))$, contradicting $\mathcal M\models \bigwedge _{k=1}^m\Box \theta _k(\underline{a})$ and $\mathcal M\not \models \Box \phi (\underline{a})$.

Let the type (6.12) be realized by some tuple $\underline{b}$ from $\mathcal M_i$ (actually, there is such a tuple already in $\mathcal M_0$ by the above weak saturation property of $\mathcal M_0$). We let $A=\{\underline{a}\}$ and $\nu$ be the partial modal morphism $\nu : A\longrightarrow \mathcal M_i$ mapping the $\underline{a}$ to the $\underline{b}$. By Lemma 6.2, there is a modal morphism $\nu _i: \mathcal M_i\longrightarrow \mathcal M_{i+1}$ such that $\nu _i(\underline{a})=\iota _{D_i}(\nu (\underline{a}))=\iota _{D_i}(\underline{b})$.

If we now apply repeatedly Corollary 6.1, for all $j\ge i$, we can find modal morphisms $\nu _{j+1}$ such that $\nu _{j+1}\circ \iota _{D_j}= \iota _{D_{j+1}}\circ \nu _j$.

Putting all these $\nu _j$ together in the chain limit, we get a modal morphism $\nu : \mathcal M\longrightarrow \mathcal M$ which maps (the colimit equivalence class of) $\underline{a}$ into (the colimit equivalence class of) $\underline{b}$, so that we have $\mathcal M\not \models \phi [\nu ]$, as required. $\dashv$

4.1 Invariance Models

We now consider strong completeness for invariance models:

Theorem 6.2

Suppose that T is an extension of S5. For a given sentence $\phi$, we have that if $T\not \vdash \phi$ then there is an invariance model $\mathfrak M$ of T such that $\mathfrak M\not \models \phi$.

Proof

Again, we can freely suppose that T is maximal consistent and the theorem is proved if we find a classical model $\mathcal M=(M,\models _{\mathcal M})$ for T satisfying the following condition for every $\mathcal L\cup M$-sentence $\phi$:

• (**) if $\mathcal M\not \models \Box \phi$, then there exists a bijective modal endomorphism $\nu : \mathcal M\longrightarrow \mathcal M$ such that $\mathcal M\not \models \phi [\nu ]$.

Notice in fact that, if T is an extension of S5, the inverse of a bijective modal morphism is also a modal morphism. Thus, if $(**)$ holds, then we can turn the classical model $\mathcal M$ into the invariance model $\mathfrak M=(M, \mathcal {I}, E)$ by taking as E the set of bijective modal endomorphisms of $\mathcal M$ and by defining $\mathcal {I}$ as in the proof of Theorem 6.1.

To find a classical model satisfying $(**)$, we proceed as in the proof of Theorem 6.1: we first build the sufficiently saturated model $\mathcal M_0$, the chain of models (6.11) and its chain colimit $\mathcal M$. Also, given $\phi$ with parameters in $\mathcal M_i$ such that $\mathcal M_i\not \models \Box \phi$, we build a modal morphism $\nu _i: \mathcal M_i\longrightarrow \mathcal M_{i+1}$ such that $\mathcal M_{i+1}\not \models \phi [\nu _i]$. The question is now how to extend this modal morphism to a bijective modal morphism $\mathcal M\longrightarrow \mathcal M$. To this aim we shall use Corollary 6.2 and a double chain argument. Because of Corollary 6.2 we can in fact inductively define for every $j\ge i$ a modal morphism $\nu _{j+1}: \mathcal M_{j+1} \rightarrow \mathcal M_{j+2}$ so that we have $\nu _{j+1}\circ \nu _j= \iota _{D_{j+1}}\circ \iota _{D_j}$.

This equality holds for all $j\ge i$; thus, applying it to k and $k+1$, we get (for every $k\ge i$)

$$ \iota _{D_{k+2}}\circ \iota _{D_{k+1}}\circ \nu _k= \nu _{k+2}\circ \nu _{k+1}\circ \nu _k= \nu _{k+2}\circ \iota _{D_{k+1}}\circ \iota _{D_{k}} $$

This means that the family of modal morphisms $\{\nu _{i+2s}\}_{s\ge 0}$ determines the required modal morphism $\mathcal M\longrightarrow \mathcal M$ extending $\nu _i$: this morphism is bijective because its inverse is the modal morphism determined by the family of modal morphisms $\{\nu _{i+2s+1}\}_{s\ge 0}$. $\dashv$

5 Conclusions

We proved strong completeness theorems for transformational and invariance models. Such models are special cases of presheaf models, where the domain category of presheaves is a monoid (resp. a group). Presheaf models have been shown to be quite effective in proving the weakness of Kripke semantics in quantified modal logic (Ghilardi 1989, 1991), however a systematic semantic investigation on them (covering e.g. crucial topics like correspondence theory) still waits for substantial development.

Another potentially interesting (although difficult) research direction would be that of identifying classes of monoids and groups whose associated transformational and invariance models are sensible to a transparent modal axiomatization. Invariance theory is at the heart of mathematics in various areas and it would be nice if modal logic could contribute to it in some respect.