\documentclass[11pt]{article}

\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsfonts}
\usepackage{amsthm}
\usepackage{mathrsfs}
\usepackage{tikz}

\setlength{\parindent}{0in}
\setlength{\parskip}{3mm}

\title {Equivalence of Star-free and FO(<) languages]}
\date {November 26th}
\author {Daniel Winton}

\begin{document}

\newtheorem{Thm}{Theorem}
\newtheorem{Pf}{Proof}
A language $L$ over an alphabet $\Sigma$ is said to be star-free if it can be given by a regular expression without use of the kleene star operation $*$. This means that a star-free language can be obtained by applying the union, concatenation, and complementation operations a finite number of times on $\emptyset$ and singleton subsets of $\Sigma$. There is a natural correspondence between the operations of a star-free language and logical connectives. This correspondence makes the proof that every star-free language is expressable in FO[$<$], the set of first order formulas with ordering, relatively simple.

\begin{Thm}

If a language is star-free, then it is definable in FO[$<$].

\end{Thm}

Let $S(i,j)$ indicate that position $j$ immediately follows position $i$ and $Q_a(i)$ denote that position $i$ carries letter $a$. Notice that $S(i,j)$ is in FO$[<]$ as $S(i,j)=i<j \land \forall k (i<k \rightarrow j\leq k)$.

Proof. Let $L$ be a star-free regular language and $L'=\{\langle x, i ,j \rangle:$ the part of the string $x$, between indices $i$ and $j$ is contained in $L\}$. Let $\phi_L(i,j)\in$ FO[$<]$ be the formula denoting that for a given string $x, x[i,j)\in L$, that is, $\phi_L(i,j)$ is the the representation of $L'$ in FO[$<$]. We will show that such a $\phi_L(i,j)$ exists via induction on $L$. This is sufficient, as for a given symbol $n$ that always represents the length of a string $x$, $\phi_L(0,n)$ is the formula in FO$[<]$ representing the language $L$. 

First, we must show that $\phi_L$ is in FO$[<]$ for $L$ one of the basis languages, $\emptyset, \epsilon$, and $c$, for some $c\not=\epsilon$ in $\Sigma$.

We have that

$\phi_\emptyset(i,j) =false;$

$\phi_\epsilon(i,j)= i=j;$ 

$\phi_c(i,j)= i<j (Q_c(i)\land S(i,j)).$

Now, we must show that given star-free languages $L_1$ and $L_2$ with FO$[<]$ translations $\psi_1(i,j)$ and $\psi_2(i,j)$ respectively, we have $\phi_{L_1\cup L_2}(i,j)$, $\phi_{L_1\cdot L_2}(i,j)$, and $\phi_{\widetilde{L_1}}(i,j)$ are in FO$[<]$.

We have that

 $\phi_{L_1\cup L_2}(i,j)=\psi_1(i,j) \lor \psi_2(i,j);$

 $\phi_{L_1\cdot L_2}(i,j)=\exists k(i\leq k \land k \leq j) (\psi_1(i,k) \land \psi_2(k,j));$

 $\phi_{\widetilde{L_1}}(i,j)=\lnot \psi_{1}(i,j)$.

As star-free languages can be obtained by applying the union, concatenation, and complementation operations a finite number of times on $\emptyset$ and singleton subsets of $\Sigma$, then we are done. \qedsymbol

%Notice that here that our formulas $\phi_{L}(i,j)$ define the language $L=\{\langle x,i,j\rangle: x[i,j) belongs to L\}$. Then, for $n=|x|$, $\phi_{L}(0,n) defines L.

%Proof. We will show that any star-free language is describable in FO$[<]$ via induction. Let $S$ be a star-free language. Then the regular expression that describes $S$ is given by only union, concatenation, and complementation a finite number of times on $\emptyset$ and singleton letters. 

%Notice that the singleton sets $a, \emptyset$ are definable in FO$[<].$

%$a$ is given by $\exists i (\Sigma(a) \land Q_a(i))\land\forall j \lnot(j= i)\lnot\exists b(\Sigma(b)\land Q_b(j));$ and

%$\emptyset$ is given by $\forall i\lnot\exists a(Q_a(i)\land \Sigma(a))$.

%First, we show that the union, concatenation, and complementation operations on singleton sets are $FO[<]$ definable.

%$a\cdot b$ is given by $\exists i\exists j(\Sigma(a) \land \Sigma(b)\land S(i,j)\land Q_a(i) \land Q_b(j))\land\forall k\lnot(k=i\lor k=j)\lnot\exists c(\Sigma(c)\land Q_c(k));$

