Proof We prove sufficiency of 2-homogeneity first. Let $\mathfrak M$ be any 2-homogeneous binary model. We are going to define another model $\mathfrak N$ and a 2-isomorphism I between them. $\mathfrak N$ will be finite when $\mathfrak M$ is so. Then we show that $\mathfrak N$ is transitive.

Some notation and terminology. The variables of FO2 will be denoted by $x,y$ . By the 2-type of $a,b\in \mathfrak M$ we understand the set of FO2-formulas $\rho (x,y)$ that are true for $a,b$ in $\mathfrak M$ . Formally,

$$ \begin{align*} \textsf{Type}(a,b,\mathfrak M) = \{\rho(x,y)\in FO2 : \mathfrak M\models\rho[a,b]\} . \end{align*} $$

Now we define

• $[a] = \{ b\in M : \textsf {Type}(b,b,\mathfrak M)=\textsf {Type}(a,a,\mathfrak M)\}$ ,

• $[a,b] = \textsf {Type}(a,b,\mathfrak M)$ ,

• $\textsf {Types}([a],[b]) = \{ [p,q] : p\in [a],\ q\in [b]\}$ .

We call the elements of $\{[a] : a\in M\}$ 1-Types. Note that $[a]$ is a subset of the model, while $[p,q]$ is a set of FO2-formulas.

The type $[p,q]$ determines $[q,p]$ , and we call the latter the converse type ${[p,q]}^{\smallsmile }$ of $[p,q]$ . Taking the converse is a bijection between $\textsf {Types}([a],[b])$ and $\textsf {Types}([b],[a])$ . We call a type $[p,q]$ symmetric when $[p,q]=[q,p]$ , otherwise we call it asymmetric. There is a unique element of $\textsf {Types}([a],[a])$ which contains $x=y$ , we call this the identity type on $[a]$ , it is denoted by $\textsf {id}({a})$ , and it is symmetric. A non-identity type is a type which is not an identity type.

We begin the definition of $\mathfrak N$ . A group $\mathfrak G=\langle G,+\rangle $ will be used in the definition of $\mathfrak N$ . That is, G is the universe of the group, and $+$ is its group-operation. The identity element (or zero-element) of $+$ is denoted by $0$ , and the inverse of an element a is denoted by $-a$ . We call a group asymmetric when its zero-element is its only element of order 2, i.e., when $x+x=0$ implies $x=0$ in it. Let $\mathfrak G$ be any commutative asymmetric group of size at least twice that of $\textsf {Types}([a],[b])$ for any $a,b\in M$ , i.e.,

(g1) $$ \begin{align} |G| \ge 2\cdot|\textsf{Types}([a],[b])|\quad\text{ for all } a,b\in M . \end{align} $$

There is such a $\mathfrak G$ because for each odd number n the group $\mathbb {Z}_n$ of integers smaller than n and with addition modulo n is asymmetric, and then one can construct an asymmetric group of any infinite size by taking an elementary submodel of a sufficiently big ultraproduct of the $\mathbb {Z}_n$ with odd n. Equivalently, use the upward Löwenheim–Skolem–Tarski Theorem [Reference Chang and Keisler9, Corollaries 2.1.5 and 2.1.6].

The universe N of $\mathfrak N$ is defined as

$$ \begin{align*} N = \{ ([a],g) : a\in M, g\in G\} . \end{align*} $$

Clearly, if M is finite, then G can be chosen to be finite, and then N is finite.

For the definition of the relations of $\mathfrak N$ , let $\lambda =\langle \lambda _{[a],[b]} : a,b\in M\rangle $ be a system of functions mapping G to the types of $\mathfrak M$ that satisfies the following conditions for all $a,b\in M$ . We will write $\lambda _{a,b}$ in place of $\lambda _{[a],[b]}$ , for easier readability.

• $\lambda _{a,b}:G\to \textsf {Types}([a],[b])$ is surjective,

• $\lambda _{a,b}(g) = {\lambda _{b,a}(-g)}^{\smallsmile }\quad \mbox {and}\quad \lambda _{a,a}(0)=\textsf {id}({a})$ .

There is such a system $\lambda $ of functions, because of the following. When $[a]\ne [b]$ , take any surjective $\lambda _{b,a}:G\to \textsf {Types}([b],[a])$ , there is such since $|G|\ge |\textsf {Types}([b],[a])|$ by (g1), then define $\lambda _{a,b}(g)={\lambda _{b,a}(-g)}^{\smallsmile }$ , and this is also surjective because $\textsf {Types}([a],[b])=\{ {-t}^{\smallsmile } : t\in \textsf {Types}([b],[a])\}$ .

Assume now $[a]=[b]$ . Since G is asymmetric, there is a set $P\subseteq G$ such that P, $-P=\{ -g : g\in P\}$ together with $\{ 0\}$ form a partition of G. Let S denote the set of all non-identity symmetric types in $T=\textsf {Types}([a],[a])$ , then there is a set $A\subseteq T$ such that A, ${A}^{\smallsmile }=\{{t}^{\smallsmile } : t\in A\}$ , and S together with $\{\textsf {id}({a})\}$ form a partition of T. Now, $|P|\ge |S\cup A|$ by (g1), so there is a surjective function $L:P\to (S\cup A)$ . Define now $\lambda _{a,a}(g)=L(g)$ for $g\in P$ , $\lambda _{a,a}(g)={L(-g)}^{\smallsmile }$ for $g\in -P$ , and $\lambda _{a,a}(0)=\textsf {id}({a})$ . This function satisfies the required conditions (because both functions of taking inverse in the group and taking converse in the types are their own inverses).

Now we define, for all $a,b\in M$ and $g,h\in G$

$$ \begin{align*} \textsf{ty}(([a],g),([b],h)) = \lambda_{a,b}(h-g), \end{align*} $$

