\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{Ehrenfeucht-Fraïssé games}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{model_theory}{}\paragraph*{{Model theory}}\label{model_theory}

[[!include model theory - contents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak
\noindent\hyperlink{backandforth_systems}{Back-and-forth systems}\dotfill \pageref*{backandforth_systems} \linebreak
\noindent\hyperlink{unnested_ehrenfeuchtfrass_games}{Unnested Ehrenfeucht-Fra\"i{}ss\'e{} games}\dotfill \pageref*{unnested_ehrenfeuchtfrass_games} \linebreak
\noindent\hyperlink{dynamic_ehrenfeuchtfrass_games}{Dynamic Ehrenfeucht-Fra\"i{}ss\'e{} games}\dotfill \pageref*{dynamic_ehrenfeuchtfrass_games} \linebreak
\noindent\hyperlink{backandforth_sequences}{Back-and-forth sequences}\dotfill \pageref*{backandforth_sequences} \linebreak
\noindent\hyperlink{use_in_infinitary_logic}{Use in infinitary logic}\dotfill \pageref*{use_in_infinitary_logic} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

\textbf{Ehrenfeucht-Fra\"i{}ss\'e{} games} are a technique in [[model theory]] for studying whether to structures are elementary equivalent. Variations can be used to study equivalence with respect to logics other than first-order logic.

The games are played by two players: the \emph{spoiler}, whose objective is to establish a difference between the two structures, and the \emph{duplicator}, whose objective is to show that the two structures are similar.

A game is played in turns for a number of rounds (in general an ordinal, but usually a finite number or $\omega$). In each round the spoiler picks an element of one of the structures and then the duplicator responds by picking an element of the other structure. At the end of the game they have together selected two sequences of equal length of elements of the two structures, and the duplicator wins if the sequences generate isomorphic substructures of the given structures. (See below for variations in the winning conditions.)

\hypertarget{definition}{}\subsection*{{Definition}}\label{definition}

We first define the \textbf{Ehrenfeucht-Fra\"i{}ss\'e{} game of length $\gamma$ on $\mathfrak{A}$ and $\mathfrak{B}$}, $EF_\gamma(\mathfrak{A},\mathfrak{B})$. It is a game of perfect information played as follows. The ordinal $\gamma$ is the length of the game, and at step $i\lt\gamma$, the spoiler chooses an element of either $\mathfrak{A}$ or $\mathfrak{B}$; then the duplicator chooses an element of the other structure. Between them they choose $a_i\in A$ and $b_i\in B$. At the end of the game we have a \textbf{play} which is a pair $(\bar a,\bar b)$ of sequences of length $\gamma$. We count this play as a \textbf{win for the duplicator} if there is an isomorphism $f :
\langle\bar a\rangle_{\mathfrak{A}} \to \langle\bar
b\rangle_{\mathfrak{B}}$ such that $f(a_i)=b_i$ for $i\lt\gamma$. (The notation $\langle\bar a\rangle_{\mathfrak{A}}$ denotes the substructure of $\mathfrak{A}$ generated by the sequence $\bar a$.)

An alternative way of phrasing the winning condition is to say that the play $(\bar a,\bar b)$ is a win for the duplicator if and only if $(\mathfrak{A},\bar a) \equiv_0 (\mathfrak{B},\bar b)$, i.e., the expansions of the two structures by the given sequences satisfy the same atomic (or the same quantifier-free) sentences.

\begin{example}
\label{DefEF}\hypertarget{DefEF}{}
We write $\mathfrak{A} \sim_\gamma \mathfrak{B}$ to mean that the duplicator has a winning strategy in the game $EF_\gamma(\mathfrak{A},\mathfrak{B})$.

\end{example}
It is easy to see that this is an equivalence relation on structures, and $\mathfrak{A} \sim_\gamma \mathfrak{B}$ always holds when $\mathfrak{A}$ and $\mathfrak{B}$ are isomorphic. Note the $EF_\gamma(\mathfrak{A},\mathfrak{B})$ is an infinite game if $\gamma\ge\omega$.

\hypertarget{backandforth_systems}{}\subsection*{{Back-and-forth systems}}\label{backandforth_systems}

For the game $EF_\omega(\mathfrak{A},\mathfrak{B})$ we have the following alternative characterization of $\mathfrak{A} \sim_\omega
\mathfrak{B}$.

A \textbf{back-and-forth system} from $\mathfrak{A}$ to $\mathfrak{B}$ is an inhabited set $I$ of pairs $(\bar a,\bar b)$ of equal length sequences from $\mathfrak{A}$ and $\mathfrak{B}$ such that

\begin{itemize}%
\item for every $(\bar a,\bar b)\in I$ we have $(\mathfrak{A},\bar a)
\equiv_0 (\mathfrak{B},\bar b)$, and


\item for every $(\bar a,\bar b)\in I$ and every $a\in A$, there is a $b\in B$ such that $(\bar a a, \bar b b)\in I$, and


\item for every $(\bar a,\bar b)\in I$ and every $b\in B$, there is an $a
\in A$ such that $(\bar a a, \bar b b)\in I$.



\end{itemize}
\begin{example}
\label{PropBF}\hypertarget{PropBF}{}
There is a back-and-forth system from $\mathfrak{A}$ to $\mathfrak{B}$ if and only if $\mathfrak{A} \sim_\omega \mathfrak{B}$.

\end{example}
For this reason we say that $\mathfrak{A}$ and $\mathfrak{B}$ are \textbf{back-and-forth equivalent} if and only if $\mathfrak{A} \sim_\omega
\mathfrak{B}$. (Other names for back-and-forth equivalence are partial isomorphism or potential isomorphism.)

\begin{example}
\label{ACFBF}\hypertarget{ACFBF}{}
Any two algebraically closed fields of equal characteristic and infinite transcendence degree over their respective prime subfields are back-and-forth equivalent. A back-and-forth system is in this case given by the pairs of generating sequences for isomorphic finitely generated subfields.

\end{example}
\begin{example}
\label{ThmCountableBF}\hypertarget{ThmCountableBF}{}
Suppose $\mathfrak{A}$ and $\mathfrak{B}$ are at most countable back-and-forth equivalent structures. Then $\mathfrak{A}$ and $\mathfrak{B}$ are isomorphic, and if the play $(\bar a,\bar b)$ is a win for the duplicator in $EF_\omega(\mathfrak{A},\mathfrak{B})$, then there is an isomorphism $f : \mathfrak{A} \to \mathfrak{B}$ with $f(a_i)=b_i$ for $i\lt\omega$.

\end{example}
\begin{example}
\label{CantorThm}\hypertarget{CantorThm}{}
\textbf{(Cantor's Theorem)} Any two countable [[DLO|dense linear orders without endpoints]] are isomorphic. A back-and-forth system is given by the pairs of finite sequences of isomorphic finite suborders.

\end{example}
\hypertarget{unnested_ehrenfeuchtfrass_games}{}\subsection*{{Unnested Ehrenfeucht-Fra\"i{}ss\'e{} games}}\label{unnested_ehrenfeuchtfrass_games}

One major application of Ehrenfeucht-Fra\"i{}ss\'e{} games is to study elementary equivalence. For languages without (non-constant) function symbols, however, we need a slight modification to the above definitions.

The \textbf{unnested Ehrenfeucht-Fra\"i{}ss\'e{} game of length $\gamma$ on $\mathfrak{A}$ and $\mathfrak{B}$}, $EF_\gamma[\mathfrak{A},\mathfrak{B}]$ is played exactly like $EF_\gamma(\mathfrak{A},\mathfrak{B})$, but a play $(\bar a,\bar b)$ counts as a \textbf{win for the duplicator} if and only $(\mathfrak{A},\bar
a)$ and $(\mathfrak{B},\bar b)$ satisfy the same \textbf{unnested} atomic formulas.

Recall that an \textbf{unnested atomic formula} for a first-order language of one of the following forms:

\begin{itemize}%
\item $x = y$ for variables $x$ and $y$,


\item $x = c$ for variable $x$ and constant symbol $c$,


\item $x = f(\bar y)$ for variables $x$ and $\bar y$ and function symbol $f$,


\item $R(\bar x)$ for variables $\bar x$ and relation symbol $R$.



\end{itemize}
Any atomic formula is equivalent to a $\Delta$-formula built from unnested atomic formulas (but the quantifier rank grows with the size of the involved terms).

\begin{example}
\label{DefEFunnested}\hypertarget{DefEFunnested}{}
We write $\mathfrak{A} \approx_\gamma \mathfrak{B}$ to mean that the duplicator has a winning strategy in the game $EF_\gamma[\mathfrak{A},\mathfrak{B}]$.

\end{example}
Note that $\mathfrak{A} \sim_\gamma \mathfrak{B}$ implies $\mathfrak{A} \approx_\gamma \mathfrak{B}$ and the converse holds whenever the language has no constant and function symbols (as in that case every atomic formula is automatically unnested).

The key reason to introduce the unnested formulas and games is the following theorem:

\begin{example}
\label{FraisseHintikka}\hypertarget{FraisseHintikka}{}
\textbf{(Fra\"i{}ss\'e{}-Hintikka theorem)} Suppose the language $L$ has finitely many symbols. Then we can effectively find for each $k,n\lt\omega$ a finite set $\Theta_{n,k}$ of unnested formulas in $n$ free variables of quantifier rank at most $k$, such that

\begin{itemize}%
\item for every $L$-structure $\mathfrak{A}$, all $k,n\lt\omega$, and all $n$-tuples $\bar a$ from $\mathfrak{A}$, there is exactly one formula $\theta$ in $\Theta_{n,k}$ with $(\mathfrak{A},\bar a)
\vDash \theta$,


\item for all $k,n\lt\omega$ and all $L$-structures $\mathfrak{A}$ and $\mathfrak{B}$ and corresponding $n$-tuples $\bar a$ and $\bar b$ we have $(\mathfrak{A},\bar a) \approx_k (\mathfrak{B},\bar b)$ if and only if there is $\theta\in\Theta_{n,k}$ satisfied by both $(\mathfrak{A},\bar a)$ and $(\mathfrak{B},\bar b)$,


\item for all $k,n\lt\omega$ it holds that every unnested formula in $n$ free variables of quantifier rank at most $k$ is equivalent to a disjunction of formulas in $\Theta_{n,k}$.



\end{itemize}
\end{example}
This appears as Theorem 3.3.2 in \hyperlink{Hodges93}{Hodges 93}.

\begin{example}
\label{FraisseTheorem}\hypertarget{FraisseTheorem}{}
\textbf{(Fra\"i{}ss\'e{}`s theorem)} Two structures $\mathfrak{A}$ and $\mathfrak{B}$ in a finite language are elementarily equivalent, $\mathfrak{A} \equiv \mathfrak{B}$, if and only if for every $k\lt\omega$, $\mathfrak{A} \approx_k \mathfrak{B}$.

\end{example}
\hypertarget{dynamic_ehrenfeuchtfrass_games}{}\subsection*{{Dynamic Ehrenfeucht-Fra\"i{}ss\'e{} games}}\label{dynamic_ehrenfeuchtfrass_games}

The condition occurring in Fra\"i{}ss\'e{}`s theorem, that for every $k\lt\omega$, $\mathfrak{A} \approx_k \mathfrak{B}$, is nicely captured by another variation of either the ordinary or the unnested Ehrenfeucht-Fra\"i{}ss\'e{} game. Namely, instead of taking an ordinal $\gamma$ to be the length of the game, we can let an ordinal $\alpha$ be part of the playing field, so to speak, indicating in a sense how many times the spoiler can change his mind about the length of the game, yet keeping the game finite.

More precisely, we define the \textbf{dynamic Ehrenfeucht-Fra\"i{}ss\'e{} game measured by $\alpha$ on $\mathfrak{A}$ and $\mathfrak{B}$}, $EFD_\alpha(\mathfrak{A},\mathfrak{B})$, to be a finite game of perfect information, defined by induction on $\alpha$ as follows:

\begin{itemize}%
\item for $\alpha=0$ there is a unique play (i.e., the players do nothing) that is a win for the duplicator if and only if $\mathfrak{A}
\equiv_0 \mathfrak{B}$,


\item for $\alpha=\beta+1$, a play consists of the spoiler picking an element of one structure, followed by the duplicator picking an element of the other structure, followed by a play of $EFD_\beta((\mathfrak{A},a),(\mathfrak{B},b))$, where $a\in A$ and $b\in B$ are the two elements picked, and this play in $EFD_\alpha(\mathfrak{A},\mathfrak{B})$ is a win for duplicator if and only if the play in $EFD_\beta((\mathfrak{A},a),(\mathfrak{B},b))$ is a win for duplicator,


\item for $\alpha$ a limit ordinal, a play consists of the spoiler picking an ordinal $\beta\lt\alpha$, and then a continued play in $EFD_\beta(\mathfrak{A},\mathfrak{B})$, and this play in $EFD_\alpha(\mathfrak{A},\mathfrak{B})$ is a win for duplicator if and only if the play in $EFD_\beta(\mathfrak{A},\mathfrak{B})$ is a win for duplicator.



\end{itemize}
The game $EFD_\alpha[\mathfrak{A},\mathfrak{B}]$ is defined similarly, using unnested atomic formulas in the base case.

\begin{example}
\label{DefEFD}\hypertarget{DefEFD}{}
We write $\mathfrak{A} \sim^\alpha_\omega \mathfrak{B}$ to mean that the duplicator has a winning strategy in the game $EFD_\alpha(\mathfrak{A},\mathfrak{B})$ and $\mathfrak{A}
\approx^\alpha_\omega \mathfrak{B}$ to mean that the duplicator has a winning strategy in the game $EFD_\alpha[\mathfrak{A},\mathfrak{B}]$.

\end{example}
We use a subscript $\omega$ to indicate that the relations ${\sim^\alpha_\omega}$ and ${\approx^\alpha_\omega}$ form approximations to ${\sim_\omega}$ and ${\approx_\omega}$, respectively.

\hypertarget{backandforth_sequences}{}\subsection*{{Back-and-forth sequences}}\label{backandforth_sequences}

There is an alternative characterization of the relations ${\sim^\alpha_\omega}$ in terms of \textbf{back-and-forth sequences}.

We define a \textbf{back-and-forth sequence of length $\alpha$ from $\mathfrak{A}$ to $\mathfrak{B}$} to be a sequence $(I_\beta)_{\beta\lt\alpha}$ of inhabited sets of pairs $(\bar a,\bar
b)$ of equal length sequences from $\mathfrak{A}$ and $\mathfrak{B}$ such that

\begin{itemize}%
\item $I_\beta \subseteq I_\gamma$ for $\gamma\lt\beta\lt\alpha$,


\item for every $\beta\lt\alpha$ and every $(\bar a,\bar b)\in I_\beta$ we have $(\mathfrak{A},\bar a) \equiv_0 (\mathfrak{B},\bar b)$, and


\item for every $\beta+1\lt\alpha$ and every $(\bar a,\bar b)\in
I_{\beta+1}$ and every $a\in A$, there is a $b\in B$ such that $(\bar a a, \bar b b)\in I_\beta$, and


\item for every $\beta+1\lt\alpha$ and every $(\bar a,\bar b)\in
I_{\beta+1}$ and every $b\in B$, there is an $a \in A$ such that $(\bar a a, \bar b b)\in I_\beta$.



\end{itemize}
\begin{example}
\label{PropBFD}\hypertarget{PropBFD}{}
There is a back-and-forth sequence of length $\alpha$ from $\mathfrak{A}$ to $\mathfrak{B}$ if and only if $\mathfrak{A}
\sim^\alpha_\omega \mathfrak{B}$.

\end{example}
Clearly, if $\mathfrak{A}$ and $\mathfrak{B}$ are back-and-forth equivalent, then we can make a back-and-forth sequences of any length by taking the constant sequence at a back-and-forth system.

\hypertarget{use_in_infinitary_logic}{}\subsection*{{Use in infinitary logic}}\label{use_in_infinitary_logic}

Recall that the formulas in the logic $L_{\infty\omega}$ can be built using infinitary disjunctions and conjunctions. We write $\mathfrak{A}
\equiv_{\infty\omega} \mathfrak{B}$ (resp. $\mathfrak{A}
\equiv_{\infty\omega}^\alpha \mathfrak{B}$) to mean that $\mathfrak{A}$ and $\mathfrak{B}$ satisfy the same sentences of $L_{\infty\omega}$ (resp. of quantifier rank at most $\alpha$).

There is a close relationship between the expressivity of this infinitary logic and the relations ${\sim_\omega}$ and ${\sim_\omega^\alpha}$, as the following theorem shows:

\begin{example}
\label{KarpTheorem}\hypertarget{KarpTheorem}{}
We have $\mathfrak{A} \equiv_{\infty\omega}^\alpha \mathfrak{B}$ if and only if $\mathfrak{A} \sim_\omega^\alpha \mathfrak{B}$ and $\mathfrak{A} \equiv_{\infty\omega} \mathfrak{B}$ if and only if $\mathfrak{A} \sim_\omega \mathfrak{B}$.

\end{example}
This is Theorem 4.47 and Proposition 7.48 in \hyperlink{Vaananen2011}{V\"a{}\"a{}n\"a{}nen 2011}.

\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[type in model theory]]

\end{itemize}
\hypertarget{references}{}\subsection*{{References}}\label{references}

\begin{itemize}%
\item [[Wilfrid Hodges]], \emph{Model Theory}, Cambridge University Press 1993


\item Jouko V\"a{}\"a{}n\"a{}nen, \emph{Models and Games}, Cambridge University Press 2011


\item Wikipedia, \emph{\href{https://en.wikipedia.org/wiki/Ehrenfeucht%E2%80%93Fra%C3%AFss%C3%A9_game}{Ehrenfeucht--Fra\"i{}ss\'e{} game}}



\end{itemize}
[[!redirects Ehrenfeucht-Fraïssé game]] [[!redirects Ehrenfeucht-Fraisse games]] [[!redirects Ehrenfeucht-Fraisse game]] [[!redirects back-and-forth games]] [[!redirects back-and-forth game]] [[!redirects back-and-forth argument]]



\end{document}