%$a + b$ is given by $\exists i (\Sigma(a) \land \Sigma(b) \land Q_a(i) \lor Q_b(i) \land \lnot(Q_a(i)\land Q_b(i));$

%$\widetilde{a}$ is given by $\emptyset\lor \exists i\exists j \exists b(Q_a(i) \land (Q_b(j) \land \Sigma(a) \land \Sigma(b)\land S(i,j) \lor S(j,i));$ 

%$\widetilde{\emptyset}$ is given by $\exists i \exists a(\Sigma(a) \land (Q_a(i))$.

%Assume that $\phi_1$ and $\phi_2$ are first-order formulas such that $L_1=L(\phi_1)$ and $L_2=L(\phi_2)$ for $L_1$ and $L_2$ star-free languages. We will show that $L_1\cdot L_2$, $L_1\cup L_2$ and $\widetilde{\phi_1}$ are all first order-definable.

%$L_1\cdot L_2$ is given by $\exists i(\phi_1|_{\leq i} \land \phi_2|_{>i})$; 

%$L_1\cup L_2$ is given by $(\phi_1\land \lnot \phi_2) \lor (\lnot\phi_1 \land \phi_2);$ and

%$\widetilde{L_1}$ is given by $\lnot(\phi_1)$.

%As $S$ must be the language given by one of these cases, then $S$ is first definable in FO$[<]$ as desired.

% START OF CONVERSE HERE 

We now show that the converse of the above statement is true. That is, we will show that if a language is definable in FO[$<$] then it is star-free. 

\begin{Thm}

If a language is definable in FO[$<$], then it is star free.

\end{Thm}

For any formula $\phi(u_1, ..., u_m)$ in FO[$<$] we define its star-free translation $L_\phi$ through use of stacked words. The alphabet of our stacked words is $\Sigma\times\{0,1\}^m$, where $m$ is the number of free variables in $\phi$. For a string $x\in\Sigma^n$ we have stacked word $x'$ given by an $(m+1)\times n$ matrix with first row given by the string $x$ and each subsequent row $r_i$ corresponding to variable $u_i$. Each row will have exactly one $1$, where the column this $1$ lies in is given by the index of the variable. We define $L_\phi$ by $L_\phi=\{x':x \models \phi(a_1,..., a_m)\}$ where the $a_i$ are the values of $u_i$ as assigned by $x$. We show that for each $\phi\in$ FO[$<$] we have $L_\phi$ is star-free regular. We willl prove this via induction on quantifier depth.

Proof: We first show that formulas in PL[$<$], propositional logic with ordering, are star-free. Every connective in PL[$<$] can be given in terms of $\lnot$ and $\lor$. Note that given $L_1$ and $L_2$ star-free languages with regular expressions $\alpha_1$ and $\alpha_2$ corresponding to $\phi_1, \phi_2\in$ FO[$<$] we have $\lnot\phi_1$ given by $\widetilde{\alpha_1}$ and $\phi_1\lor\phi_2$ given by $\alpha_1\cup\alpha_2$, both of which are clearly star-free. Thus, it suffices to show that the atomic predicates $Q_a(i)$ and $i<j$ are star-free expressable.

For $\phi(u_1, ..., u_m)$ given by $\phi=Q_{c_k}(u_j)$ and $\Sigma=\{c_1, ..., c_l\}$ we show that $L_{\phi}$ is star-free.

Lemma: The language given by taking the kleene star operation on a union of singleton elements in an alphabet $\Sigma$ is a star-free. 

Proof of Lemma: For $\Sigma=\{a_1, ..., a_n\}$ and $b_1, ..., b_m\in \Sigma$ we have that $(b_1+ ... + b_n)^*$ can be given by the complement of the regular expression $\Sigma^* (\Sigma-\{b_1, ... b_n\}) \Sigma^*$. Note that $\Sigma^\star$ is star-free as it is the complement of the empty set. $\triangle$

An arbitrary element of length $n>u_j=i$ in $L_\phi$ is a stacked word $x'$ of the form

\begin{table}[!htb]
\begin{tabular}{llllll}
                                                                       & 1                          & ...                      & $u_j=i$                    & ...                      & n                          \\ \cline{2-6} 
\multicolumn{1}{l|}{x}                                                 & \multicolumn{1}{l|}{$c_f$} & \multicolumn{1}{l|}{} & \multicolumn{1}{l|}{$c_k$} & \multicolumn{1}{l|}{} & \multicolumn{1}{l|}{$c_g$} \\ \cline{2-6} 
\multicolumn{1}{l|}{1}                                                 & \multicolumn{1}{l|}{}      & \multicolumn{1}{l|}{}    & \multicolumn{1}{l|}{}      & \multicolumn{1}{l|}{}    & \multicolumn{1}{l|}{}      \\ \cline{2-6} 
\multicolumn{1}{l|}{\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular}} & \multicolumn{1}{l|}{}      & \multicolumn{1}{l|}{}    & \multicolumn{1}{l|}{}      & \multicolumn{1}{l|}{}    & \multicolumn{1}{l|}{}      \\ \cline{2-6} 
\multicolumn{1}{l|}{j}                                                 & \multicolumn{1}{l|}{0}     & \multicolumn{1}{l|}{...} & \multicolumn{1}{l|}{1}     & \multicolumn{1}{l|}{...} & \multicolumn{1}{l|}{0}     \\ \cline{2-6} 
\multicolumn{1}{l|}{\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular}} & \multicolumn{1}{l|}{}      & \multicolumn{1}{l|}{}    & \multicolumn{1}{l|}{}      & \multicolumn{1}{l|}{}    & \multicolumn{1}{l|}{}      \\ \cline{2-6} 
\multicolumn{1}{l|}{m}                                                 & \multicolumn{1}{l|}{}      & \multicolumn{1}{l|}{}    & \multicolumn{1}{l|}{}      & \multicolumn{1}{l|}{}    & \multicolumn{1}{l|}{}      \\ \cline{2-6} 
\end{tabular}
\end{table}
 