where $h-g$ denotes $h+-g$ as usual in group theory. Then $\textsf {ty}$ maps $N\times N$ to the types of $\mathfrak M$ . Let $\textsf {R}$ be an arbitrary binary relation symbol in the language of $\mathfrak M$ . The binary relation $R^{\mathfrak N}$ belonging to $\textsf {R}$ in $\mathfrak N$ is defined as

$$ \begin{align*} R^{\mathfrak N} = \{ (p,q)\in N\times N : \textsf{R}(x,y)\in\textsf{ty}(p,q)\} . \end{align*} $$

By this, the model $\mathfrak N$ has been defined.

Next, we exhibit a 2-isomorphism between $\mathfrak M$ and $\mathfrak N$ . We define $I\subseteq (M\times N)\cup (M^2\times N^2)$ by requiring for all $a,b\in M$ and $p,q\in N$ that

• $\langle a,p\rangle \in I\quad \text { iff }\quad p=([a],g)$ for some g,

• $\langle (a,b),(p,q)\rangle \in I\quad \text { iff }\quad [a,b]=\textsf {ty}(p,q)$ .

We now show that I is a 2-isomorphism between $\mathfrak M$ and $\mathfrak N$ . From the conditions defining a 2-isomorphism, I clearly satisfies (i) by its very definition.

Next we show that the restriction property (iii) holds for I. Assume that $\langle (a,b),(p,q)\rangle \in I$ . This means that $[a,b]=\textsf {ty}(p,q)$ . Assume that $p=([c],g)$ and $q=([d],h)$ . From the definition of $\textsf {ty}(p,q)$ it is clear that $\textsf {ty}(p,q)\in \textsf {Types}([c],[d])$ . Thus, $[a,b]=[r,s]$ for some $r\in [c]$ and $s\in [d]$ . But this implies that $[a]=[r]=[c]$ and $[b]=[s]=[d]$ , hence $\langle a,p\rangle \in I$ and $\langle b,q\rangle \in I$ .

We show that I satisfies local isomorphism property (ii). Let $\textsf {R}$ be an arbitrary relation symbol in the language of $\mathfrak M$ . Assume that $\langle a,p\rangle \in I$ . Then $p=([a],g)$ for some g by the definition of I, and we have to show that $R(p,p)$ holds in $\mathfrak N$ iff $R(a,a)$ holds in $\mathfrak M$ . By definition, $R(p,p)$ holds in $\mathfrak N$ iff $\textsf {R}(x,y)\in \textsf {ty}(p,p)=\lambda _{a,a}(g-g)=\lambda _{a,a}(0)=\textsf {id}({a})$ , and $\textsf {R}(x,y)\in \textsf {id}({a})$ iff $R(a,a)$ holds in $\mathfrak M$ , by the definition of $\textsf {id}({a})$ .

Assume that $\langle (a,b),(p,q)\rangle \in I$ . Then $[a,b]=\textsf {ty}(p,q)$ by the definition of I. We have to show that each of $a=b, R(a,a)$ , $R(a,b)$ , $R(b,a)$ , and $R(b,b)$ holds in $\mathfrak M$ iff the same holds in $\mathfrak N$ for $p,q$ in place of $a,b$ . Assume that $p=([c],g)$ and $q=([d],h)$ , then $\textsf {ty}(p,q)=\lambda _{c,d}(h-g)$ by the definition of $\textsf {ty}$ . Now, $a=b$ iff $x=y\in [a,b]=\textsf {ty}(p,q)=\lambda _{c,d}(h-g)$ , and $x=y\in \lambda _{c,d}(h-g)$ iff ( $[c]=[d]$ and $h-g=0$ ) iff $p=q$ . Similarly, $R(a,b)$ iff $\textsf {R}(x,y)\in [a,b]=\textsf {ty}(p,q)$ iff $R(p,q)$ , by the definition of $\mathfrak N$ . For the next case, we want to show that

(t1) $$ \begin{align} \textsf{ty}(p,q)={\textsf{ty}(q,p)}^{\smallsmile}. \end{align} $$

Indeed, $\textsf {ty}(p,q)=\lambda _{c,d}(h-g)={\lambda _{d,c}(g-h)}^{\smallsmile }={\textsf {ty}(q,p)}^{\smallsmile }$ , by the second condition that $\lambda $ has to satisfy. By this, (t1) is proved.

Now, $R(b,a)$ iff $\textsf {R}(x,y)\in [b,a]={[a,b]}^{\smallsmile }={\textsf {ty}(p,q)}^{\smallsmile }=\textsf {ty}(q,p)$ iff $R(q,p)$ . Finally, $R(a,a)$ iff $R(p,p)$ and $R(b,b)$ iff $R(q,q)$ hold by the first case of (ii), since we have already shown the restriction property (iii). Thus, $\langle (a,b),(p,q)\rangle $ indeed specifies a partial isomorphism between $\mathfrak M$ restricted to $\{ a,b\}$ and $\mathfrak N$ restricted to $\{ p,q\}$ .

We check the back-and-forth property (iv) for I. To check the first part, notice that to any $a\in M$ there is at least one $p=([a],g)$ in N, because G is nonempty. The second part is clear, since no 1-Type $[a]$ is empty. To check the third and fourth parts of the back-and-forth property, assume that $\langle a,p\rangle \in I$ with $p=([a],g)$ . Let $b\in M$ be arbitrary. We have to find a $q\in N$ such that $[a,b]=\textsf {ty}(p,q)$ . By surjectivity of $\lambda _{a,b}$ , there is $f\in G$ with $[a,b]=\lambda _{a,b}(f)$ . Let $q=(b,f+g)$ . Then $\textsf {ty}(p,q)=\lambda _{a,b}(f+g-g)=\lambda _{a,b}(f)=[a,b]$ and we are done with the third part. Let now $q=([b],h)\in N$ be arbitrary. We have to find $c\in M$ such that $[a,c]=\textsf {ty}(p,q)$ . Now, $\textsf {ty}(p,q)\in \textsf {Types}([a],[b])$ which means that there are $a'\in [a]$ and $b'\in [b]$ such that $\textsf {ty}(p,q)=\textsf {Type}(a',b',\mathfrak M)$ . By $a'\in [a]$ we have $\textsf {Type}(a',a',\mathfrak M)=\textsf {Type}(a,a,\mathfrak M)$ , so by 2-homogeneity of $\mathfrak M$ there is $c\in M$ such that $\textsf {Type}(a,c,\mathfrak M)=\textsf {Type}(a',b',\mathfrak M)$ and this shows that $[a,c]=\textsf {ty}(p,q)$ . So, (iv) holds for I. We have seen that I is a 2-isomorphism between $\mathfrak M$ and $\mathfrak N$ .

We show that $\mathfrak N$ is transitive. We have to show that if $p,q\in N$ are of the same type in $\mathfrak N$ , then there is an automorphism of $\mathfrak N$ that takes p to q. Assume that $p=([a],g)$ and $q=([b],h)$ . Then $\langle a,p\rangle \in I$ and $\langle b,q\rangle \in I$ , by the definition of I. Since I is a 2-isomorphism between $\mathfrak M$ and $\mathfrak N$ , we get that the same formulas hold in $\mathfrak N$ for p as in $\mathfrak M$ for a, and the same for q and b. Hence, a and b are of the same type in $\mathfrak M$ (since p and q are of the same type in $\mathfrak N$ ). It is easy to check that a and b are of the same type in $\mathfrak N$ iff $[a]=[b]$ . Let $k=-g+h$ and define $\alpha :N\to N$ by

$$ \begin{align*} \alpha(([c],f)) = ([c],f+k)\quad\text{ for all } c\in M \text{ and } f\in G. \end{align*} $$

Now, $\alpha (p)=q$ by $[a]=[b]$ and $h=g+k$ . We show that $\alpha $ is an automorphism of $\mathfrak N$ . First, $\alpha $ is a permutation of N because $\mathfrak G$ is a group. Let $\textsf {R}$ be a binary relation symbol in the language of $\mathfrak N$ , and let $r=([c],i)\in N$ , $s=([d],j)\in N$ . Now, $R(r,s)$ holds in $\mathfrak N$ iff $\textsf {R}(x,y)\in \textsf {ty}(r,s)=\lambda _{c,d}(j-i)$ . Similarly, $R(\alpha (r),\alpha (s))$ holds in $\mathfrak N$ iff $\textsf {R}(x,y)\in \textsf {ty}(\alpha (r),\alpha (s))=\lambda _{c,d}(j+k-(i+k))$ . However, $j-i=j+k-(i+k)$ because $\mathfrak G$ is commutative. Thus, $\alpha $ is indeed an automorphism, and we are done with showing that $\mathfrak N$ is transitive.

We have seen that $\mathfrak N$ is transitive, and this finishes the proof of one direction of Theorem 1.

The other direction of Theorem 1, necessity of 2-homogeneity, follows from the facts that a transitive model is always 2-homogeneous, and 2-isomorphisms preserve being 2-homogeneous. In more detail, assume that I is a 2-isomorphism between $\mathfrak M$ and the transitive $\mathfrak N$ . We have to show that $\mathfrak M$ is 2-homogeneous. Let $a,b,c\in M$ be such that $[a]=[b]$ . By the back-and-forth property in the definition of a 2-isomorphism, there are $a',b',c'\in N$ such that $\langle a,a'\rangle $ , $\langle b,b'\rangle $ , $\langle (a,c),(a',c')\rangle $ are all in I. Then $\textsf {Type}(a',a',\mathfrak N)=\textsf {Type}(b',b',\mathfrak N)$ since I is a 2-isomorphism and $[a]=[b]$ . Since $\mathfrak N$ is 2-transitive, there is an automorphism of $\mathfrak N$ that takes $a'$ to $b'$ . Let $d'$ be the image of $c'$ under this automorphism. Then $\textsf {Type}(a',c',\mathfrak N)=\textsf {Type}(b',d',\mathfrak N)$ since automorphisms preserve 2-types of elements. By the back-and-forth property of I again, there is $d\in M$ such that $\langle (b,d),(b',d')\rangle \in I$ . Then $\textsf {Type}(a,c,\mathfrak M)=\textsf {Type}(a',c',\mathfrak N)=\textsf {Type}(b',d',\mathfrak N)=\textsf { Type}(b,d,\mathfrak M)$ and we are done.⊣

Proof For the definition of an $\omega $ -saturated model see, e.g., [Reference Chang and Keisler9]. First we prove

(S) $$ \begin{align} \mathfrak M \text{ is } \omega\text{-saturated implies that } \mathfrak M \text{ is 2-homogeneous.} \end{align} $$

Assume that $\mathfrak M$ is $\omega $ -saturated. Let $a,b,c\in M$ be such that $\textsf {Type}(a,a,\mathfrak M)=\textsf {Type}(b,b,\mathfrak M)$ . Let $Y=\{ b\}\subseteq M$ and let $\Gamma (x) = \{ \rho (x,b)\in FO2 : \rho (c,a)\text { in }\mathfrak M\}$ . Then $\Gamma (x)$ is a set of formulas in the language of $\langle \mathfrak M,b\rangle $ . We show that it is consistent with the theory of $\langle \mathfrak M,b\rangle $ . Let $\Delta $ be a finite subset of $\Gamma (x)$ , let $\delta (y)$ denote the formula $\exists x\bigwedge \Delta [b/y]$ that we get from $\exists x\bigwedge \Delta $ by replacing b everywhere with y. Then $\mathfrak M\models \delta (a)$ by the definition of $\Gamma (x)$ , and so $\mathfrak M\models \delta (b)$ since $a,b$ have the same 1-Type in $\mathfrak M$ . But $\mathfrak M\models \delta (b)$ means that $\langle \mathfrak M, b\rangle \models \exists x\bigwedge \Delta $ that shows that $\Delta $ is consistent with the theory of $\langle {\mathfrak M},b\rangle $ . Since $\Delta $ is an arbitrary finite subset of $\Gamma (x)$ , this means that $\Gamma (x)$ is consistent with the theory of $\langle \mathfrak M,b\rangle $ . Since $\mathfrak M$ is $\omega $ -saturated, then there is $d\in M$ for which $\Gamma (d)$ holds. This means that $\textsf {Type}(a,c,\mathfrak M)=\textsf {Type}(b,d,\mathfrak M)$ and we are done with showing (S).