such that $x\in \Sigma^n$ and all entries in $x'$ are in $\{0, 1\}$. $L_\phi$ can then be given by the regular expression.

{\tiny
\begin{table}[!htb]
$\left(\footnotesize\begin{tabular}{|l|}
\hline
$\!c_1\!\!$                                             \\ \hline
$\!0\!$                                                \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\end{tabular}
 + ... +
\begin{tabular}{|l|}
\hline
$c_1$                                             \\ \hline
1                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
1                                                 \\ \hline
\end{tabular}
+ ... +
\begin{tabular}{|l|}
\hline
$c_l$                                             \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\end{tabular}
+ ... +
\begin{tabular}{|l|}
\hline
$c_l$                                             \\ \hline
1                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
1                                                 \\ \hline
\end{tabular}
 \ \right)^*$
$\left(\footnotesize \begin{tabular}{|l|}
\hline
$c_k$                                             \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
1                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\end{tabular}
+ ... +
\begin{tabular}{|l|}
\hline
$c_k$                                             \\ \hline
1                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
1                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
1                                                 \\ \hline
\end{tabular} \ \right)$
\\
$\left(\footnotesize \begin{tabular}{|l|}
\hline
$c_1$                                             \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\end{tabular}
 + ... +
\begin{tabular}{|l|}
\hline
$c_1$                                             \\ \hline
1                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
1                                                 \\ \hline
\end{tabular}
+ ... +
\begin{tabular}{|l|}
\hline
$c_l$                                             \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\end{tabular}
+ ... +
\begin{tabular}{|l|}
\hline
$c_l$                                             \\ \hline
1                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
1                                                 \\ \hline
\end{tabular}
 \ \right)^*$
\end{table}.
}

By the Lemma above, we have that this regular expression is star-free.

Now we show that for $\phi(u_1, ..., u_m)$ given by $\phi=u_i<u_j$, for $i,j\in\{1, ..., m\}$ we have $L_\phi$ is star-free. An arbitrary element of length $n>u_i=k,u_j=l$ in $L_\phi$ is a stacked word $x'$ of the form 

\begin{table}[!htb]
\begin{tabular}{llllllll}
                                                                       & 1                          & ...                      & $u_i=k$                    & ...                      & $u_j=l$                    & ...                      & n                          \\ \cline{2-8} 