Now, Theorem 2 follows from (S) and Theorem 1 by using that each infinite model is elementarily equivalent—hence 2-equivalent—with an $\omega $ -saturated one (see [Reference Chang and Keisler9, Lemma 5.1.4]), that each finite model is $\omega $ -saturated (see [Reference Chang and Keisler9, Proposition 5.1.2]), and that the model $\mathfrak N$ in the proof of Theorem 1 can be constructed to be finite whenever $\mathfrak M$ is finite. ⊣

Proof The binary model $\mathfrak M$ has 45 elements and 4 basic relations $S,G,R,B$ . Let $\langle \mathbb {Z}_5,+\rangle $ denote the group of non-negative numbers smaller than 5 with addition modulo 5, and let $9=\{ 0,1,\dots ,8\}$ denote the set of non-negative integers smaller than 9. We define

$$ \begin{align*} M = 5\times 9 . \end{align*} $$

• Let $s,g$ be permutations of 9 defined, in cycle form, as $s=(012)(345)(678)$  and  $g=(136)(147)(258)$ ,

• and let $r,b\subseteq 9\times 9$ be defined as $r=\{0,3,6\}\times \{0,1,2\}\cup \{1,4,7\}\times \{3,4,5\}\cup \{2,5,8\}\times \{6,7,8\}$ and $b=\{0,4,8\}\times \{0,5,7\}\cup \{1,5,6\}\times \{1,3,8\}\cup \{2,3,7\}\times \{2,4,6\}$ .

Now, the basic relations of $\mathfrak M$ are defined as

• $S=\{\langle (i,j),(i,s(j))\rangle : i\in 5, j\in 9\}$ ,

• $G=\{\langle (i,j),(i,g(j))\rangle : i\in 5, j\in 9\}$ ,

• $R=\{\langle (i,j),(i+1,k)\rangle : i\in 5, (j,k)\in r\}$ ,

• $B=\{\langle (i,j),(i+2,k)\rangle : i\in 5, (j,k)\in b\}$ .

We show that $\mathfrak M$ is not 3-equivalent to any transitive model. Let us call a model 3,1-transitive when any two elements of the same 3-type can be taken to each other by an automorphism. A transitive model $\mathfrak N$ is 3,1-transitive, because let $a,b\in N$ have the same 3-types, then they have the same types in $\mathfrak N$ , therefore there is an automorphism taking a to b, by transitivity of $\mathfrak N$ . Thus, it is enough to show that if $\mathfrak M$ is 3-equivalent to $\mathfrak N$ then $\mathfrak N$ is not 3,1-transitive.

Assume that $\mathfrak M$ is 3-equivalent to $\mathfrak N$ . For a first-order formula $\rho (x,y)$ with free variables among $x,y$ let $\rho (\mathfrak M)$ denote the relation that $\rho $ defines in $\mathfrak M$ , i.e., $\rho (\mathfrak M)=\{(a,b) : \mathfrak M\models \rho [a,b]\}$ . Let $\mathfrak {R}\mathfrak {a}(\mathfrak M)$ be the relation algebra of FO3-definable binary relations of $\mathfrak M$ , i.e., the universe of $\mathfrak {R}\mathfrak {a}(\mathfrak M)$ is $\{ \rho {(\mathfrak M)} : \rho (x,y)\in FO3\}$ , and the operations of $\mathfrak {R}\mathfrak {a}(\mathfrak M)$ are the operations of taking union, converse, and relation composition of binary relations together with the (base-sensitive) operations of taking complement in $M\times M$ and the identity constant $\{ (u,u) : u\in M\}$ on M. Let $\mathfrak {R}\mathfrak {a}(\mathfrak N)$ denote the similar algebra of FO3-definable binary relations of $\mathfrak N$ . We show the following:

(1) $$ \begin{align} \mathfrak M \text{ is 3-equivalent to } \mathfrak N \text{ implies that } \mathfrak{R}\mathfrak{a}(\mathfrak M) \text{ is isomorphic to } \mathfrak{R}\mathfrak{a}(\mathfrak N). \end{align} $$

Indeed, it is easy to check that the relation $\{(\rho (\mathfrak M),\rho (\mathfrak N)) : \rho (x,y)\in FO3\}$ is an isomorphism between $\mathfrak {R}\mathfrak {a}(\mathfrak M)$ and $\mathfrak {R}\mathfrak {a}(\mathfrak N)$ when $\mathfrak M$ is 3-equivalent to $\mathfrak N$ .

A base-automorphism of $\mathfrak {R}\mathfrak {a}(\mathfrak N)$ is a permutation $\alpha $ of N that leaves all elements of $\mathfrak {R}\mathfrak {a}(\mathfrak N)$ fixed when taking Z to $\{ (\alpha (u),\alpha (v)) : (u,v)\in Z\}$ . Now, $\mathfrak {R}\mathfrak {a}(\mathfrak N)$ is called c-permutational iff any element of N can be taken to any other by a base-automorphism.

(2) $$ \begin{align} \mathfrak N \text{ is 3,1-transitive implies that } \mathfrak{R}\mathfrak{a}(\mathfrak N) \text{ is c-permutational}. \end{align} $$

To check (2), notice first that all elements in $\mathfrak N$ have the same 3-type. This is so because $\mathfrak M$ is such and this property can be expressed with FO3 formulas $\{\exists x\rho (x,x)\to \forall x\rho (x,x) : \rho (x,y)\in FO3\}$ . Therefore, $\mathfrak N$ is 3,1-transitive means that each element of N can be taken to any other element of N by an automorphism of $\mathfrak N$ . Finally, an automorphism $\alpha $ of $\mathfrak N$ is a base-automorphism of $\mathfrak {R}\mathfrak {a}(\mathfrak N)$ and we are done.

From now on, we will use [Reference Andréka, Düntsch and Németi2].

(3) $$ \begin{align} \mathfrak{R}\mathfrak{a}(\mathfrak M) \text{ is the algebra } \mathfrak A \text{ defined in [2, section 2]}. \end{align} $$

Indeed, it can be checked that the basic relations $S,G,R,B$ of $\mathfrak M$ coincide with the relations $s,g,r_0,b_0$ in [Reference Andréka, Düntsch and Németi2, Section 2]. It is stated in [Reference Andréka, Düntsch and Németi2, p. 375, line 16] that $\mathfrak A$ is generated by these four elements, so each element of A is FO3-definable in $\mathfrak M$ . In the other direction, it is a theorem of relation algebra theory that all FO3-definable elements of $\mathfrak M$ can be generated from the basic relations of $\mathfrak M$ with the operations of $\mathfrak {R}\mathfrak {a}(\mathfrak M)$ , see e.g., [Reference Tarski and Givant32, Section 3.9] or [Reference Hirsch and Hodkinson15, Theorem 3.32]. Thus, the elements of A are exactly the FO3-definable binary relations of $\mathfrak M$ and we are done.

In the proof of [Reference Andréka, Düntsch and Németi2, Theorem 1] it is proved that $\mathfrak A$ is not isomorphic to any c-permutational algebra, and so $\mathfrak N$ cannot be 3,1-permutational by (1) and (2). The proof of Theorem 3 is complete. ⊣

Proof of Lemma 1 Let $\textsf {Th}, \Sigma , \mathfrak M, R$ be as in the first two sentences of the statement of Lemma 1. Assume that R cuts a 2-type in $\mathfrak M$ . By using this, we are going to define a relation S distinct from R which also satisfies $\Sigma $ in $\mathfrak M$ , contradicting that $\Sigma $ is an implicit definition.

Assume that

(a) $$ \begin{align} R(a,b) \text{ and not } R(c,d) \text{ in } \mathfrak M \end{align} $$

for some $a,b,c,d$ such that $\textsf {Type}(a,b,\mathfrak M)=\textsf {Type}(c,d,\mathfrak M)$ . Let $T=\textsf {Type}(a,b,\mathfrak M)$  and

$$ \begin{align*} t = \{ (m,n)\in M\times M : \textsf{Type}(m,n,\mathfrak M)=T\} . \end{align*} $$

We note that

(d) $$ \begin{align} T \text{ is not an identity type} \end{align} $$

by (a) and $\mathfrak M$ being transitive: assume $(m,m)\in t$ for some $m\in M$ , then $(a,a), (c,c)\in t$ and there is an automorphism $\alpha $ of $\mathfrak M$ taking a to c. Hence $(a,a)\in R$ iff $(c,c)\in R$ because automorphisms preserve meanings of formulas and hence they leave solutions of implicit definitions fixed. However, $a=b$ and $c=d$ by t being an identity type, contradicting (a).

For a binary relation Z, let $Z^{-1}=\{ (v,u) : (u,v)\in Z\}$ denote its inverse, Z is symmetric means that $Z=Z^{-1}$ . We define $S\subseteq M\times M$ as follows. If $T\ne {T}^{\smallsmile }$ or $t\cap R$ is symmetric, then we define S by “interchanging” $t\cap R$ with $t\setminus R$ , i.e.,

$$ \begin{align*} S=(R\setminus t)\cup (t\setminus R) . \end{align*} $$

If $T={T}^{\smallsmile }$ and $t\cap R$ is not symmetric then S is defined by “interchanging” $(t\cap R\setminus R^{-1})$ with its inverse $(t\cap R^{-1}\setminus R)$ , i.e.,

$$ \begin{align*} S=(R\setminus [t\cap R\setminus R^{-1}])\cup (t\cap R^{-1}\setminus R) . \end{align*} $$

Then S is distinct from R by $t\cap R$ being nonempty in the first case, and by $(t\cap R\setminus R^{-1})\cup (t\cap R^{-1}\setminus R)$ being nonempty in the second case. However,

(s) $$ \begin{align} S \text{ and } R \text{ differ only inside } t, \end{align} $$

that is, $[R(m,n) \text { iff } S(m,n)]$ for all $(m,n)\in M\times M\setminus t$ . We are going to show that $\langle \mathfrak M,S\rangle \models \Sigma $ . We define $J\subseteq (M\times M)\cup (M^2\times M^2)$ by requiring for all $m,n,p,q\in M$ that

• $\langle m,p\rangle \in J\quad \text {iff}\quad \textsf {Type}(m,m,\mathfrak M)=\textsf {Type}(p,p,\mathfrak M)$ ,

• $\langle (m,n),(p,q)\rangle \in J\quad \text {iff}\quad \textsf {Type}(m,n,\mathfrak M)=\textsf {Type}(p,q,\mathfrak M)$ and $[(m,n)\in R\leftrightarrow (p,q)\in S)]$ and $[(n,m)\in R\leftrightarrow (q,p)\in S)]$ .

We now show that J is a 2-isomorphism between $\langle \mathfrak M,R\rangle $ and $\langle \mathfrak M,S\rangle $ . We check properties (i)–(iv) in the definition of a 2-isomorphism. (i) is satisfied by the definition of J. Restriction property (iii) is satisfied, because if $\textsf {Type}(a,b,\mathfrak M)=\textsf {Type}(p,q,\mathfrak M)$ then $\textsf {Type}(a,a,\mathfrak M)=\textsf {Type}(b,b,\mathfrak M)$ and $\textsf {Type}(p,p,\mathfrak M)=\textsf { Type}(q,q,\mathfrak M)$ .