\multicolumn{1}{l|}{x}                                                 & \multicolumn{1}{l|}{$c_a$} & \multicolumn{1}{l|}{} & \multicolumn{1}{l|}{$c_b$} & \multicolumn{1}{l|}{} & \multicolumn{1}{l|}{$c_c$} & \multicolumn{1}{l|}{} & \multicolumn{1}{l|}{$c_d$} \\ \cline{2-8} 
\multicolumn{1}{l|}{1}                                                 & \multicolumn{1}{l|}{}      & \multicolumn{1}{l|}{}    & \multicolumn{1}{l|}{}      & \multicolumn{1}{l|}{}    & \multicolumn{1}{l|}{}      & \multicolumn{1}{l|}{}    & \multicolumn{1}{l|}{}      \\ \cline{2-8} 
\multicolumn{1}{l|}{\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular}} & \multicolumn{1}{l|}{}      & \multicolumn{1}{l|}{}    & \multicolumn{1}{l|}{}      & \multicolumn{1}{l|}{}    & \multicolumn{1}{l|}{}      & \multicolumn{1}{l|}{}    & \multicolumn{1}{l|}{}      \\ \cline{2-8} 
\multicolumn{1}{l|}{i}                                                 & \multicolumn{1}{l|}{0}     & \multicolumn{1}{l|}{...} & \multicolumn{1}{l|}{1}     & \multicolumn{1}{l|}{...} & \multicolumn{1}{l|}{0}     & \multicolumn{1}{l|}{...} & \multicolumn{1}{l|}{0}     \\ \cline{2-8} 
\multicolumn{1}{l|}{\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular}} & \multicolumn{1}{l|}{}      & \multicolumn{1}{l|}{}    & \multicolumn{1}{l|}{}      & \multicolumn{1}{l|}{}    & \multicolumn{1}{l|}{}      & \multicolumn{1}{l|}{}    & \multicolumn{1}{l|}{}      \\ \cline{2-8} 
\multicolumn{1}{l|}{j}                                                 & \multicolumn{1}{l|}{0}     & \multicolumn{1}{l|}{...} & \multicolumn{1}{l|}{0}     & \multicolumn{1}{l|}{...} & \multicolumn{1}{l|}{1}     & \multicolumn{1}{l|}{...} & \multicolumn{1}{l|}{0}     \\ \cline{2-8} 
\multicolumn{1}{l|}{\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular}} & \multicolumn{1}{l|}{}      & \multicolumn{1}{l|}{}    & \multicolumn{1}{l|}{}      & \multicolumn{1}{l|}{}    & \multicolumn{1}{l|}{}      & \multicolumn{1}{l|}{}    & \multicolumn{1}{l|}{}      \\ \cline{2-8} 
\multicolumn{1}{l|}{m}                                                 & \multicolumn{1}{l|}{}      & \multicolumn{1}{l|}{}    & \multicolumn{1}{l|}{}      & \multicolumn{1}{l|}{}    & \multicolumn{1}{l|}{}      & \multicolumn{1}{l|}{}    & \multicolumn{1}{l|}{}      \\ \cline{2-8} 
\end{tabular}
\end{table}

such that $x\in \Sigma^n$ and the rest of the entries in $ x'$ are in $\{0,1\}$. $L_\phi$ can be given by the following regular expression

\begin{table}[!htb]
$\left(\footnotesize \begin{tabular}{|l|}
\hline
                                                  \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\end{tabular}
+ ... +
\begin{tabular}{|l|}
\hline
                                                  \\ \hline
1                                              \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
1                                                 \\ \hline
\end{tabular} \right)^*$
$\left(\footnotesize\begin{tabular}{|l|}
\hline
                                                  \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
1                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\end{tabular}
+ ... +
\begin{tabular}{|l|}
\hline
                                                  \\ \hline
1                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
1                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
1                                                 \\ \hline
\end{tabular}\right)$
$\left (\footnotesize\begin{tabular}{|l|}
\hline
                                                  \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\end{tabular}
+ ... +
\begin{tabular}{|l|}
\hline
                                                  \\ \hline
1                                              \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
1                                                 \\ \hline
\end{tabular} \right)^*$
\\
$\left(\footnotesize\begin{tabular}{|l|}
\hline
                                                  \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                               \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
1                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\end{tabular}
+ ... +
\begin{tabular}{|l|}
\hline
                                                  \\ \hline
1                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
1                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
1                                                 \\ \hline
\end{tabular}\right)$
$\left(\footnotesize\begin{tabular}{|l|}
\hline
                                                  \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\end{tabular}
+ ... +
\begin{tabular}{|l|}
\hline
                                                  \\ \hline
1                                              \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
0                                                 \\ \hline
\begin{tabular}[c]{@{}l@{}}.\\ .\\ .\end{tabular} \\ \hline
1                                                 \\ \hline
\end{tabular} \right)^*$.

\end{table}


We have shown that the atomic predicates and logical connectives defining PL[$<$] are star-free expressable, and so we are done with the proof of the base case.

%Assume that all formulas in FO[$<$] with $n$ quantifiers have star-free translations. We will show that any formula in FO[$<$] with $n+1$ quantifiers also has a star-free translation.  

%Let $\psi(v,w, ...)=\exists u \phi(u,v,w,...)$ where $\phi$ is a formula in FO[$<$] with $n$ quantifiers. We are allowed to assume the first quantifier in $\psi$ is existential as $\exists \equiv \lnot (\forall \lnot)$ and we have shown in the base-case that the negation of a formula in FO[$<$] with a star-free translation also has a star-free translation. As $\phi$ has $n$ quantifiers, then by assumption it is star-free regular. Therefore, there must exist a unique minimal automaton $M_\phi$ over the alphabet of our stacked words defining the language $L_\phi$ of $\phi$. For convenience sake, assume that the last row in the matrices giving the stacked words of $L_\phi$ corresponds to the variable $u$. For $M_\phi$ of the form 

%First, we must show that Theorem 2 holds for the base case, that is, the set of languages in FO[$<$] with no quantifiers. We will denote the set of formulas in FO[$<]$ with no quantifiers by PL[$<$], as they are exactly the set of formulas in propositional logic with ordering. Note that any connective in propositional logic can be given in terms of $\lor$ and $\lnot$. We will prove the base case via induction on formula complexity.






\end{document}