Checking local isomorphism property (ii): Assume $\langle (m,n),(p,q)\rangle \in J$ . Then J is a local isomorphism with respect to the language of $\mathfrak M$ by $\textsf {Type}(m,n,\mathfrak M)=\textsf {Type}(p,q,\mathfrak M)$ . We now check local isomorphism with respect to the new relation symbol $\textsf {R}$ . Indeed, $R(m,m)$ iff $S(p,p)$ holds because $R(m,m)$ iff $R(p,p)$ by the restriction property, and $R(p,p)$ iff $S(p,p)$ by (s) and (d). We have $R(m,n)$ iff $S(p,q)$ and $R(n,m)$ iff $S(q,p)$ by the definition of J. Thus property (ii) holds.

Checking back-and-forth property (iv): The first line is satisfied by $\langle a,a\rangle \in J$ for all $a\in M$ . For checking the second line, let $m,n,m'\in M$ , $\langle m,n\rangle \in J$ . Let $\alpha $ be an automorphism of $\mathfrak M$ that takes m to n. There is such an $\alpha $ because $\langle m,n\rangle \in J$ and $\mathfrak M$ is transitive.

Assume that $\textsf {Type}(m,m',\mathfrak M)\notin \{ T,{T}^{\smallsmile }\}$ . Let $n'=\alpha (m')$ . Then $\textsf {Type}(n,n',\mathfrak M)=\textsf {Type}(m,m',\mathfrak M)\notin \{ T,{T}^{\smallsmile }\}$ , because automorphisms do not change 2-types. By (s) then $R(e,f)$ iff $S(e,f)$ for all $(e,f)$ in $\{(m,m'),(m',m), (n,n'),(n',n)\}$ , thus $\langle (m,m'),(n,n')\rangle \in J$ by the definition of J.

Assume now that $\textsf {Type}(m,m',\mathfrak M)=T$ and $T\ne {T}^{\smallsmile }$ or $t\cap R$ is symmetric. If $R(m,m')$ , then let $\beta $ be an automorphism that takes c to n and let $n'=\beta (d)$ . Then $(n,n')\in (t\setminus R)$ by (a), so $(n,n')\in S$ by the definition of S. Assume $T\ne {T}^{\smallsmile }$ , then $(m',m)\in R$ iff $(n',n)\in S$ by (s). Assume that $T={T}^{\smallsmile }$ and $t\cap R$ is symmetric. Then $t\cap R^{-1}$ is also symmetric, hence $(m',m)\in R$ and $(n',n)\notin R$ , so $(n',n)\in S$ . Thus $\langle (m,m'),(n,n')\rangle \in J$ . If not $R(m,m')$ , then let $\beta $ be an automorphism that takes a to n and let $n'=\beta (b)$ . From here on, the argument showing $\langle (m,m'),(n,n')\rangle \in J$ is completely analogous to the previous case.

Assume now that $\textsf {Type}(m,m',\mathfrak M)=T={T}^{\smallsmile }$ and $t\cap R$ is not symmetric, say, $(e,f)\in t\cap R\setminus R^{-1}$ . If $(m,m')\in (R\cap R^{-1})$ then let $n'=\alpha (m')$ . Then $(n,n')\in (R\cap R^{-1})$ by $\alpha (R)=R$ and so $\alpha (R^{-1})=R^{-1}$ . Also, $(n,n')\in S\cap S^{-1}$ in this case, by the definition of S. Hence $\langle (m,m'),(n,n')\rangle \in J$ . The case $(m,m')\notin (R\cup R^{-1})$ is completely analogous. Assume $(m,m')\in R\setminus R^{-1}$ . Let $\beta $ be an automorphism taking f to n, and let $n'=\beta (e)$ . Then $(n,n')\in R^{-1}\setminus R$ , so $(n,n')\in S\setminus S^{-1}$ by the definition of S, and so $\langle (m,m'),(n,n')\rangle \in J$ by the definition of J. The case $(m,m')\in R^{-1}\setminus R$ is completely analogous.

The case when $\textsf {Type}(m,m',\mathfrak M)={T}^{\smallsmile }$ can be proved in a completely analogous way. By this, checking the second line is finished. The third line of (iv) follows in our case from the second one by noticing that J is symmetric both in $M\times M$ and in $M^2\times M^2$ .

Thus J is a 2-isomorphism between $\langle \mathfrak M,R\rangle $ and $\langle \mathfrak M,S\rangle $ , so $\langle \mathfrak M,S\rangle \models \Sigma $ . Thus both R and the distinct S satisfy $\Sigma $ , this contradicts $\Sigma $ being an implicit definition. The proof of Lemma 1 is complete. ⊣

Proof of Lemma 2 Clearly, (i) implies (ii) and (ii) implies (iii). To show that (iii) implies (i), assume that (i) does not hold, we will infer the negation of (iii).

We will refer to the negation of (i) just as “ $\textsf {R}$ is not 2-definable”. Thus we want to show that there is a model $\langle \mathfrak M,R\rangle \models \textsf {Th}\cup \Sigma $ such that $\mathfrak M$ is 2-homogeneous and R cuts a 2-type in $\mathfrak M$ .

By a 2-partition we understand a system $\langle \pi _i : i\le n\rangle $ of FO2-formulas in the language of $\textsf {Th}$ such that $\textsf {Th}\cup \Sigma \models (\bigvee \{ \pi _i : i\le n\}\land \bigwedge \{ \lnot (\pi _i\land \pi _j) : i<j\le n\}$ . We say that $\textsf {R}$ cannot cut $\pi $ when $\textsf {Th}\cup \Sigma \models \forall x,y(\pi (x,y)\to \textsf {R}(x,y))\lor (\forall x,y(\pi (x,y)\to \lnot \textsf {R}(x,y))$ . We say that $\textsf {R}$ cannot cut into the 2-partition $\langle \pi _i : i\le n\rangle $ when $\textsf {R}$ cannot cut any $\pi _i$ for $i\le n$ . We will use the following statement

(L1) $$ \begin{align} \textsf{R} \text{ is 2-definable}\quad \text{iff}\quad \text{there is a 2-partition } \textsf{R} \text{ cannot cut into}. \end{align} $$

Indeed, if $\textsf {R}$ is definable by the FO2-formula $\rho (x,y)$ , then $\textsf {R}$ cannot cut into $\langle \rho , \lnot \rho \rangle $ . In the other direction, assume that $\textsf {R}$ cannot cut into $\langle \pi _i : i\le n\rangle $ . Let us treat natural numbers in von Neumann’s sense, i.e., each natural number n is the set of smaller natural numbers: $n=\{ i\in \omega : i<n\}$ . For $J\subseteq n$ let $\pi (J)=\bigwedge \{ \pi _j : j\in J\}\land \bigwedge \{\lnot \pi _j : j\in n\setminus J\}$ . By the assumption that $\textsf {R}$ cannot cut into $\langle \pi _i : i<n\rangle $ we have that $\textsf {R}$ is a union of some $\pi _i$ s in each model of $\textsf {Th}\cup \Sigma $ , i.e., $\textsf {Th}\cup \Sigma \models \bigvee \{ \textsf {R}(x,y)\leftrightarrow \pi (J) : J\subseteq n\}$ . Since $\Sigma $ is an implicit definition, we have $\textsf {Th}\cup \Sigma (\textsf {R})\cup \Sigma (\textsf {R}')\models \textsf {R}(x,y)\leftrightarrow \textsf {R}'(x,y)$ where $\textsf {R}'$ is a brand new binary relation symbol, so by compactness

(s) $$ \begin{align} \textsf{Th}\cup\Sigma_0(\textsf{R})\cup\Sigma_0(\textsf{R}')\models \textsf{R}(x,y)\leftrightarrow \textsf{R}'(x,y)\quad\text{for some finite } \Sigma_0\subseteq\Sigma. \end{align} $$

Let $\sigma (\textsf {R})=\bigwedge \Sigma _0(\textsf {R})$ for a $\Sigma _0$ satisfying (s). Assume that $\langle \mathfrak M,R\rangle \models \textsf {Th}\cup \Sigma $ . Then there is a unique J such that $\mathfrak M\models \textsf {R}(x,y)\leftrightarrow \pi (J)$ , since $\pi (J)\land \pi (K)$ is inconsistent for distinct J and K. By $\langle \mathfrak M,R\rangle \models \Sigma $ and $\Sigma _0\subseteq \Sigma $ we have that $\mathfrak M\models \sigma (\pi (J))$ . Also, $\mathfrak M\models \sigma (\pi (K))$ is not true for $K\ne J$ by (s) since $\pi (J)$ and $\pi (K)$ define distinct relations in $\mathfrak M$ . This shows that $\textsf {Th}\cup \Sigma \models \textsf {R}(x,y)\leftrightarrow \bigwedge \{\sigma (\pi (J))\to \pi (J) : J\subseteq n\}$ , and this is a 2-definition for $\textsf {R}$ . Statement (L1) has been proved.

To prove (iii), we construct a 2-type T in the language of $\textsf {Th}$ such that the set

(L2) $$ \begin{align} \textsf{Th}\cup\Sigma\cup \{ \textsf{R}(x,y), \lnot \textsf{R}(z,v)\}\cup T(x,y)\cup T(z,v) \end{align} $$

of FO-formulas is consistent. That T is a 2-type means that either $\rho \in T$ or $\lnot \rho \in T$ for all FO2-formulas $\rho $ in the language of $\textsf {Th}$ . We say that a set of open FO-formulas is consistent when there is a model and an evaluation that make the set true. Equivalently, one can consider the free variables in the set to be constants, we will use this second option.

Let $\tau $ be an FO2-formula in the language of $\textsf {Th}$ . A 2-partition of $\tau $ is a system $\langle \pi _i : i\le n\rangle $ such that $\textsf {Th}\cup \Sigma \models (\tau \leftrightarrow \bigvee \{\pi _i : i<n\})\land \bigwedge \{\lnot (\pi _i\land \pi _j) : i<j<n\}$ . Let T be a set of FO2 formulas in the language of $\textsf {Th}$ . We say that T is good iff $\textsf {R}$ can cut into any 2-partition of $\bigwedge T_0$ , for all finite subsets $T_0$ of T. Clearly, a directed union of good sets is a good set again, so there is a maximal one among the good sets by Zorn’s lemma. We will show that any maximal good set is a 2-type and that the set in (L2) with any good T is consistent. We begin with this second statement.

Assume that T is good and let $T_0\subseteq T$ be finite. Then $\textsf {R}$ can cut into any 2-partition of $\bigwedge T_0$ , in particular $\textsf {R}$ can cut into $\bigwedge T_0$ . This means that there is a model of $\textsf {Th}\cup \Sigma \cup \{ \textsf {R}(x,y), \lnot \textsf {R}(z,v)\}\cup T_0(x,y)\cup T_0(z,v)$ . By compactness, the set in (L2) is consistent.

To show that a maximal good T is a 2-type, let T be any good set and let $\rho $ be any FO2 formula in the language of $\textsf {Th}$ . We show that either $T\cup \{\rho \}$ is good or $T\cup \{\lnot \rho \}$ is good. Assume that neither of $T\cup \{\rho \}$ and $T\cup \{\lnot \rho \}$ is good. Then there are finite subsets $T_0, T_1$ of T and 2-partitions $\pi =\langle \pi _i : i\le n\rangle $ of $\rho \land \bigwedge T_0$ and $\delta =\langle \delta _j : j<m\rangle $ of $\lnot \rho \land \bigwedge T_1$ such that $\textsf {R}$ cannot cut into either of these two partitions. We can now combine $\pi $ and $\delta $ to form a 2-partition $\sigma $ of $\bigwedge (T_0\cup T_1)$ by letting the members of the partition $\sigma $ be $\pi _i\land \bigwedge T_1$ and $\delta _j\land \bigwedge T_0$ for $i<n, j<m$ . Clearly, $\textsf {R}$ cannot cut into $\sigma $ by our assumption that $\textsf {R}$ cannot cut into either of $\pi $ and $\delta $ ; this contradicts to T being good. With this, we have proved that any maximal good T is a 2-type.

By the above, we now have a 2-type T such that the set $\Delta =\textsf {Th}\cup \Sigma \cup \{ \textsf {R}(x,y), \lnot \textsf {R}(z,v)\}\cup T(x,y)\cup T(z,v)$ is consistent. Let then $\langle \mathfrak M,R\rangle $ be any $\omega $ -saturated model of $\Delta $ . Then $\mathfrak M$ is also $\omega $ -saturated, and so it is 2-homogeneous by statement (S) in the proof of Theorem 2. Also, $\textsf {R}$ cuts the 2-type T in $\mathfrak M$ by $\langle \mathfrak M,R\rangle \models \Delta $ . We derived the negation of (iii) from the negation of (i), and this finishes the proof of Lemma 2. ⊣

Proof of Theorem 4 Assume that $\Sigma $ is a strong implicit definition of $\textsf {R}$ w.r.t. $\textsf {Th}$ . We are going to show that $\Sigma $ can be made explicit, i.e., $\textsf {R}$ has an explicit definition over $\textsf {Th}$ that uses only two variables.

Take any 2-homogeneous model $\mathfrak M$ of $\textsf {Th}$ , and let $\overline {\mathfrak M}$ be a transitive model with I a 2-isomorphism between $\mathfrak M$ and $\overline {\mathfrak M}$ . There are such $\overline {\mathfrak M}$ and I by Theorem 1. $\overline {\mathfrak M}$ is a model of $\textsf {Th}$ because 2-isomorphic models satisfy the same FO2-formulas. Since $\Sigma $ is a strong implicit definition of $\textsf {R}$ in $\textsf {Th}$ , there is $\overline {R}$ which satisfies $\Sigma $ in $\overline {\mathfrak M}$ , i.e., $\langle \overline {\mathfrak M},\overline {R}\rangle \models \Sigma $ .

Since $\overline {\mathfrak M}$ is transitive, $\overline {R}$ does not cut 2-types in $\overline {\mathfrak M}$ , by Lemma 1. We now “transfer” $\overline {R}$ to the model $\mathfrak M$ by the following definition: take any pair $(a,b)$ in $\mathfrak M$ . We define R so that this pair is related by R if and only if there is a pair of the same type in $\overline {\mathfrak M}$ which is related by $\overline {R}$ . Formally:

$$ \begin{align*} R = \{(a,b)\in M\times M : \exists c,d[\overline{R}(c,d)\text{ and }\textsf{Type}(a,b,\mathfrak M)=\textsf{Type}(c,d,\overline{\mathfrak M})\} . \end{align*} $$

We now show that with this definition, the 2-isomorphism I between $\mathfrak M$ and $\overline {\mathfrak M}$ remains a 2-isomorphism between $\langle \mathfrak M,R\rangle $ and $\langle \overline {\mathfrak M},\overline {R}\rangle $ . Since I is a 2-isomorphism between $\mathfrak M$ and $\overline {\mathfrak M}$ , it satisfies conditions (i), (iii), and (iv) in the definition of a 2-isomorphism, and it also satisfies condition (ii) for atomic formulas other than $R(v,z)$ . Therefore, we only have to show that if $\langle (a,b), (a',b')\rangle \in I$ , then $R(a,b)$ iff $\overline {R}(a',b')$ .

Assume that $\langle (a,b), (a',b')\rangle \in I$ . If $R(a,b)$ , then there are $c,d\in \overline {\mathfrak M}$ such that $\overline {R}(c,d)$ and $\textsf {Type}(c,d,\overline {\mathfrak M})=\textsf {Type}(a,b,\mathfrak M)$ , by the definition of R. The 2-type of $(a',b')$ is also the same as that of $(a,b)$ , since they are I-related by assumption. Hence the 2-type of $(c,d)$ is the same as that of $(a',b')$ (since they both equal the 2-type of $(a,b)$ ). By $\overline {R}(c,d)$ we now get $\overline {R}(a',b')$ , since we have seen that $\overline {R}$ does not distinguish elements of the same 2-type. In the other direction, assume that $\overline {R}(a',b')$ . Since $(a,b)$ is I-related to $(a',b')$ , their 2-types equal, hence $R(a,b)$ by the definition of R. By this, we have seen that I is a 2-isomorphism between the expanded models $\langle \mathfrak M,R\rangle $ and $\langle \overline {\mathfrak M},\overline {R}\rangle $ . Since the latter is a model of $\Sigma $ , we get that $\langle \mathfrak M,R\rangle $ is a model of $\Sigma $ , too. By its definition, R does not cut 2-types in $\mathfrak M$ .

Since $\Sigma $ is a weak definition over $\textsf {Th}$ and the 2-homogeneous $\mathfrak M\models \textsf {Th}$ was chosen arbitrarily, we get that R does not cut 2-types in $\mathfrak M$ whenever $\langle \mathfrak M,R\rangle \models \textsf {Th}\cup \Sigma $ and $\mathfrak M$ is 2-homogeneous. Thus, $\Sigma $ can be made explicit in $\textsf {Th}$ , by Lemma 2 and this finishes the proof of Theorem 4. ⊣

Question 1. Does $L^2_{\infty ,\omega }$ have weak Beth definability property?