\documentclass{amsart}
\usepackage{latexsym,amssymb,eucal}
%%
\bibliographystyle{plain}
\pagestyle{myheadings}
\setlength{\unitlength}{1em}
\renewcommand{\SS}{\mbox{\sf S}}
\newcommand{\goth}[1]{\mathfrak{#1}}
\newcommand{\cal}[1]{\mathcal{#1}}
%%
%%
%% Abkuerzungsfile Datum 23. Maerz 1993
%%
%% Abkuerzungen fuer die Tafellettern
%%
\newcommand{\BA}{\mathbb{A}}
\newcommand{\BB}{\mathbb{B}}
\newcommand{\BC}{\mathbb{C}}
\newcommand{\BD}{\mathbb{D}}
\newcommand{\BE}{\mathbb{E}}
\newcommand{\BF}{\mathbb{F}}
\newcommand{\BG}{\mathbb{G}}
\newcommand{\BH}{\mathbb{H}}
\newcommand{\BI}{\mathbb{I}}
\newcommand{\BJ}{\mathbb{J}}
\newcommand{\BK}{\mathbb{K}}
\newcommand{\BL}{\mathbb{L}}
\newcommand{\BM}{\mathbb{M}}
\newcommand{\BN}{\mathbb{N}}
\newcommand{\BO}{\mathbb{O}}
\newcommand{\BP}{\mathbb{P}}
\newcommand{\BQ}{\mathbb{Q}}
\newcommand{\BR}{\mathbb{R}}
\newcommand{\BS}{\mathbb{S}}
\newcommand{\BT}{\mathbb{T}}
\newcommand{\BU}{\mathbb{U}}
\newcommand{\BV}{\mathbb{V}}
\newcommand{\BW}{\mathbb{W}}
\newcommand{\BX}{\mathbb{X}}
\newcommand{\BY}{\mathbb{Y}}
\newcommand{\BZ}{\mathbb{Z}}
%%
%% Grosse Gothische Buchstaben
%%
\newcommand{\GA}{\mathfrak{A}}
\newcommand{\GB}{\mathfrak{B}}
\newcommand{\GC}{\mathfrak{C}}
\newcommand{\GD}{\mathfrak{D}}
\newcommand{\GE}{\mathfrak{E}}
\newcommand{\GF}{\mathfrak{F}}
\newcommand{\GG}{\mathfrak{G}}
\newcommand{\GH}{\mathfrak{H}}
\newcommand{\GI}{\mathfrak{I}}
\newcommand{\GJ}{\mathfrak{J}}
\newcommand{\GK}{\mathfrak{K}}
\newcommand{\GL}{\mathfrak{L}}
\newcommand{\GM}{\mathfrak{M}}
\newcommand{\GN}{\mathfrak{N}}
\newcommand{\GO}{\mathfrak{O}}
\newcommand{\GP}{\mathfrak{P}}
\newcommand{\GQ}{\mathfrak{Q}}
\newcommand{\GR}{\mathfrak{R}}
\newcommand{\GS}{\mathfrak{S}}
\newcommand{\GT}{\mathfrak{T}}
\newcommand{\GU}{\mathfrak{U}}
\newcommand{\GV}{\mathfrak{V}}
\newcommand{\GW}{\mathfrak{W}}
\newcommand{\GX}{\mathfrak{X}}
\newcommand{\GY}{\mathfrak{Y}}
\newcommand{\GZ}{\mathfrak{Z}}
%%
%% Kleine Gothische Buchstaben
%%
\newcommand{\Ga}{\mathfrak{a}}
\newcommand{\Gb}{\mathfrak{b}}
\newcommand{\Gc}{\mathfrak{c}}
\newcommand{\Gd}{\mathfrak{d}}
\newcommand{\Ge}{\mathfrak{e}}
\newcommand{\Gf}{\mathfrak{f}}
\newcommand{\Gg}{\mathfrak{g}}
\newcommand{\Gh}{\mathfrak{h}}
\newcommand{\Gi}{\mathfrak{i}}
\newcommand{\Gj}{\mathfrak{j}}
\newcommand{\Gk}{\mathfrak{k}}
\newcommand{\Gl}{\mathfrak{l}}
\newcommand{\Gm}{\mathfrak{m}}
\newcommand{\Gn}{\mathfrak{n}}
\newcommand{\Go}{\mathfrak{o}}
\newcommand{\Gp}{\mathfrak{p}}
\newcommand{\Gq}{\mathfrak{q}}
\newcommand{\Gr}{\mathfrak{r}}
\newcommand{\Gs}{\mathfrak{s}}
\newcommand{\Gt}{\mathfrak{t}}
\newcommand{\Gu}{\mathfrak{u}}
\newcommand{\Gv}{\mathfrak{v}}
\newcommand{\Gw}{\mathfrak{w}}
\newcommand{\Gx}{\mathfrak{x}}
\newcommand{\Gy}{\mathfrak{y}}
\newcommand{\Gz}{\mathfrak{z}}
%%
%% Grosse Sanserif Buchstaben
%%
\newcommand{\SA}{\mbox{\sf A}}
\newcommand{\SB}{\mbox{\sf B}}
\newcommand{\SC}{\mbox{\sf C}}
\newcommand{\SD}{\mbox{\sf D}}
\newcommand{\SE}{\mbox{\sf E}}
\newcommand{\SF}{\mbox{\sf F}}
\newcommand{\SG}{\mbox{\sf G}}
\newcommand{\SH}{\mbox{\sf H}}
\newcommand{\SI}{\mbox{\sf I}}
\newcommand{\SJ}{\mbox{\sf J}}
\newcommand{\SK}{\mbox{\sf K}}
\newcommand{\SL}{\mbox{\sf L}}
\newcommand{\SM}{\mbox{\sf M}}
\newcommand{\SN}{\mbox{\sf N}}
\newcommand{\SO}{\mbox{\sf O}}
\newcommand{\SP}{\mbox{\sf P}}
\newcommand{\SQ}{\mbox{\sf Q}}
\newcommand{\SR}{\mbox{\sf R}}
% \newcommand{\SS}{\mbox{\sf S}}
\newcommand{\ST}{\mbox{\sf T}}
\newcommand{\SU}{\mbox{\sf U}}
\newcommand{\SV}{\mbox{\sf V}}
\newcommand{\SW}{\mbox{\sf W}}
\newcommand{\SX}{\mbox{\sf X}}
\newcommand{\SY}{\mbox{\sf Y}}
\newcommand{\SZ}{\mbox{\sf Z}}
%%
%% Kleine Sanserif Buchstaben
%%
\newcommand{\Sa}{\mbox{\sf a}}
% \newcommand{\Sb}{\mbox{\sf b}}
\newcommand{\Sc}{\mbox{\sf c}}
\newcommand{\Sd}{\mbox{\sf d}}
\newcommand{\Se}{\mbox{\sf e}}
\newcommand{\Sf}{\mbox{\sf f}}
\newcommand{\Sg}{\mbox{\sf g}}
\newcommand{\Sh}{\mbox{\sf h}}
\newcommand{\Si}{\mbox{\sf i}}
\newcommand{\Sj}{\mbox{\sf j}}
\newcommand{\Sk}{\mbox{\sf k}}
\newcommand{\Sl}{\mbox{\sf l}}
\newcommand{\Sm}{\mbox{\sf m}}
\newcommand{\Sn}{\mbox{\sf n}}
\newcommand{\So}{\mbox{\sf o}}
\newcommand{\Sq}{\mbox{\sf q}}
\newcommand{\Sr}{\mbox{\sf r}}
\newcommand{\Ss}{\mbox{\sf s}}
\newcommand{\St}{\mbox{\sf t}}
\newcommand{\Su}{\mbox{\sf u}}
\newcommand{\Sv}{\mbox{\sf v}}
\newcommand{\Sw}{\mbox{\sf w}}
\newcommand{\Sx}{\mbox{\sf x}}
\newcommand{\Sy}{\mbox{\sf y}}
\newcommand{\Sz}{\mbox{\sf z}}
%%
%% Grosse Euler Fonts
%%
\newcommand{\EA}{\eul{A}}
\newcommand{\EB}{\eul{B}}
\newcommand{\EC}{\eul{C}}
\newcommand{\ED}{\eul{D}}
\newcommand{\EE}{\eul{E}}
\newcommand{\EF}{\eul{F}}
\newcommand{\EG}{\eul{G}}
\newcommand{\EH}{\eul{H}}
\newcommand{\EI}{\eul{I}}
\newcommand{\EJ}{\eul{J}}
\newcommand{\EK}{\eul{K}}
\newcommand{\EL}{\eul{L}}
\newcommand{\EM}{\eul{M}}
\newcommand{\EN}{\eul{N}}
\newcommand{\EO}{\eul{O}}
\newcommand{\EP}{\eul{P}}
\newcommand{\EQ}{\eul{Q}}
\newcommand{\ER}{\eul{R}}
\newcommand{\ES}{\eul{S}}
\newcommand{\ET}{\eul{T}}
\newcommand{\EU}{\eul{U}}
\newcommand{\EV}{\eul{V}}
\newcommand{\EW}{\eul{W}}
\newcommand{\EX}{\eul{X}}
\newcommand{\EY}{\eul{Y}}
\newcommand{\EZ}{\eul{Z}}
%
% Abkuerzungen fuer die kalligraphischen Lettern
%
\newcommand{\CA}{\mathcal{A}}
\newcommand{\CB}{\mathcal{B}}
\newcommand{\CC}{\mathcal{C}}
\newcommand{\CD}{\mathcal{D}}
\newcommand{\CE}{\mathcal{E}}
\newcommand{\CF}{\mathcal{F}}
\newcommand{\CG}{\mathcal{G}}
\newcommand{\CH}{\mathcal{H}}
\newcommand{\CI}{\mathcal{I}}
\newcommand{\CJ}{\mathcal{J}}
\newcommand{\CK}{\mathcal{K}}
\newcommand{\CL}{\mathcal{L}}
\newcommand{\CM}{\mathcal{M}}
\newcommand{\CN}{\mathcal{N}}
\newcommand{\CO}{\mathcal{O}}
\newcommand{\CP}{\mathcal{P}}
\newcommand{\CQ}{\mathcal{Q}}
\newcommand{\CR}{\mathcal{R}}
\newcommand{\CS}{\mathcal{S}}
\newcommand{\CT}{\mathcal{T}}
\newcommand{\CU}{\mathcal{U}}
\newcommand{\CV}{\mathcal{V}}
\newcommand{\CW}{\mathcal{W}}
\newcommand{\CX}{\mathcal{X}}
\newcommand{\CY}{\mathcal{Y}}
\newcommand{\CZ}{\mathcal{Z}}
%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                                      %
%  logik.sty -- Datum 10. April 1994                                   %
%  Definiert Theoreme, bold math italic, logische Zeichen und          %
%  jede Menge Modaloperatoren                                          %
%                                                                      %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% BoldMathItalic
%
\newfont{\bmi}{cmbxti10 scaled 1000}
%
%  Theorem Umgebungen
%
\newtheorem{thm}{Theorem}[section]
\newtheorem{lem}[thm]{Lemma}
\newtheorem{defn}[thm]{Definition}
\newtheorem{claim}[thm]{Claim}
\newtheorem{prop}[thm]{Proposition}
\newtheorem{cor}[thm]{Corollary}
\newtheorem{conj}[thm]{Conjecture}
\newcommand{\proofbeg}{\begin{proof}}
\newcommand{\proofend}{\end{proof}}
%
% Die Booleschen Symbole
%
\newcommand{\pf}{\rightarrow}
\newcommand{\dpf}{\leftrightarrow}
\newcommand{\und}{\wedge}
\newcommand{\oder}{\vee}
\newcommand{\nicht}{\neg}
\newcommand{\gund}{\bigwedge}
\newcommand{\goder}{\bigvee}
%
% Zeichenhilfen: Klammern, Ueberstreichungen etc.
%
\newcommand{\auf}{\langle}
\newcommand{\zu}{\rangle}
\newcommand{\upp}[1]{{\uparrow\! #1}}
\newcommand{\low}[1]{{\downarrow\! #1}}
\newcommand{\dfgl}{\leftrightharpoons}
\newcommand{\wht}[1]{\widehat{#1}}
\newcommand{\oli}[1]{\overline{#1}}
\newcommand{\uli}[1]{\underline{#1}}
\newcommand{\wit}[1]{\widetilde{#1}}
\newcommand{\nmodels}{\nvDash}
%%
%%  Modalitaeten: Orientierungsmodalitaeten
%%
\newcommand{\oben}{\begin{picture}(.8,.8)
                \put(.4,.17){\makebox(0,0){$\Diamond$}}
                \put(.4,.29){\line(0,1){.3}}
                   \end{picture}}
\newcommand{\unten}{\begin{picture}(.8,.8)
                \put(.4,.17){\makebox(0,0){$\Diamond$}}
                \put(.4,.29){\line(0,-1){.3}}
                   \end{picture}}
\newcommand{\links}{\begin{picture}(.8,.8)
                \put(.4,.17){\makebox(0,0){$\Diamond$}}
                \put(.4,.29){\line(-1,0){.3}}
                   \end{picture}}
\newcommand{\rechts}{\begin{picture}(.8,.8)
                \put(.4,.17){\makebox(0,0){$\Diamond$}}
                \put(.4,.29){\line(1,0){.3}}
                   \end{picture}}
\newcommand{\qoben}{\begin{picture}(.8,.8)
                \put(.4,.17){\makebox(0,0){$\Box$}}
                \put(.4,.29){\line(0,1){.3}}
                   \end{picture}}
\newcommand{\qunten}{\begin{picture}(.8,.8)
                \put(.4,.17){\makebox(0,0){$\Box$}}
                \put(.4,.29){\line(0,-1){.3}}
                   \end{picture}}
\newcommand{\qlinks}{\begin{picture}(.8,.8)
                \put(.4,.17){\makebox(0,0){$\Box$}}
                \put(.4,.29){\line(-1,0){.3}}
                   \end{picture}}
\newcommand{\qrechts}{\begin{picture}(.8,.8)
                \put(.4,.17){\makebox(0,0){$\Box$}}
                \put(.4,.29){\line(1,0){.3}}
                   \end{picture}}
%
% Die Weisse Relation      
%
\newcommand{\wD}{\lozenge}
\newcommand{\wq}{\square}
\newcommand{\whd}{\lhd}
\newcommand{\rwhd}{\rhd}
\newcommand{\nhd}{\ntriangleleft}
\newcommand{\nwhd}{\ntriangleleft}
\newcommand{\raute}{\lozenge}             
\newcommand{\qu}{\square}
\newcommand{\quadrat}{\square}
%
%
%
\oddsidemargin=1truecm\relax%
\evensidemargin=0truecm\relax%
\marginparwidth=2truecm\relax%
\marginparsep=0.2truecm\relax%
%
%
%
\topmargin=-2truecm\relax%
\topmargin=-1truecm\relax%
\headheight=1truecm\relax%                                 %Seite DIN A4
\headsep=0.4truecm\relax%
\textheight=24truecm\relax%
\textheight=22truecm\relax%
\textwidth=15truecm\relax%
\topskip=\baselineskip%
% \footheight=1truecm\relax%
% \footskip=1truecm%%
% \parskip=0.4cm
%
%
%
\newcommand{\punkt}[1]{\put(#1){\makebox(0,0){$\bullet$}}}
\newcommand{\ubla}[2]{\put(#1){\makebox(0,0){#2}}}
\newcommand{\sees}[1]{\stackrel{#1}{\rightarrow}}
\newcommand{\glb}{\mbox{\sl glb\/}}
\newcommand{\lub}{\mbox{\sl lub\/}}
%
\newcommand{\tw}[1]{\mbox{\sl tw\/}(#1)}
\newcommand{\bw}[1]{\mbox{\sl bw\/}(#1)}
\newcommand{\wt}[1]{\mbox{\sl wt\/}(#1)}
%
%
\newcommand{\vor}{\begin{picture}(1.2,1)
                \put(.65,.3){\makebox(0,0){$>$}}
                \put(.6,.3){\makebox(0,0){$\bigcirc$}}
                \end{picture}}
\newcommand{\stackvor}[1]{\vor_{#1}}
%\newocmmand{\upp}[1]{\uparrow\! #1\!}
\newcommand{\down}[1]{\downarrow\! #1 \!}
\newcommand{\wupp}{\begin{picture}(.6,1)
                        \put(.3,.42){\makebox(0,0){$\uparrow$}}
                        \put(.1,0){\line(1,0){.4}}
                      \end{picture}}
\newcommand{\wdown}{\begin{picture}(.6,1)
                        \put(.3,.4){\makebox(0,0){$\downarrow$}}
                        \put(.1,.9){\line(1,0){.4}}
                      \end{picture}}
\newcommand{\wlhd}{\unlhd}
\newcommand{\shp}{\shortparallel}
\newcommand{\desc}[2]{#1 \leftrightsquigarrow #2}
\newcommand{\descri}[3]{#1 \leftrightsquigarrow_{#3} #2}
\newcommand{\master}{\boxtimes}
\newcommand{\fmaster}{\boxplus}
%%
%% Das Mathematische Phi anstatt des Philologischen
%%
\renewcommand{\phi}{\varphi}
%%
\newcommand{\ext}[1]{\mbox{NExt}\, #1}
%%
%%
\newcommand{\titel}{Logic and Syntax --- A Personal Perspective}
\newcommand{\titelleiste}[1]{\markboth{{\it Marcus Kracht, \quad
\titel, \quad \today}}{{\it #1}}}
%
%
%
\title{\titel}
\author{Marcus Kracht}
\address{{\em II. Mathematisches Institut} \\
{\em Freie Universit\"{a}t Berlin} \\
{\em Arnimallee 3} \\
{\em D -- 14195 Berlin} \\
{\tt kracht@math.fu-berlin.de}}
%
%
\begin{document}
\begin{abstract}
Logic, in particular modal logic, can not only be used in semantics 
but also in syntax. Here we study syntactic formalisms from a logical 
point of view. This is a reflection in terms of logic of the view 
that grammar is nothing but a catalogue of abstract descriptive 
principles rather than a productive device, a view that was current 
mainly in the 80ies. The main target of this inverstigation is 
the theory of Government and Binding, although the methods allow 
for a much wider application. 
\end{abstract}
\maketitle
\section{Introduction}
%
%
%
When one talks about the connection between logic and language 
then the first thing that comes to mind is semantics. In fact, 
many distinguished logicians have concerned themselves quite 
intensively with the questions of meaning in natural languages, 
for  examples Russell, Carnap, Church, and Montague. Their 
reflections have led to the development of Type Theory and 
Categorial Grammar. This is a rather fruitful area of research. 
Yet, there is another field of application of formal logic to 
language that has been sparked off by the trend in the 80ies 
to view grammars not as production devices but as theories 
about language --- where the word `theory' is used here in the logical 
sense. The exact meaning of this statement will become clear 
later on. One should say here that this view has been the 
result of a confluence of trends. One was the fact that 
transformational grammar was struggling to get rid of 
its plethora of transformations by trying to isolate a few 
abstract principles. The task of these principles is to 
constrain the transformations in such a way that all and only the 
`natural' transformations would be allowed by the principles. 
This finally led to the elimination of all variety in the 
transformational kernel (there was only one transformation 
left, called Move--$\alpha$). It was then only a 
small step to a purely  descriptive theory of language, which has 
in that time been advocated by Jan Koster~\cite{koster:domains}. 
Another trend that brought up the descriptive approach to 
grammars was the change 
from imperative programming languages to so--called logical 
programming languages, in particular {\sc Prolog}. Many linguists 
got persuaded that the best method of developing computer software 
for natural language manipulation (and here I mean for example 
analysis, generation and translation) was to use logical 
programming languages. The hope was that they would liberate 
the linguist from questions of program execution and allow to 
just develop a database that would contain simply the linguistic 
facts. So the linguist would be able to concentrate on the 
development of this database rather than worrying about 
lousy details of implementation. 
This led in turn to the creation of grammar formalisms that 
were highly reminiscent of the target implementation language. 
The peak of this development are {\sc hpsg} (Head Driven Phrase 
Structure Grammar) and {\sc lfg} (Lexical Functional Grammar), both 
based on feature--value formalisms. It is interesting to note 
here that the pendulum has already returned to the other side. 
Transformational grammar has radically abandoned any use of 
descriptive principles in favour of a purely procedural 
approach. In computer science other programming languages and other 
paradigms (for example functional programming) have 
eclipsed {\sc Prolog}. In linguistics it is not exactly clear 
what the future will bring but as a matter of fact the 
grammar formalisms of the eighties, rather than sheding new 
light on old problems have often enough simply created many 
internal problems, mainly caused by an improper understading 
of the nature of the symbolism. The hazy propaganda behind 
{\sc Prolog} has done its part in mystifying the new tools 
rather than clarifying their potential and their limits.  

In this paper I will speak about some applications of logic, 
in particular modal logic, to the field of syntax. Several 
people have contributed to this enterprise, and they will 
all be named in due course. However, as this title suggests, 
the outline will be quite a personal one. 
%%
\nocite{rogers:say}
%%
\section{The Logical View on Grammar}
%
%
%
For a logician it is perhaps quite easy to understand the 
following description of a grammar. A {\it theory\/} about
$L$ is a set $T$ such that if $T \vdash \varphi$ then 
$\varphi$ holds of all structures of $L$. A {\it grammar\/} 
of a language $L$ is a theory $T$ such that $T \vdash \varphi$ 
iff $\varphi$ is true in all structures of $L$. So, a 
grammar is such that its consequences are all and only 
the $L$--valid sentences. Structures
are either strings, syntactic trees, or pairs 
$\auf \vec{x}, \sigma\zu$, where $\vec{x}$ 
is a string and $\sigma$ is the meaning of $\vec{x}$.  
A run of the mill grammar of English, for example, can 
be seen as a theory about English. Hardly can they claim 
to be grammars in the technical sense above. 
To give some examples: a theory of English may contain 
statements such as {\it the order of the main constituents 
in a declarative sentence is subject--verb--object}, 
{\it the verb agrees in number with the subject\/} and 
so on. Of course, they have to be suitably coded into some 
logical language, and we have to define many notions such 
as subject and object, but these are problems of 
execution rather than principle. 

The problem with the logical definition of grammar is 
that it does not tell us how the sentences of a language 
can be generated and how they can be analyzed. Hence a large 
part of our language activity is left unaccounted for. Moreover, 
still today it is not clear whether what we have in our 
mind is some knowledge of the syntax in descriptive terms 
such as the statements above or whether language as we 
see it is simply an artefact of a rather complex language 
generator--analyser whose structure we yet have to find. 
Chomsky has over and over iterated the point that in his 
view collecting facts about how the sentences of the language 
look like is not to do lingustics at all. It is like collecting 
butterflies rather than doing biological research. He 
has introduced the distinction between E--language --- 
this is what we see at the surface --- and I--language --- 
this is the manifestation of the language in the brain. 
While theories about E--language are easy to develop, 
studying I--language is still today hopelessly difficult, 
and all we have at the moment are hypotheses. 

Chomsky has also always been against descriptions and 
in favour of procedures. He has defined a {\it generative grammar\/} 
of a language $L$ to be an algorithm that generates all and only 
the correct structures of $L$. This definition has been quite 
popular in the 70ies. It defines languages by means of a generating 
device. The generative grammar already tells us how 
the structures are generated. In order to account for our 
analytic facility we also need to have a recognizing 
device for the language. Fortunately, many language classes not only 
have a characterization in terms of a generating device 
but also in terms of an automaton. For example, 
recall that a language is called regular if it can be 
generated by a {\it right--regular grammar}, that is, a grammar 
with rules of the form $\mbox{\tt X} \pf \mbox{\tt a} 
\mbox{\tt Y}$, or $\mbox{\tt X} \pf \mbox{\tt a}$, 
{\tt a} a terminal symbol and {\tt X} and 
{\tt Y} nonterminal symbols. On the other hand, a language 
is regular iff it can be recognized by a finite state 
automaton. Hence, given any regular language, there exists 
a generating device (a right--regular grammar) and an 
analysing device (the finite state automaton). Moreover, 
one can construct one from the other. 

Formal language theory has pretty much remained faithful 
to this approach. Many language classes have been defined 
by means of generating devices (= generative grammars) 
and analysing devices (= automata) have been found. There 
is, however, a problem: we hardly ever have a complete 
description of a natural language. Our knowledge 
even of the best studied languages --- such as English --- 
is still incomplete. However, we would not like to wait until 
our knowledge is perfect before we write a grammar of it. 
And, furthermore, even though it may be enough to describe 
English in terms of some generative grammar and an automaton, the 
working linguist as much as the individuum trying to learn 
English nevertheless have to work with descriptions of it, 
that is to say, theories. What we are therefore ideally like 
to have is some way of mediating between these three ways 
of defining a language: the descriptive, the generative 
and the analytic definition. There is an additional reason 
for trying to develop such tools. Grammar formalisms and 
theories are very often substantially different in the 
way they describe language. Categorial grammar, {\sc hpsg} 
and transformational grammar represent different extremes 
and still at present it is not really understood how to 
translate between a grammar presented in categorial form 
and one that is presented in {\sc hpsg} or transformational 
grammar. But if one would know how to do that then we would 
be able to see what in the different formalisms is mere change 
of notation and what is a substantial difference, and we would 
be able to compare different theories even if they were 
presented in highly different form. 

Matters are however not that simple. We will see shortly that 
many problems turn out to be undecidable. Therefore, only part 
of the project can at all be carried out to satisfaction. 
However, to see that matters are this way requires some 
logical analysis to which we now turn. 

We will discuss mainly two approaches, one based on monadic 
second order logic (MSO) and the other on Propositional 
Dynamic Logic (PDL). We recall here only the necessary 
basic facts. MSO is an extension of predicate logic by means 
of variables over unary predicates and quantifiers over 
such variables. Clearly, MSO can have any number of 
constants for predicates, functions and individuals. 
The sets of variables are $\{x_i : i \in \omega\}$ and 
$\{P_i : i \in \omega\}$. 

Now, PDL or rather PDL with converse, has two sorts of 
expressions: programs and formulae. Programs are formed by 
means of program composition ($;$), nondeterministic union ($\cup$), 
iteration ($^{\ast}$) and converse ($^{\smallsmile}$). 
The set of propositional variables is $\{p_i : i \in \omega\}$. 
Formulae are composed by means of the usual boolean 
connectives. If $\alpha$ is a program and $\varphi$ a 
formula, then $\auf \alpha\zu \varphi$ and $[\alpha]\varphi$ 
is a formula. If $\varphi$ is a formula then $\varphi?$ 
is a program. The set of basic programs is denoted by 
$\Pi_0$. There are the following equations for the converse 
%%
$$\begin{array}{l@{\quad = \quad}l}
R^{\smallsmile\smallsmile} & R \\
(R;S)^{\smallsmile} & S^{\smallsmile}; R^{\smallsmile} \\
(R \cup S)^{\smallsmile} & R^{\smallsmile} \cup S^{\smallsmile} \\
(R^{\ast})^{\smallsmile} & (R^{\smallsmile})^{\ast}
\end{array}$$
%%
Therefore, PDL with converse is expressively equivalent to 
PDL over a set $\Pi_0'$ of basic operators which contains 
for every $\zeta \in \Pi_0$ both $\zeta$ and its converse. 
There is a canonical translation of PDL--formulae into MSO:
%%
$$\begin{array}{l@{\quad := \quad}l}
p_i^{\ddagger} & P_i(x) \\
(\varphi \und \psi)^{\ddagger} & \varphi^{\ddagger} \und 
	\psi^{\ddagger} \\
(\nicht \varphi)^{\ddagger} & \nicht \varphi^{\ddagger} \\
([\alpha]\varphi)^{\ddagger} & \forall y. (\alpha(x,y)^{\dagger} 
	\pf \varphi^{\ddagger}[y/x])
\end{array}$$
%%
In the last clause $y$ is a variable not occurring in
$\varphi^{\ddagger}$. Now $(\alpha(x,y))^{\dagger}$ is 
defined as follows. Pick for each $\zeta \in \Pi_0$ 
a constant $\zeta^{\circ}$ denoting a binary relation.
Now put 
%%
$$\begin{array}{l@{\quad := \quad}l}
\alpha(x,y)^{\dagger} &  \alpha^{\circ}(x,y) \qquad \mbox{ if } 
	\alpha \in \Pi_0\\
(\alpha;\beta)(x,y)^{\dagger} & (\exists z)(\alpha(x,z)^{\dagger} 
	\und \beta(z,y)^{\dagger}) \\
(\alpha \cup \beta)(x,y)^{\dagger} & 
	\alpha(x,y)^{\dagger} \oder \beta(x,y)^{\dagger} \\
(\varphi?)(x,y)^{\dagger} & x \doteq y \und \varphi^{\ddagger} \\
(\alpha^{\ast})(x,y) & (\forall S)((\forall zz')(S(z) \und 
	\alpha(z,z')^{\dagger} \pf S(z')) \und S(x) \pf S(y))
\end{array}$$
%%
Here again some precautions concerning the choice of variables 
must be made. We will freely switch between viewing a structure 
as a structure for PDL (with converse) and the corresponding 
MSO--structure. Furthermore, there will appear a number of 
linguistic structures (strings, trees, and so on). We will 
usually only sketch how they can be turned into models for 
the languages under discussion. A reader with only little 
experience in logic will however already be able to fill in 
the details. 
%%
\section{Regular Languages}
%
%
%
Let $A = \{\mbox{\tt a}_i : i < n\}$ be some finite set, called 
the {\it alphabet}. A finite sequence over $A$ is called a 
{\it string}. $\varepsilon$ is called the {\it empty string}. 
$A^{\ast}$ is the set of all strings over $A$. A {\it (string) 
language\/} over $A$ is a subset of $A^{\ast}$. 
We denote by $\vec{x}\vec{y}$ the 
result of concatenating $\vec{x}$ and $\vec{y}$. Furthermore, 
for sets $R, S \subseteq A^{\ast}$ we put $R \cdot S := 
\{\vec{x}\vec{y} : \vec{x} \in R, \vec{y} \in S\}$ and call 
it the {\it complex product} of $R$ and $S$. We define 
$R^0 := \varepsilon$ and $R^{n+1} := R \cdot R^n$.  
Finally, we put $R^{\ast} := \bigcup_{n \in \omega} R^n$ 
and call it the {\it iteration} of $R$. 
Instead of $\{\vec{x}\}$ we simply write $\vec{x}$. A language 
over $A^{\ast}$ is {\it regular\/} if it is empty or can be 
produced from $\mbox{\tt a}_i$, $i < n$, and $\varepsilon$ 
by means of complex products, unions and iteration. 

A {\it context--free grammar\/} over 
$A$ is a triple $G = \auf N, \mbox{\tt S}, R\zu$ where $N$ is a 
finite set disjoint from $A$, $\mbox{\tt S} \in N$, and 
$R \subset N \times (N \cup A)^{\star}$ a finite set.
(One writes $\mbox{\tt X} \pf \vec{x}$ rather than 
$\auf \vec{\tt X}, \vec{x}\zu$ for a rule. Moreover, 
lower case letters denote symbols from $A$ while upper 
case letters are reserved for symbols from $N$. For 
general reference on context--free grammars and languages 
see \cite{harrison:formal}.) 
$N$ is called the set of {\it nonterminal symbols}, 
{\tt S} the {\it start symbol\/} and $R$ the set of {\it rules}.
Given some strings $\vec{x}, \vec{y} \in (N \cup A)^{\star}$, 
we say that $\vec{y}$ is {\it one--step derivable\/} from 
$\vec{x}$ if there are $\vec{u}$, $\vec{v}$, 
$\vec{w}$ and {\tt X} such that 
(1) $\vec{x} = \vec{u}\mbox{\tt X}\vec{v}$, 
(2) $\vec{y} = \vec{u}\vec{w}\vec{v}$ and 
(3) $\mbox{\tt X} \pf  \vec{w} \in R$. $\vec{y}$ is 
{\it derivable\/} from $\vec{x}$ if $\vec{y}$ can be derived 
from $\vec{x}$ by a series of one--step derivations. Finally, 
$G$ {\it generates\/} $\vec{y}$ if $\vec{y}$ is derivable from {\tt S}. 
We write $L(G)$ for the set of all strings generated by $G$. 
A language $L$ is {\it context--free\/} if there is some 
context--free grammar $G$ such that $L = L(G)$.  
A context--free grammar is {\it right--regular\/} if 
all rules have the form $\mbox{\tt X} \pf \mbox{\tt a}\mbox{\tt Y}$
or $\mbox{\tt X} \pf \mbox{\tt a}$. 

A finite--state automaton over $A$ is a quadruple $\GA = 
\auf Q, q_0, F, \delta\zu$, 
where $Q$ is a finite set, the set of {\it states}, $q_0 \in Q$ a 
distinguished state, the {\it initial state}, $F \subseteq Q$ a 
subset of $Q$ of so--called {\it final\/} or {\it accepting 
states}, and finally $\delta : Q \times A \pf \wp(Q)$ 
the so--called {\it transition function}. We write 
$q \stackrel{\mbox{\tt a}}{\pf} q'$ if $q' \in \delta(q, \mbox{\tt a})$. 
Furthermore, we write $q \stackrel{\vec{x}\vec{y}}{\pf} q'$ iff 
there is a $q'' \in Q$ such that $q \stackrel{\vec{x}}{\pf} q'' 
\stackrel{\vec{y}}{\pf} q'$. We say that $\GA$ {\it accepts\/} 
$\vec{x}$ if there exists a $q \in F$ such that 
$q_0 \stackrel{\vec{x}}{\pf} q$. We write $L(\GA)$ for the set 
of all strings accepted by $\GA$. The following is a well--known 
theorem. 
%%
\nocite{kleene:regular}
%%
\begin{thm}[Kleene]
The following are equivalent for any finite set $A$ and any language 
$L$ over $A$. 
\begin{enumerate}
\item $L$ is regular. 
\item There is a right--regular grammar $G$ such that $L = L(G)$. 
\item There is a finite--state automaton $\GA$ such that 
	$L = L(\GA)$.
\end{enumerate}
\end{thm} 
%%
We note here that there are algorithms that construct $G$ given 
$\GA$ and vice versa.  This theorem fully describes the connection 
between the generative and the analytic aspect of regular languages. 
Moreover, there is a description of regular languages by means of 
regular terms. A regular term is a term built from the symbols 
of $A$ using complex product, union and iteration. For example, 
$(\mbox{\tt a}^2 \cdot \mbox{\tt b})^{\ast} \cup \mbox{\tt a}$ 
is a regular term. It is also possible to construct such terms 
given $G$, and to construct $G$ given the regular term.  

For many purposes, however, the regular terms are not strong 
enough. They are rather clumsy and we wish to replace them by 
some higher order language. For example, take monadic second 
order logic using the following non--logical symbols: a 
binary relation symbol $<$ and a unary predicate $P_i$ for 
each $i < n$. A string is a model for this language in the 
following sense. Take the string $\vec{x} = x_0 x_1 \ldots 
x_{n-1}$. Now let $n := \{0, 1, \ldots, n-1\}$ and  
$m(\vec{x}) := \auf n, <, \auf P^{\vec{x}}_i : i < n\zu\zu$, 
where $P_i^{\vec{x}}(j)$ iff $\vec{x}_j = \mbox{\tt a}_i$. 
In this way we obtain for each language $L \subseteq A^{\ast}$ 
a monadic second order theory $\mbox{\it MSO\/}(L)$, namely the 
common logic of all structures $m(\vec{x})$ such that 
$\vec{x} \in L$. In particular, let $T_0 := \mbox{\it MSO\/}(A^{\ast})$
be the logic of all string models. It is finitely axiomatizable 
and contains eg sentences expressing that $<$ is a discrete total 
ordering with endpoints and that for each element $x$, exactly 
one $P_i$ is true at $x$. Further, given a theory $T$, we let 
$L(T)$ be the set of all strings $\vec{x}$ such that 
$m(\vec{x}) \models T$. $L$ is {\it MSO--definable\/} if 
$\mbox{\it MSO\/}(L)$ is finitely axiomatizable and 
$L = L(\mbox{\it MSO\/}(L))$. The following now holds. 
%%
\nocite{buechi:regular}
%%
\begin{thm}[B\"uchi]
The following are equivalent for any finite alphabet $A$ and any 
language $L$ over $A$. 
%%
\begin{enumerate}
\item $L$ is regular. 
\item $L$ is MSO--definable. 
\item $L$ is definable in MSO by means of a $\Sigma^1_1$--sentence. 
\end{enumerate}
\end{thm}
%%
This state of affairs is quite satisfactory. It is again possible to 
pass from a generating grammar to a MSO--sentence and back. 

An alternative to monadic second order is modal logic. The string 
models may also be viewed as models of some polymodal logic. There 
are several choices with respect to the modal operators. The simplest 
choice is the following. We will introduce boolean constants, 
$\mbox{\tt a}_i$, $i < n$, and two modal operators, $\rechts$ and 
$\links$. Both are tense duals of each other and satisfy ${\sf alt}_1$.
A string $\vec{x} = x_0 x_1 \ldots x_{n-1}$ is made into a model for 
this language as follows. We put $\GF(\vec{x}) := \auf n, 
\lhd, \rhd, \auf \mbox{\tt a}^{\vec{x}}_i : i < n\zu\zu$, 
where $i \lhd j$ iff $j = i+1$, $i \rhd j$ iff $j \lhd i$ and 
$\mbox{\tt a}_i^{\vec{x}} := \{j : x_j = \mbox{\tt a}_i\}$.  
It turns out however that this logic admits unintended models, 
namely infinite ones. We therefore add the transitive closure 
$\rechts^{\ast}$ and $\links^{\ast}$. Both shall satisfy {\sf G}, 
by which we successfully eliminate all finite models. Given a 
language $L \subseteq A^{\ast}$ we define $\mbox{\it ML\/}_4(L)$
to be the common logic of all $\GF(\vec{x})$, where $\vec{x} 
\in L$. Given a modal logic $\Theta$ containing 
$\mbox{\it ML\/}_4(A^{\ast})$ we put $L(\Theta) := 
\{\vec{x} : \GF(\vec{x}) \models \Theta\}$. Using the above 
theorem we deduce that $L(\Theta)$ is always regular. However, 
not all regular languages give rise to different logics, and 
so in contrast to the case of monadic second order logic, 
this modal logic is actually not faithful. Therefore we strengthen 
our logic once more. This time we take the full power of 
Propositional Dynamic Logic with converse, ${\bf PDL}^{\smallsmile}$. 
In our case, one program is sufficient, so we 
put $\Pi_0 := \{\zeta\}$. The interpretation of $\zeta$ 
coincides with that of $\rechts$, and so $\links$ 
corresponds to $\zeta^{\smallsmile}$, $\rechts^{\ast}$ with 
$\zeta^{\ast}$ and $\links^{\ast}$ with 
$(\zeta^{\smallsmile})^{\ast}$. Notice that the interpretation 
of the composite programs can be defined by means of 
MSO--sentences, so that ${\bf PDL}^{\smallsmile}$ is a 
fragment of monadic second order logic. Therefore, any 
logic containing the logic of strings over $A$ defines  
a regular set of strings. The converse also holds, as we 
will show. The idea is the following. Start with a right--regular 
grammar $G = \auf N, \mbox{\tt S}, R\zu$ and introduce for 
every nonterminal symbol {\tt X} a constant $c(\mbox{\tt X})$. 
%%
$$\begin{array}{l@{\quad :=\quad}l}
\mbox{\tt X}^{\dagger} & c(\mbox{\tt X}) \dpf 
       \goder \auf \mbox{\tt a} \und \auf \zeta\zu c(\mbox{\tt Y}) : 
		\mbox{\tt X} \pf \mbox{\tt aY} \in R\zu \\
G^{\dagger} & \goder \auf \mbox{\tt X}^{\dagger} : 
\mbox{\tt X} \in N\zu
\end{array}$$ 
%%
Here, the idea is that $c(\mbox{\tt X})$ is true at a point 
if that point is the left periphery of a constituent of type {\tt X}.
The logic defined by this axiom together with those defining 
all strings is denoted by $\Theta_G$. The frames for $\Theta_G$ 
are not really strings over $A$ since we have the additional 
constants as well. The aim is therefore to eliminate these 
constants. This can be done rather easily as follows. First, 
observe that $G^{\dagger}$ is a system of equivalences of 
the form $p \dpf \psi(p)$ where $\psi(p)$ contains $p$ 
only embedded in $\auf\zeta\zu$. Now the following holds. 
%%
\begin{lem}
In the logic of finite strings, the formula 
$\varphi(p) := p \dpf \alpha \oder \beta \und \auf\zeta\zu p$,  
where $\alpha$ and $\beta$ do not contain $p$, is a global 
implicit definition of $p$. That is to say, it holds that 
if in some model $\varphi(p)$ and $\varphi(q)$ 
holds everywhere then $p \dpf q$ holds everywhere as well. 
\end{lem}
%%
The proof is a simple induction on the depth of a point in the 
frame. Now, an explicit definition on $p$ is a formula $\psi$ 
in which $p$ does not occur such that if in some model 
$\varphi(p)$ holds globally, then $p \dpf \psi$ holds 
globally as well. In the present circumstances such a 
formula exists. It is  
%%
$$\auf (\beta?; \zeta)^{\ast}\zu \alpha$$
%%
Using this, we can step by step eliminate the constants 
$c(\mbox{\tt X})$ and replace $G^{\dagger}$ by a constant 
formula that does not make use of them any more. In that 
way, the regular language is shown to be axiomatically 
definable in ${\bf PDL}^{\smallsmile}$. Notice that we have actually 
produced an algorithm to convert a regular grammar into 
an axiom. Furthermore, the axiom is easily translated into 
monadic second logic, so that all transitions here are 
constructive. 
%%
\begin{thm}
The following are equivalent for any finite alphabet $A$ and 
any language $L$ over $A$. 
%%
\begin{enumerate}
\item $L$ is regular. 
\item $L$ is $\mbox{\bmi PDL}^{\smallsmile}$--definable. 
\end{enumerate}
%%
\end{thm} 
%%
We remark here that instead of {\bf PDL} with converse, 
we could have taken standard {\bf PDL} based on two operators 
which are tense duals of each other. However, these two 
are expressively equivalent, as remarked above. 
%%
\section{Context--Free Languages}
%
%
%
The results of the previous section showed how we can 
translate between various ways of defining the same 
set of objects, in this case finite strings over $A$. 
The only problem is that regular languages are not 
powerful enough. Even programming languages are not 
regular languages. They are --- with some small exceptions --- 
context--free. Fortunately, context--free languages turn 
out to have a theory that is almost as favourable as that 
of the regular languages. The following is the correspondence 
between the generative and the analytic view. (We will not 
define here the notion of a pushdown automaton.) 
%%
\nocite{chomsky:pushdown}
%%
\begin{thm}[Chomsky]
Let $A$ be a finite alphabet and $L$ a language over $A$. 
Then following are equivalent. 
%%
\begin{enumerate}
\item There is a context--free grammar $G$ such that $L = L(G)$. 
\item There is a pushdown automaton $\GA$ such that $L = L(\GA)$. 
\end{enumerate}
\end{thm}
%%
Next we will aim to extend our results on definability. 
For that we must abandon our model structures. They are too 
poor that we can define anything non--regular even by 
using monadic second order logic. (However, second order 
logic would be enough if we use binary relations, for 
example. But that is far too powerful.) Therefore, rather than 
talking about strings we shall now talk about {\it trees}. 
Recall that each derivation of a string $\vec{x}$ in a 
context--free grammar also defines a so--called parse 
or analysis tree of $\vec{x}$ (which usually depends on 
the derivation). This tree is a pair $\auf T, \ell\zu$, 
where $T \subset \omega^{\ast}$ is a tree domain 
and $\ell : T \pf A \cup N$ a labelling function. Here, 
a {\it tree domain\/} is a set $T$ of finite sequences of 
natural numbers such that (i) if $\vec{x} \in T$ and 
$\vec{y}$ is a prefix of $\vec{x}$ then also $\vec{y} 
\in T$ and (ii) if $\vec{x}i \in T$ and $j < i$ then 
also $\vec{x}j \in T$. The tree ordering is taken to 
be the converse of the prefix ordering. (So the empty 
sequence is the maximal element.) For future reference 
a {\it constituent\/} of $T$ is a subset of the form 
$\low{x} := \{y : y \leq x\}$. If the tree is labelled, 
the constituent will also be a labelled tree, with the 
appropriately restricted labelling function. 

We give an example. The following is a context--free 
set of rules. 
%%
$$\begin{array}{l@{\quad \pf \quad}l@{\qquad\qquad}l@{\quad \pf%
	\quad}l}
\mbox{\tt S} & \mbox{\tt S}\ \mbox{\tt S} &
	\mbox{\tt S} & \mbox{\tt A}\ \mbox{\tt B} \\
\mbox{\tt S} & \mbox{\tt B}\ \mbox{\tt A} &
	\mbox{\tt A} & \mbox{\tt S}\ \mbox{\tt A} \\
\mbox{\tt A} & \mbox{\tt A}\ \mbox{\tt S} & 
	\mbox{\tt A} & \mbox{\tt a} \\
\mbox{\tt B} & \mbox{\tt S}\ \mbox{\tt B} & 
	\mbox{\tt B} & \mbox{\tt B}\ \mbox{\tt S} \\
\mbox{\tt B} & \mbox{\tt b} & \multicolumn{2}{l}{}
\end{array}$$
%%
The start symbol is {\tt S} and the terminal alphabet 
is $\{\mbox{\tt a}, \mbox{\tt b}\}$. The following is a
derivation of {\tt ababab}.
%%
$$\mbox{\tt S}, \mbox{\tt AB}, \mbox{\tt ASB}, 
\mbox{\tt ASSB}, \mbox{\tt aSSB}, \mbox{\tt aSSb}, 
\mbox{\tt aBASb}, \mbox{\tt abASb}, 
\mbox{\tt abaSb}, \mbox{\tt abaBAb}, 
\mbox{\tt abaBab}, \mbox{\tt ababab}$$
%%
This grammar generates the set of all strings over 
{\tt a} and {\tt b} which contain the same number of 
{\tt a}'s and {\tt b}'s.
A derivation defines a so--called {\it parse--tree\/} or 
{\it analysis--tree\/} (see \cite{harrison:formal} 
if details are needed). In the case of the previous derivation 
we get the tree shown in Figure~\ref{fig:ana}. 
%%
\begin{figure}
\caption{An analysis tree}
\label{fig:ana}
\begin{center}
\begin{picture}(18,24)
\put(6,22){\makebox(0,0){\tt S}}
\put(5.5,21.5){\line(-1,-1){3}}
\put(6.5,21.5){\line(1,-1){3}}
\put(2,18){\makebox(0,0){\tt A}}
\put(2,17.5){\line(0,-1){3}}
\put(2,14){\makebox(0,0){\tt a}}
\put(10,18){\makebox(0,0){\tt B}}
\put(9.5,17.5){\line(-1,-1){3}}
\put(10.5,17.5){\line(1,-1){3}}
\put(6,14){\makebox(0,0){\tt S}}
\put(14,14){\makebox(0,0){\tt B}}
\put(5.75,13.5){\line(-1,-2){1.5}}
\put(6.25,13.5){\line(1,-2){1.5}}
\put(13.7,13.5){\line(-1,-2){1.5}}
\put(14.25,13.5){\line(1,-2){1.5}}
\put(4,10){\makebox(0,0){\tt B}}
	\put(4,9.5){\line(0,-1){3}}
	\put(4,6){\makebox(0,0){\tt b}}
\put(8,10){\makebox(0,0){\tt A}}
	\put(8,9.5){\line(0,-1){3}}
	\put(8,6){\makebox(0,0){\tt a}}
\put(12,10){\makebox(0,0){\tt S}}
	\put(11.875,9.5){\line(-1,-4){.75}}
	\put(11,6){\makebox(0,0){\tt B}}
	\put(11,5.5){\line(0,-1){3}}
	\put(11,2){\makebox(0,0){\tt b}}
	%%
	\put(12.125,9.5){\line(1,-4){.75}}
	\put(13,6){\makebox(0,0){\tt A}}
	\put(13,5.5){\line(0,-1){3}}
	\put(13,2){\makebox(0,0){\tt a}}
\put(16,10){\makebox(0,0){\tt B}}
	\put(16,9.5){\line(0,-1){3}}
	\put(16,6){\makebox(0,0){\tt b}}
\end{picture}
\end{center}
\end{figure}
%%

Now take monadic second order logic again, with two binary 
relations  $<$ (daughter of) and $\sqsubset$ (left of) 
and unary predicates $P_{\mbox{\tt a}}$ for each $\mbox{\tt 
a} \in A$ and $P_{\mbox{\tt X}}$ for each 
$\mbox{\tt X} \in N$. We can axiomatize the theory of all labelled 
trees over $A$ and $N$. This can be done for any context--free 
set of trees. In fact, for this we hardly need the power 
of MSO. But now notice the following. We may remove from the 
signature any number of predicates $P_{\mbox{\tt X}}$. 
(The resulting structures are trees in which the labelling 
function is only partially defined.) If $S$ is a set of 
structures that is obtained in this way we say that $S$ is 
the {\it projection\/} of a context--free set of trees. 
Any projection of a context--free set of trees is also 
MSO--definable. For the predicates for the nonterminals 
can be eliminated by existential quantification. The converse 
also holds, and this is the first result we note. 
Here, a set $S$ is {\it boundedly branching\/} if there is a 
number $n$ such that each tree of $S$ is at most $n$--branching. 
%%
\nocite{doner:acceptors}
\nocite{thatcher:cf}
\nocite{rogers:studies}
%%
\begin{thm}[Doner, Thatcher, Rogers]
Let $A$ be a finite alphabet and $S$ some set of finite trees 
over $A$. Then the following are equivalent. 
%%
\begin{enumerate}
\item $S$ is the projection of a context--free, boundedly branching set. 
\item $S$ is MSO--definable. 
\end{enumerate} 
\end{thm}
%%
The modal analysis can likewise be boosted up to the context--free 
case. We take two basic operators, $\zeta$ (interpreted as 
{\it immediate left sister of\/}) and $\eta$ (interpreted as 
{\it immediately below of\/}). For each symbol of $A$ and $N$ 
we add constants. The logic of $n$--branching trees where each 
constant is true at exactly one node is denoted by ${\bf Olt}_n$.
Consider now an extension of ${\bf Olt}_n$ by a constant 
axiom $\chi$. Then the set of finite trees satisfying 
$\mbox{\bf Olt}_n \oplus \chi$ is a context--free set. 
We say that a set of finite $n$--branching 
trees is $\mbox{\bf PDL}^{\smallsmile}$--definable if 
it is the model set of a logic $\mbox{\bf Olt}_n \oplus \chi$, 
where $\chi$ is a constant formula. 
%%
\begin{thm}
Let $A$ be a finite alphabet and $S$ some set of finite trees 
over $A$. Then if $S$ is $\mbox{\bmi PDL}^{\smallsmile}$--definable, 
$S$ is the projection of a context--free, $n$--branching set. 
\end{thm}
%%
The use of these theorems is the following. Suppose that we 
have a rather high order principle on syntactic structures, 
such as {\it every trace is 1--subjacent to its antecedent\/}
--- you do not need to know here what that exactly means --- 
then we have established that if this principle can be codified 
using either monadic second order logic or PDL with converse, 
it actually defines a set of context--free structures (modulo 
projection). In this way both James Rogers \cite{rogers:studies}
and \cite{kracht:codes} have shown that various theories of 
grammar (locality theory by Manzini \cite{manzini:locality} 
and relativized minimality by Rizzi \cite{rizzi:minimality}) 
predict that English is context--free since it does not 
participate in unbounded head--movement, which has been 
isolated as the only source of non--context--freeness. 
%%
\section{Monadic Second Order Logic or Dynamic Logic?}
%
%
%
The preceding discussion seems to imply that there is actually 
no difference between the monadic second order logic and 
PDL (with or without converse). However, in the context of 
trees one can show that MSO is actually expressively stronger. 
(This is why in the last theorem we have an implication and 
not an equivalence.) The example is the following. Take all 
homogeneously ternary 
branching trees of finite depth. Let $S$ be the set of 
these trees decorated with boolean labels {\tt P} and {\tt Q} 
such that (a) {\tt P} is true along a binary branching 
subtree and (b) {\tt Q} is true at all leaves at which 
{\tt P} is true. The following context--free grammar 
generates these trees. 
%%
$$\begin{array}{l@{\quad \pf \quad}l}
\mbox{\tt P} \und \nicht \mbox{\tt Q} & 
	\mbox{\tt P} \quad \mbox{\tt P} \quad \nicht \mbox{\tt P} \\
\mbox{\tt P} \und \nicht \mbox{\tt Q} & 
	\mbox{\tt P} \quad \nicht \mbox{\tt P} \quad \mbox{\tt P} \\
\mbox{\tt P} \und \nicht \mbox{\tt Q} & 
	\nicht \mbox{\tt P} \quad \mbox{\tt P} \quad \mbox{\tt P} 
\end{array}$$
%%
Now consider the 
projection of this set onto the language containing 
only {\tt Q}. Then this set is not PDL--definable,  
but it is MSO--definable. The proof is given in 
\cite{kracht:tools}. 

The choice between the two language is therefore one of 
expressivity. It seems therefore to be just a matter 
of convenience which one we chooses. However, there is 
more to that. Let $F$ be a finite set. An 
$F$--tree is a pair $\auf T, \ell\zu$, where $T$ is a 
tree domain and $\ell : T \pf \wp(F)$ a function. 
Define an $F$--grammar to be a pair 
$\auf L, F, \Phi\zu$, where $F$ is a finite set, the set 
of {\it features}, $L$ is an F--lexicon and $\Phi$ 
a (finite) set of theorems in some language for trees 
containing constants for the features from $F$. $L$ 
consists of a finite set of pairs $\lambda = \auf a, E\zu$, 
where $a$ is a member of the alphabet and $E\subseteq F$ a 
set of features. We call $\chi_{\lambda} := \gund_{f \in E} f \und 
\gund_{f \in F - E} \nicht f$ the {\it characteristic formula\/} 
of $\lambda$. The disjunction of all $\chi_{\lambda}$ 
where the first component of $\lambda$ is $a$ is called 
the {\it characteristic formula\/} of $a$. 
We say that $a$ {\it has\/} the feature $f \in E$ but that it 
{\it lacks\/} the feature $g \in F - E$. $\Phi$ 
{\it accepts\/} a string $\vec{x} = a_0 \ldots a_{n-1}$ 
iff there exists an $F$--tree $T$ with yield 
$x_0 \ldots x_{n-1}$ such that $T \models \Phi$ and 
for each $i < n$ the label of $x_i$ satisfies the 
characteristic formula of $a_i$. 

Let $\GT = \auf T, \ell\zu$ be an $F$--tree and $G \subseteq F$. Then 
$\GT_G := \auf T, \ell_G\zu$, where $\ell_G(x) := \ell(x) \cap G$ 
is a $G$--tree and called the {\it projection\/} of $\GT$ 
onto $G$. Now call a feature $f \in F$ {\it inessential\/} in a set 
$S$ of $F$--trees if any tree in $S_{F - f}$ is the projection 
of exactly one tree from $S$. This means that if we already 
know how the features distinct from $f$ are distributed, 
we know how $f$ itself is distributed. Call $f$ {\it eliminable\/} 
if there is a formula $\varphi$ using only the constants for 
features distinct from $f$ such that 
%%
$$\mbox{\sf Th}\, S \models f \dpf \varphi$$
%%
It follows that if $f$ is eliminable it is also inessential, 
but the converse need not hold, as the above example shows. 
In MSO, however, every inessential feature is also eliminable. 
Therefore, whether or not an inessential feature is actually 
eliminable depends on the logical language. 
We may however also turn this around and use the strength 
of the logical language to define the complexity of languages. 
A language $S$ (a set of $F$--trees) has complexity at most 
$\Theta$, where $\Theta$ is some logical language, if (a) $S$ is 
$\Theta$--definable and (b) every inessential feature of $S$ 
is $\Theta$--eliminable. We have seen above that there 
are languages whose complexity is MSO but not PDL. It has 
been shown in \cite{kracht:essential} that the logic with 
four modal operators introduced earlier is strictly weaker 
than PDL and still stronger than boolean logic. (There is 
some maneuvering involved to adjust the definitions to 
the last two cases for we also have to satisfy (a). The 
interested reader is referred to the paper.)
%%
\section{Beyond Context--Free Languages}
%
%
%
As we have seen, all logics presented here define some 
restricted class of languages, namely context--free 
languages, although they define them not via their strings 
but via their structure trees. In fact, for some years it 
has been the consensus among many linguists that 
natural languages are in fact context--free. {\sc Gpsg}
(Generalized Phrase Structure Grammar) was built on 
this assumption. However, in the mid eighties rather 
firm evidence appeared that there exist non--context--free 
languages. The evidence was based on data from 
Z\"urit\"u\"utsch (see Shieber \cite{shieber:evidence}). 
To appreciate these results, let us give some 
examples from three languages, English, German 
and Dutch. (The examples are translations of each other.)
%%
\\[2mm]
\begin{tabular}{ll}
(1E) & {\sf that the children swim}. \\
(2E) & {\sf that Mary teaches the children to swim.} \\
(3E) & {\sf that Peter lets Mary teach the children to swim.} \\
\\
(1G) & {\sf da{\ss} die Kinder schwimmen.} \\
(2G) & {\sf da{\ss} Maria die Kinder schwimmen lehrt.} \\
(3G) & {\sf da{\ss} Peter Maria die Kinder schwimmen 
	lehren l\"a{\ss}t.} \\
\\
(1D) & {\sf dat de kinderen zwemmen.} \\
(2D) & {\sf dat Maria de kinderen laat zwemmen.} \\
(3D) & {\sf dat Peter Maria de kinderen laat leren zwemmen.} 
\end{tabular}
\\[2mm]
%%
These examples can be continued ad libitum.
The word order schemata of these languages are remarkably 
different. To see this more clearly, let us abbreviate the 
word order as follows. We write $V_i$ for the $i$th 
verb and $S_i$ for the subject of the $i$th verb. Then we 
have 
%%
\\[2mm]
\begin{tabular}{l@{\quad : \quad}l}
English & $S_1\; V_1\; S_2 \; V_2\; S_3\; V_3 \ldots$ \\
German  & $S_1\; S_2\; S_3 \ldots V_3\; V_2\; V_1$ \\
Dutch   & $S_1\; S_2\; S_3 \ldots V_1\;  V_2\;  V_3 \ldots$
\end{tabular}
\\[2mm]
%%
We say that in German the dependencies between verbs and 
their subjects are nested while they are crossed in Dutch. 
Now, this suffices to show that Dutch cannot be strongly 
context--free since one cannot get the right 
constituent analysis using a context--free grammar. 
Yet, the data above do {\it not\/} show that no 
context--free grammar can generate the Dutch language 
as a string language. Namely, we can simply generate the 
crossed dependencies as nested ones.  Yet, a proof that 
Dutch is not weakly context--free has 
been found by Huybregts, see \cite{huybregts:overlapping}. 
He showed that there are verbs which require certain types of 
subjects, and so generating the dependencies nested rather 
than crossed would mean that one looses control over the 
restrictions on subjects. Shiebers proof on Z\"urit\"u\"utsch
uses a similar argument. Z\"urit\"u\"utsch allows for the 
Dutch type word order and moreover there are raising 
verbs assigning dative case and those assigning 
accusative case. Since case marking is distinct, 
this proves the claim. 
%%
\footnote{Notice that the verbs {\sf teach}, {\sf let} and so 
on on the one hand take an object (which in Z\"urit\"u\"utsch 
can be either direct or indirect object) and on the other hand 
also an infinitive, whose subject is the object of the 
higher verb. This is why these noun phrases behave both as 
objects and as subjects.}
%%

It has of course always been felt that even if some 
languages are context--free as string languages, 
the corresponding set of analysis trees in many cases 
is not. An example for which this has been argued is
German. (The standard analysis within transformational 
grammar is that all lower verbs raise to the highest 
verb to form a single complex verb.) Also, recently it has 
been shown that German is most likely not weakly context--free 
either (see \cite{groenink:surface}). These intuitions however were 
rather difficult to condense into real proofs, so one 
should say that linguists hoped rather than feared that 
one would be able to find non context--free--string 
languages. After their discovery matters became rather 
complex. On the one hand, transformational grammar has 
always been able to handle such languages, and no change 
was called for; similarly for {\sc lfg}, which was built on 
non--cf structures anyway. However, surface based 
approaches had to adapt to the new situation. 
Several recipes have been tried. One was the 
introduction of string vectors to enhance the 
power of manipulation, another was the introduction 
of stacks of indices in the nonterminals, a third 
was the use of adjunction. These approaches are 
by no means identical; typically they lead to different 
structural analyses. For a survey of different approaches 
see \cite{joshietal:convergence} and \cite{groenink:surface}.

We have earlier quoted results to that Government and Binding 
(GB) predicts that languages are strongly context--free
if they have no unbounded head movement. A case in point 
is English. In that case it was possible to eliminate movement 
by a mechanism that is known as {\it gap--threading}, which 
has first been proposed in {\sc gpsg} (see \cite{gazdar:gpsg}). 
It allows to dispense with movement in favour of passing 
on some finite amount of information on the displaced 
element to its corresponding gap. If we want to analyse 
the whole theory however we cannot hope to eliminate 
head movement in a similar way. Z\"urit\"u\"utsch is known 
to be not context--free. Yet there is a straightforward 
analysis in GB using head movement. It follows that 
head movement adds some complexity to the theory. 
It is therefore indispensable to analyse in detail 
the structures created by GB. 
%%
\section{An Outline of Government and Binding Theory}
%%
Let us now take a look at the standard GB theory. GB is 
part of the tradition called {\it transformational grammar}, 
which takes its name from the fact that it uses {\it transformations}. 
A transformation is an operation on trees, typically a 
unary operation. The basic idea has been that the structures 
of a language are created in two stages. In the first stage 
a so--called deep--structure is generated by a rather 
simple grammar (a context--free grammar of some sort). 
In the next stage, transformations successively operate and 
transform the deep--structure into the surface--structure. 
This surface structure is a tree and may contain phonetically 
empty elements. 
However, if all these things are stripped off we obtain 
the sentence in its official form. Here is an example 
from German. The verb {\it anvertrauen\/} has three 
arguments, a subject (S), a direct object (DO) and 
an indirect object (IO). At deep--structure these come 
in the order S--IO--DO, with the verb being last. From 
this basic order the surface sentence is derived by 
a series of transformations, which consist in simply 
moving around certain constituents. To be able to track 
the derivation the notation of traces with indices is used. 
A $t$ is put at the place where the string originates, 
and give it an index. The displaced constituent also 
gets this index. Notice that only constituents may 
move and therefore they are the bearers of indices. 
Some constituents are highlighted by brackets. 
%%
\\[2mm]
\begin{tabular}{ll}
{\sf der K\"onig seinem Minister diese Geheimnis anvertraute.} 
	& (deep--structure) \\
{\sf [dieses Geheimnis]$_1$ der K\"onig seinem Minister $t_1$ 
	anvertraute.} & \\
{\sf vertraute$_2$ [dieses Geheimnis]$_1$ der K\"onig 
	seinem Minister $t_1$ an $t_2$.} & \\
{\sf [der K\"onig]$t_3$ vertraute$_2$ [dieses Geheimnis]$_1$ 
	$t_3$ seinem Minister $t_1$ an $t_2$.} & (surface--structure) \\
{\sf der K\"onig vertraute dieses Geheimnis seinem Minister an.} 
	& (phonetic form) \\
{\it The king confided this secret to his minister.} & 
\end{tabular}
\\[2mm]
%%
This model has been reformed a number of times. In GB, 
it is assumed that there are four so--called levels of 
representation, D--structure (the former deep--structure), 
S--structure (the former surface--structure), LF (logical 
form) and PF (phonetic form). A derivation is a pair 
$\partial = \auf \vec{\goth{S}}, j\zu$ where 
$\vec{\goth{S}} = \auf \GS_i : i < p\zu$ is a 
sequence of structures and $j < p$. We say 
that $\goth{S}_0$ is the {\it D--structure\/} of 
$\partial$, $\goth{S}_j$ its {\it S--structure\/} 
or surface form and $\goth{S}_{p-1}$ its logical form. The 
phonetic form is derived from the surface form 
by means of some processes that were rarely studied 
in GB. For our purposes we may think of the PF 
simply as the string associated with the surface 
form (together will all empty elements deleted). 
Each $\goth{S}_{i+1}$, $i < p-1$, is derived from 
$\goth{S}_i$ by means of applying the rule 
Move--$\alpha$. We will specify its action later. 
It is assumed that for each level there is a set of 
principles that defines well--formedness at this level. 
In fact, a level of representation is one at which 
such conditions are operative beyond the mere fact 
that the sequence is a derivation. To give an example, 
at S--structure each noun phrase must have case. 
This need not hold at D--structure. So the situation 
is like this. We start with a structure $\goth{S}_0$. 
For it to be a legitimate start, we must satisfy the 
conditions of D--structure. Next we successively 
apply Move--$\alpha$. If the conditions for S--structure 
are met for $\goth{S}_i$, we may call the structure 
the S--structure and derive the phonetic form from it. 
(Also PF has a set of well--formedness conditions 
associated for it.) After that we continue to apply 
Move--$\alpha$ until the conditions of LF are met. 
If we succeed, we have a well--formed derivation. 
%%
\begin{center}
\begin{picture}(30,12)
\put(2,6){\makebox(0,0){\sc ds}}
\put(3,6){\vector(1,0){2}}
\put(6,6){\makebox(0,0){$\GS_1$}}
\put(8,6){\makebox(0,0){$\leadsto$}}
\put(10,6){\makebox(0,0){$\GS_2$}}
\put(12,6){\makebox(0,0){$\leadsto$}}
\put(14,6){\makebox(0,0){$\GS_3$}}
\put(16,6){\makebox(0,0){$\ldots$}}
\put(18,6){\makebox(0,0){$\leadsto$}}
\put(20,6){\makebox(0,0){$\GS_i$}}
	\put(20,10){\makebox(0,0){\sc ss}}
	\put(20,9){\vector(0,-1){2}}
\put(20,5){\vector(1,-1){3}}
\put(24,1){\makebox(0,0){$\vec{x}$}}
\put(20,1){\makebox(0,0){\sc pf}}
\put(21,1){\vector(1,0){2}}
\put(22,6){\makebox(0,0){$\leadsto$}}
\put(24,6){\makebox(0,0){$\GS_{i+1}$}}
\put(26,6){\makebox(0,0){$\ldots$}}
\put(28,6){\makebox(0,0){$\leadsto$}}
\put(30,6){\makebox(0,0){$\GS_j$}}
\put(34,6){\makebox(0,0){\sc lf}}
\put(33,6){\vector(-1,0){2}}
\end{picture}
\end{center}
%%
Now, what is this rule of Move--$\alpha$? It 
consists in taking some constituent of type {\tt X} in the tree, 
and moving it to some other place, and coindexing the 
two elements. This is illustrated in Figure~\ref{fig:move}.
%%
\footnote{Actually, in the linguistic literature one talks 
of {\it the\/} constituent {\tt X} when one actually
means a particular constituent of category {\tt X}. We 
will also use this kind of talk here hoping that it causes
no confusion.} 
%%
\begin{figure}
\caption{A Movement Step}
\label{fig:move}
\begin{center}
\begin{picture}(22,24)
\put(1,22){\makebox(0,0){$(a)$}}
\put(6,22){\line(1,-1){12}}
\put(6,22){\line(-1,-1){4}}
\put(1,18){\makebox(0,0){\tt X}}
\put(2,18){\line(0,-1){3.5}}
\put(2,14){\makebox(0,0){$e$}}
\put(10,18){\line(-1,-1){3.5}}
\put(6,14){\makebox(0,0){\sf was}}
\put(14,14){\line(-1,-1){3.5}}
\put(10,10){\makebox(0,0){\sf seen}}
\put(19,10){\makebox(0,0)[l]{\tt X}}
\put(18,10){\line(-1,-2){2}}
\put(18,10){\line(1,-2){2}}
\put(16,6){\line(1,0){4}}
\put(18,5){\makebox(0,0){\sf a man}}
\end{picture}
%%
\begin{picture}(22,24)
\put(1,22){\makebox(0,0){$(b)$}}
\put(6,22){\line(1,-1){12}}
\put(6,22){\line(-1,-1){4}}
\put(1,18){\makebox(0,0)[r]{$\mbox{\tt X}_i$}}
\put(2,18){\line(-1,-2){2}}
\put(2,18){\line(1,-2){2}}
\put(0,14){\line(1,0){4}}
\put(2,13){\makebox(0,0){\sf a man}}
\put(10,18){\line(-1,-1){3.5}}
\put(6,14){\makebox(0,0){\sf was}}
\put(14,14){\line(-1,-1){3.5}}
\put(10,10){\makebox(0,0){\sf seen}}
\put(19,10){\makebox(0,0)[l]{\mbox{\tt X}}}
\put(18,10){\line(0,-1){3.5}}
\put(18,6){\makebox(0,0){$t_i$}}
\end{picture}
\end{center}
\end{figure}
%%
By a conjuration 
of the various principles at the levels of representation 
it turns out that the set of places to which the constituent 
{\tt X} can be moved as well as the set of constituents that 
are eligible for movement in the first place are quite 
restricted. We will note here that the constituent 
$\mbox{\tt X}_i$ must in particular c--command $t_i$. 
%%
\footnote{Talk of $\mbox{\tt X}_i$ as if it uniquely 
identifies a constituent is justified in this context, since 
there is always only one full constituent with a given 
index.}
%%
This is defined as follows. 
%%
\begin{defn}
Let $\auf T, <\zu$ be a tree and $x, y \in T$. 
$x$ {\bmi c--commands} $y$ iff $x$ is the root or 
there is a node $z$ immediately above $x$ and 
$z \geq y$. 
\end{defn}
%%
Another condition, explained later, says that $t_i$ 
must be {\it subjacent to\/} $\mbox{\tt X}_i$. 
The use of the term {\it movement\/} is 
actually inaccurate. What happens is rather complex. 
At the place where {\tt X} has been we insert a 
so--called {\it trace}, which gets an index  that 
is identical to the index of {\tt X}. (So, we need 
to assume that constituents get equipped with an index at 
D--structure. But there are other solutions.) In the 
received terminology we say that there is a {\it chain--link\/} 
between the new {\tt X} and the trace just inserted, 
and we call $\mbox{\tt X}_i$ the {\it antecedent\/} of the 
trace $t_i$, and the trace is in some circumstances also 
referred to as the {\it gap} with {\it filler\/} 
$\mbox{\tt X}_i$. Of course, $\mbox{\tt X}_i$ may be displaced 
from its new position as well, so that we get a series of 
connected chain links for a single D--structure 
constituent, called a {\it chain}. Notice that when 
$\mbox{\tt X}_i$ is moved to a new position, it leaves a 
trace $t'_i$ of identical index, which now c--commands 
the original trace $t_i$. 
%%
\footnote{In the standard literature, one uses 
notations such as $t'_i$, $t''_i$ etc to distinguish the 
various traces of the same constituent $\mbox{\tt X}_i$. 
However, the actual representation just contains occurrences 
of $t_i$ at different places.}
%%
\section{Multidominance Structures}
%
%
%
For many linguists of different background it has 
always been an alternative to view movement simply 
as adding another daughter link. In the special 
jargon one speaks of {\it structure sharing}. 
Consider the following configuration, where {\tt Y}
is immediately above {\tt X}, which has been displaced 
and received some index $i$. Let {\tt Z} immediately 
dominate the trace of {\tt X}, $t_i$. 
%%
$$\ldots [\ldots \mbox{\tt X}_i \ldots [\ldots t_i \ldots]_{\mbox{\tt Z}} 
\;\ldots]_{\mbox{\tt Y}}\; \ldots$$
%%
Then we assume that $\mbox{\tt X}_i$ and $t_i$ are represented 
by one and the same structure (isomorphic to {\tt X}), 
which is immediately below {\tt Y} and {\tt Z}. We say that 
{\tt Y} and {\tt Z} {\it share\/} the structure {\tt X}. For example, 
rather than proceeding from $(a)$ to $(b)$ as in 
Figure~\ref{fig:move} we now proceed from $(a)$ 
to $(c)$, as shown in Figure~\ref{fig:link}.
%%
\begin{figure}
\caption{A Linking Step}
\label{fig:link}
\begin{center}
\begin{picture}(22,24)
\put(1,22){\makebox(0,0){$(c)$}}
\put(6,22){\line(1,-1){12}}
\put(2,18){\vector(1,1){4}}
\put(2,18){\line(0,-1){12}}
\put(2,6){\line(1,0){8}}
\put(10,6){\line(2,1){8}}
% \put(2,18){\makebox(0,0){\tt X}}
\put(10,18){\line(-1,-1){3.5}}
\put(6,14){\makebox(0,0){\sf was}}
\put(14,14){\line(-1,-1){3.5}}
\put(10,10){\makebox(0,0){\sf seen}}
\put(19,10){\makebox(0,0)[l]{\tt X}}
\put(18,10){\line(-1,-2){2}}
\put(18,10){\line(1,-2){2}}
\put(16,6){\line(1,0){4}}
\put(18,5){\makebox(0,0){\sf a man}}
\end{picture}
\end{center}
\end{figure}
%%
In {\sc hpsg} this idea has been made the leading philosophy. 
Within transformational grammar this move has always 
been resisted, for reasons that are actually not so 
clear. For some brief period in the 90ies Chomsky 
has revived an older idea that what we analyse as 
movement is actually a combination of copying and 
deletion, though the deletion is done at some level 
of representation rather than immediately after the 
copying. Hence, we rather generate the following structure
%%
$$\ldots [\ldots \mbox{\tt X} \ldots  [\ldots \mbox{\tt X} 
\ldots]_{\mbox{\tt Z}}\; \ldots]_{\mbox{\tt Y}}\; \ldots$$
%%
This is exemplified in Figure~\ref{fig:cop}.
%%
%%
\begin{figure}
\caption{A Copying Step}
\label{fig:cop}
\begin{center}
%%
\begin{picture}(22,24)
\put(1,22){\makebox(0,0){$(d)$}}
\put(6,22){\line(1,-1){12}}
\put(6,22){\line(-1,-1){4}}
\put(1,18){\makebox(0,0)[r]{\tt X}}
\put(2,18){\line(-1,-2){2}}
\put(2,18){\line(1,-2){2}}
\put(0,14){\line(1,0){4}}
\put(2,13){\makebox(0,0){\sf a man}}
\put(10,18){\line(-1,-1){3.5}}
\put(6,14){\makebox(0,0){\sf was}}
\put(14,14){\line(-1,-1){3.5}}
\put(10,10){\makebox(0,0){\sf seen}}
\put(19,10){\makebox(0,0)[l]{\tt X}}
\put(18,10){\line(-1,-2){2}}
\put(18,10){\line(1,-2){2}}
\put(16,6){\line(1,0){4}}
\put(18,5){\makebox(0,0){\sf a man}}
\end{picture}
\end{center}
\end{figure}
%%
The absence of indices is actually fully intentional. 
The corresponding structure is written out in a string 
as follows. 
%%
\begin{center}
{\sf [[a man] [was [seen [$\uli{\mbox{\sf a man}}$]]]].}
\end{center}
%%
A empty sequence is marked by underlining it. 
It was believed --- wrongly, I think --- that copying 
makes the formation of chains superfluous. 

Even if transformational grammarians have never 
proposed the use of reentrancy and would probably 
even reject them as legitimate syntactic objects,
it is shown in \cite{kracht:chains} that the 
reentrant syntactic structures have certain advantages 
over the corresponding trace structures from a linguistic 
point of view. Here we will point out a different advantage 
of these structures. \cite{rogers:studies} has argued that 
the addition of indices or the ability to talk about 
isomorphic constituents require logical tools that 
easily yield undecidability. If one is careless enough, 
one ends up with a variant of third order logic over 
trees, a rather strong logical system indeed. However, 
there is no need to do things like that. We may simply 
use reentrant structures instead of the standard ones. 
In what is to follow in this paper we will actually show 
that with the help of reentrant structures we 
can give a full logical analysis of GB--theories without 
assuming too much power. Namely, a fragment of the 
monadic second order theory corresponding to {\bf PDL} 
is with high probability already enough. This means in 
particular that we make no use of derivations at all (and this 
seems to be the reason why reentrant structures are 
so unpopular with transformational syntacticians). 
We will outline this approach here. Let $\auf T, \prec\zu$ 
be a tree. A {\it pre--chain\/} is a set of constituents 
of the tree which is linearly ordered by c--command. 
A pre--chain is a {\it pre--trace chain\/} if all but one 
constituents is a trace. If we are given a syntactic 
structure in a derivation (see the previous section), 
then the chains are the sets of all constituents with 
the same index. We define a {\it pre--trace chain 
structure\/} ({\it preTCS\/}) to be a pair 
$\auf T, C\zu$ where $T$ is a tree and $C$ a set of 
pre--trace chains subject to certain conditions that 
are of no immediate concern here. 

A pair $\GG = \auf G, \prec\zu$, where $\prec \subseteq G^2$ 
is called a {\it rooted acyclic graph\/} if the 
transitive closure of $\prec$ is acyclic and has 
a unique maximal element, called the {\it root}. 
%%
\begin{defn}
A {\bmi pre--multidominance structure (preMDS)} is 
pair $\GM = \auf M, \prec\zu$ such that (1) $\GM$ is a 
rooted acyclic graph, (2) for each $x \in M$ the set 
$M(x) := \{y : x \prec y\}$ is linearly ordered by 
$\prec^+$, which is denoted by $<$. $\GM$ is a {\bmi tree} 
if $\sharp M(x) \leq 1$ for all $x \in M$.
\end{defn}
%%
Here, $\prec$ is the relation {\it is immediately 
dominated by\/} and $<$ the relation {\it is dominated by}. 
A pair $\auf x, y\zu$ where 
$x \prec y$ is called a {\it link}. If $y$ is the 
maximal element of $M(x)$ with respect to $<$, 
$\auf x, y\zu$ is called the {\it surface link\/} 
of $x$. From a preMDS we can construct 
a movement structure as follows. Call a sequence 
$I \in M^+$ an {\it identifier\/} if its first 
element is the root and if $I = J;x;y;K$ for some 
sequences $J,K$ then $y \prec x$ (ie $\auf y, x\zu$ 
is a link). We write $J \prec I$ if $J = I;x$ for 
some $x$. It is easy to see that the set of identifiers 
forms a tree with $\prec$ the relation of immediate 
domination. (This is the standard unravelling 
technique.) Now call a {\it link\/} of $I$ a pair 
$\auf x, y\zu$ such that $I = J; y; x; K$ for some 
sequences $J$ and $K$. $I$ is a {\it surface identifier\/} 
if for all links of $I$ are surface links. 
$I$ is a {\it trace identifier\/} if it has the form 
$J;x;y$ where (a) $J;x$ is a surface identifier 
and (b) $\auf y, x\zu$ is a non--surface link. 
Let $T(\GM)$ be the set of surface identifiers and 
$\GT(\GM) := \auf T(\GM), \prec\zu$. Then 
$\GT(\GM)$ is a tree. Now say that $I$ {\it identifies\/} 
$x$ if $x$ is the last element of $I$. Pick an 
element $x \in M$. $\GC(x)$ will consist of all 
constituents of $\GT(\GM)$ that are of the form 
$\low{I}$, where $I$ identifies $x$. The pair 
$\auf \GT(\GM), \{\GC(x) : x \in M\}\zu$ is a 
preTCS. One can also pass easily from a preTCS  
$\GT = \auf T, C\zu$ to a preMDS. Let $x \approx y$ 
if there is a chain $\GC$ such that $\low{x}, \low{y}
\in \GC$. Put $[x] := \{y : y \approx x\}$ and 
$[x] \prec [y]$ if there exists $x' \in [x]$ and 
$y' \in [y]$ such that $x' \prec y'$. Finally, 
$[T] := \{[x] : x \in T\}$ and 
$\GM(\GT) :=  \auf [T], \prec\zu$. $\GM(\GT)$ 
is a preMDS. 

These constructions show that it is possible to 
pass back and forth between the original structures 
of GB (in the guise of preTCSs) and the reentrant 
structures, called preMDS. A derivation is a sequence 
of preTCSs whose initial member is a tree and in which 
each noninitial member is derived from the previous 
member by means of movement. The analogous operation 
on preMDSs is called a {\it link extension}. 
%%
\begin{defn}
Let $\GM = \auf M, \prec\zu$ be a preMDS. An element $x$ 
is an {\bmi unmoved element} if $x$ is the root or 
$M(x) = \{z\}$, where $z$ is an unmoved element.
\end{defn}
%%
%%
\begin{defn}
Let $\GM = \auf M, \prec_M\zu$ and $\GN = \auf N, \prec_N\zu$
be preTCSs. $\GN$ is called a {\bmi 1--step link 
extension of} $\GM$ if $N = M$ and $\prec_N\; =\; 
\prec_M \cup\, \{\auf x,y\zu\}$, where 
$\auf x, y\zu \not\in \; \prec_M$ and $y$ is 
an unmoved element. A {\bmi derivation} of preMDSs is 
a sequence $\auf \GM_i : i < p\zu$ such that 
$\GM_0$ is a tree and $\GM_{i+1}$ ($i < p-1$) is a 
1--step link extension of $\GM_i$. 
\end{defn}
%%
\begin{lem}
\label{lem:tree}
Let $\GM = \auf M, \prec\zu$ be a preMDS. Then 
there is a derivation $\auf \GM_i : i < p\zu$ 
such that $\GM = \GM_{p-1}$ and
$\auf M_{i+1}, <_{i+1} \zu = \auf M_i, <_i\zu$ for 
all $i < p-1$. 
In particular, $\auf M, <\zu$ is a tree. 
\end{lem}
%%
It turns out that the operations defined earlier not 
only translate preTCSs into preMDSs and back but they 
translate derivations into derivations:
%%
\begin{thm}
For each derivation on preTCS the analogous sequence of 
preMDSs is a derivation. Conversely, for every derivation 
of preMDSs the corresponding sequence of preTCSs is a 
derivation. This correspondence is bijective. 
\end{thm}
%%
This theorem allows to switch freely between these two 
representations. Let us say that we have simplified 
things at least at three points: (A) we have omitted 
the level of logical form, (B) the structures are 
unordered and (C) there is no adjunction, only substitution.
All this can be remedied. However, the details are 
lengthy and unrevealing. The interested reader is 
referred to the abovementioned paper. We will continue 
with this simplified model. 
%%
\section{Axiomatizing Government and Binding Theories}
%
%
%
Now that we have introduced the new structures let us 
attack the question whether it is possible to write 
for some given GB theory an equivalent logical theory 
over preMDSs. The main obstacle is the notion of a 
derivation. We wish that the logical theory says 
directly, given a structure $\GM$, whether or not it is 
a legitimate structure without taking recourse to the 
derivational history. That this is at all possible 
can be motivated from the fact that the logical form 
(which in our simplified model is already the S--structure)
contains a record of the derivational history in form 
of the traces (alias chains). Although the derivational 
history cannot be uniquely recovered, the chains alone 
give as much information as we need. For example, we 
can easily see how long the derivation was. (Simply 
count the number of traces.) Yet, the details are still 
quite involved. We will begin by noting that the class 
of preMDS is $\mbox{\bf PDL}^{\smallsmile}$--definable 
in a language using one primitive program, {\it up}. 
We write {\it down} for its dual, $\mbox{\it up}^{\smallsmile}$. 
Furthere, write $\oben$ for $\auf \mbox{\it up\/}\zu$, 
$\unten$ for $\auf \mbox{\it down\/}\zu$, 
$\oben^+$ for $\auf \mbox{\it up\/}^+\zu$ and 
$\unten^+$ for $\auf \mbox{\it down\/}^+\zu$. 
%%
$$\begin{array}{ll}
(a)\quad \qoben^+ (\qoben^+ p \pf p) \pf \qoben^+ p & 
	(b)\quad \qunten^+ (\qunten^+ p  \pf p) \pf \qunten^+ p \\
(c)\quad \qoben^+ \oben^+ p \pf \oben^+ \qoben^+ p & 
(d)\quad\oben p \und \oben q \pf \oben (p \und 
	(q \oder \qunten^+ q \oder \qoben^+ q)) 
\end{array}$$
%%
$(a)$ and $(b)$ together force that the structures are finite 
and that {\it up\/} is irreflexive and cycle--free. The 
existence of a root is a consequence of $(c)$. That $M(x)$ 
is linearly ordered by $<$ is the content of $(d)$. 

Next we wish to implement the various principles operative 
at the levels. The difficulty that we face here is 
that if $\varphi$ is a condition for D--structures, 
we cannot check $\varphi$ at S--structure, since the 
two structures are in general not isomorphic. The 
D--structure can be reconstructed as follows. 
Call a link $\auf x, y\zu$ a {\it base link\/}
if $y$ is the lowest element of $M(x)$. The 
D--structure is that part of the S--structure that 
is constituted by the root and all base links. 
The idea is therefore to substitute the formula 
$\varphi$ expressing a condition on D--structure 
by a formula $\varphi^{\bullet}$ such that 
the S--structure satisfies $\varphi^{\bullet}$ iff 
the D--structure satisfies $\varphi$. So, rather than 
using {\it up} and {\it down} by which we may follow 
any link we must use the relation $\prec^{\bullet} 
:= \{\auf x, y\zu : \auf x, y\zu \mbox{ is a base link}\}$ 
and its converse. It is not possible to do that using 
some program construct, we have to introduce a new relation 
$\mbox{\it up}^{\bullet}$ into $\Pi_0$ together will 
the following axioms. 
%%
$$\begin{array}{ll}
(e)\quad \auf\mbox{\it up\/}^{\bullet}\zu p \pf 
	[\mbox{\it up\/}^{\bullet}] p & 
(f)\quad \auf \mbox{\it up\/}^{\bullet}\zu p \pf 
	\oben p \\
(g)\quad \oben q \pf \auf \mbox{\it up\/}^{\bullet}\zu 
	\oben^{\ast} q & 
\end{array}$$
%%
These axioms correspond to the following conditions. 
$\mbox{\it up}^{\bullet}$ is a partial function (by $(e$)), 
whose graph is contained in $\prec$ (by $(f)$) and which 
picks out the least element from $M(x)$ for given $x$ (by $(g)$). 
We now enrich the preMDS by a second accessibility relation, 
$\prec^{\bullet}$, which encodes the D--structure. 
$\GM$ is a tree iff $\prec^{\bullet} = \prec$. 
Therefore, $\GM = \auf M, \prec_M, \prec_M^{\bullet}\zu$ 
is derived from $\GN = \auf N, \prec_M, \prec_M^{\bullet}\zu$
iff $M = N$, $\prec_M^{\bullet} = \prec_N^{\bullet}$ and 
$\prec_M \supseteq \prec_N$ (cf Lemma~\ref{lem:tree}). 
Now let $\varphi$ be a formula. Then let $\varphi^{\bullet}$ 
be the result of replacing $\mbox{\it up\/}$ by 
$\mbox{\it up\/}^{\bullet}$. 
%%
\begin{lem}
Let $\GM = \auf M, \prec, \prec^{\bullet}\zu$ be a preMDS and 
$\GN$ its D--structure. Then $\GM \models \varphi^{\bullet}$ 
iff $\GN \models \varphi$. 
\end{lem}
%%
The proof straightforward. $\varphi^{\bullet}$ uses only 
relations defined over $\mbox{\it up\/}^{\bullet}$ and 
$\mbox{\it down\/}^{\bullet}$. So
$\auf M, \prec, \prec^{\bullet}\zu \models \varphi^{\bullet}$ iff 
$\auf M, \prec^{\bullet}\zu \models \varphi^{\bullet}$ 
iff $\GN \models \varphi^{\bullet}$.
Notice that it is immaterial whether or not 
$\varphi$ contains occurrences of $\mbox{\it up\/}^{\bullet}$ 
and $\mbox{\it down\/}^{\bullet}$, though by construction it does 
not. Hence, on condition that the D--structure conditions are 
$\mbox{\bf PDL}^{\smallsmile}$--definable, we can define 
them also as S--structure conditions in an extended language. 

Now for the last part, the well--formedness of the derivation. 
The main condition is the following. If $\mbox{\tt X}_i$ is the 
antecedent of $t_i$ then 
%%
\begin{enumerate}
\item $\mbox{\tt X}_i$  c--commands $t_i$ but does not dominate 
	$t_i$ and 
\item $t_i$ is subjacent to $\mbox{\tt X}_i$. 
\end{enumerate}
%%
Our structures are such that condition 
(1) is automatically fulfilled. Condition (2) must be enforced 
by some axiom, however. It is defined as follows. There is a 
notion of a {\it barrier}, which can be defined by means 
of some constant formula {\sf b}. We will not go into the details 
of that here. Let $u$ be the node immediately dominating 
$\mbox{\tt X}_i$.   Then $t_i$ is {\it subjacent\/} to 
$\mbox{\tt X}_i$ if the open interval 
$]t_i, u[$ in the tree contains at most one barrier. This is the 
definition for trees. To be able to translate this into a 
condition on preMDSs, we must analyze the relationship between 
preMDSs and its derivations. The problem is that a given preMDS 
(or given a preTCS) there are alternative analyses. We may 
illustrate this with split--DPs in German. (We annotate each 
step with the type of movement, for those in the know.)
%%
\\[2mm]
\begin{tabular}{ll}
{\sf Diese B\"ucher hatte ich damals alle meinem Chef gegeben.} & 
(phonetic form) \\
{\it I had then given all these books to my boss.} & \\
{\sf damals ich meinem Chef alle diese B\"ucher gegeben hatte.} & 
(d--structure) \\
\\
First Derivation: & \\
{\sf [alle diese B\"ucher]$_1$ damals ich meinem Chef $t_1$ gegeben 
	hatte.} & (Scrambling) \\
{\sf ich$_2$ [alle diese B\"ucher]$_1$ damals $t_2$ meinem Chef 
	$t_1$ gegeben.} & (Scrambling) \\
{\sf hatte$_3$ ich$_2$ [alle diese B\"ucher]$_1$ damals $t_2$ meinem Chef 
	$t_1$ gegeben $t_3$.} & (V2) \\
{\sf [diese B\"ucher]$_4$ hatte$_3$ ich$_2$ [alle $t_4$]$_1$ damals 
	$t_2$ meinem Chef $t_1$ gegeben $t_3$.} & (Topicalization) \\
\\
Second Derivation: & \\
{\sf [diese B\"ucher]$_1$ damals ich meinem Chef [alle $t_1$] gegeben 
	hatte.} & (Topicalization) \\
{\sf [diese B\"ucher]$_1$ [alle $t_1$]$_2$ damals ich meinem Chef $t_2$
	gegeben hatte.} & (Scrambling) \\
{\sf [diese B\"ucher]$_1$ ich$_3$ [alle $t_1$]$_2$ damals $t_3$ meinem 
	Chef $t_2$ gegeben hatte.} & (Scrambling) \\
{\sf [diese B\"ucher]$_1$ hatte$_4$ ich$_3$ [alle $t_1$]$_2$ damals 
	$t_3$ meinem Chef $t_2$ gegeben $t_4$.} & (V2) \\
\end{tabular}
\\[2mm]
%%
We see that up to renumbering the structures are the same. However, 
in the first derivation the phrase {\sf die B\"ucher} first takes 
a free ride up inside the quantified phrase {\sf alle diese 
B\"ucher} and then moves further up to the sentence initial 
position. In the second derivation, it moves in one step into 
the final position. One can see that the distance of the movement 
(in terms of nodes) is larger. 

How is the difference between these derivations accounted for? 
The answer is not clear, in fact. There are two competing principles 
for derivations that select different derivations. The first is 
called {\sl Freeze}. A derivation satisfies {\sl Freeze\/} if 
no constituent is moved out of a derived constituent (ie one 
that has been moved before). The first derivation does not 
satisfy {\sl Freeze}, but the second does. Another principle 
is that of {\sl Shortest Steps}. It says that a derivation 
must the shortest possible movement steps. The first derivation 
satisfies {\sl Shortest Steps}, but the second does not. There 
are structures which have derivations that satisfy neither 
principle. It can be shown that {\sl Freeze\/}--derivations 
always choose the longest possible path. It turns out that 
these paths have rather unique properties that make them 
suitable for our purposes. 

Let $x, y \in M$ and $x < y$. A {\it path\/} from $x$ to $y$ is 
a subset $\Pi$ of $M$ that has $x$ as lowest element, $y$ as 
maximal element and which is connected via 
$\prec$ and linearly ordered by $<$. 
The {\it length\/} of $\Pi$ is its $\sharp \Pi - 1$. The 
{\it barrier count\/} is the number of barriers in $\Pi - 
\{x,y\}$. 
%%
\begin{lem}
Let $\GM$ be a preMDS, $x, y \in M$ and $x < y$. 
There is a unique longest path $\Lambda$ from $x$ to 
$y$. Moreover, every path from $x$ to $y$ is a 
subset of $\Lambda$. 
\end{lem}
%%
\proofbeg
For a proof, notice that by Lemma~\ref{lem:tree}, $\GM$ is s
derived from a preMDS $\auf M, \prec_0\zu$ that is also a tree. 
Hence, $\auf M, <\zu$ is a tree and $< = \prec_0^+$. So, 
take $x < y$. Now set $\Lambda := [x,y]$.  This set is 
linearly ordered by $<$. It is also maximal. We have to show 
that it is connected via $\prec$. But $< = \prec_0^+$ by 
Lemma~\ref{lem:tree}. So, $\Lambda$ is $\prec_0$--connected 
and therefore also $\prec$--connected, since $\prec_0 
\subseteq \prec$. 
\proofend

Now consider an element $x$. Let $y \in M(x)$ and let $z$ be the 
minimal element of $M(x)$ such that $z > y$. Then a path $\Pi$ from 
$y$ to $z$ is called {\it movement link of\/} $x$ {\it at\/} $y$. 
$\Pi$ is called {\it maximal\/} if it is of maximal length, 
and {\it minimal\/} if it is of minimal length. 
Now, informally stated, the situation is as follows. Given a 
preMDS $\GM$, a {\sl Freeze\/} derivation satisfies 
{\sl Subjacency\/} iff all maximal movement links have 
barrier count $\leq 1$. In this reformulation we can 
modally define those preMDSs which are generated from trees 
by means of {\sl Freeze} derivations respecting {\sl Subjacency}.
%%
$$U(p) := \qunten^{\ast}\qoben^{\ast} (p \pf \qunten^+ \nicht p 
	\und \qoben^+ \nicht p)$$
%%
$U(p)$ holds at $x$ iff the set of points satisfying $p$ is an 
antichain. 
%%
$$K(p,q,r) := p \und U(p) \und U(q) \und U(r) \und 
	\oben q \und 
	\unten (r \und \oben q) \und \qoben^{\ast} (\oben^+ q \pf 
	\nicht \unten r)$$
%%
$K(p,q,r)$ holds at $x$ if there are $y$ and $z$ such that 
$y > x$, $x \in M(z)$, $q$ holds at $y$, $r$ at $z$, the set 
of points for $p$, $q$ and $r$ are antichains, and $y$ is the 
smallest element $> x$ which is also in $M(z)$. 
%%
$$\begin{array}{l@{\quad := \quad}l}
\nabla & \mbox{\it up\/}; (\nicht \mbox{\sf b}?;
	\mbox{\it up\/})^{\ast}; \mbox{\sf b}? \\
\sigma_F & K(p,q,r) \pf [\nabla^2] \unten^+ q 
\end{array}$$
%%
\begin{thm}
$\GM \models \sigma_F$ iff it has a {\sl Freeze}--derivation 
satisfying {\sl Subjacency}.
\end{thm}
%%
\section{Shortest Steps}
%%
Now, we wish to extend this result to {\sl Shortest Steps\/} 
derivations. Our candidate is $\sigma_S$. It says that for 
each element we can design a sequence of minimal movement 
steps satisfying subjacency. 
%%
$$\sigma_S := K(p,q,r) \pf \auf \nabla^2 \zu \unten^+ q$$
%%
Obviously, if there exists a unique minimal path then this 
formulation would suffice.  For then a {\sl Shortest Steps\/} 
derivation satisfies {\sl Subjacency\/} iff all minimal movement
links have barrier count $\leq 1$ iff there always exists 
{\it some\/} path from $x$ to $y$ which has barrier count 
$\leq 1$. However, matters are more difficult here.
For there need {\it not\/} exist a unique smallest 
path. A conterexample is as follows. Let $M$ be the set 
natural numbers $< 5$ and $\prec = \{\auf 0,1\zu, \auf 1,2\zu, 
\auf 2,3\zu, \auf 3,4\zu, \auf 0,3\zu, \auf 1,4\zu\}$. Then 
$\prec^+ = <$. Let $x := 0$ and $y := 4$. The longest path 
from $x$ to $y$ is the whole interval. However, there exist 
two minimal paths: $\{0,3,4\}$ and $\{0,1,4\}$. 
Moreover, there exist structures in which the minimal path 
is actually not eligible, that is, it does not correspond 
to an actual derivation. This is exemplified in 
Figure~\ref{fig:paradox}. In this derivation it is the 
constituent marked {\tt A} that moves first. After that 
{\tt B} moves and in the third step {\tt C} jumps out 
of the landing site of {\tt A}. However, the shortest 
path would definitely be the one from {\tt D}. However, 
{\tt D} is empty, since its content has been moved out 
of {\tt B} at the very first step. So, {\tt D} is not 
eligible. The problem that we see here is that one 
cannot have all elements optimize their journey 
independently. 

What can be done? In \cite{kracht:chains} it is proposed 
that a path is a shortest path if its links are the 
highest possible. 
%%
\begin{defn}
Let $\auf u, v\zu$ be a link.  $\auf u, v\zu$ 
is {\it maximal\/} for $y$ if there is no $v' > v$ 
such that $\auf u, v'\zu$ is a link and $v' \leq y$.
Let $x$ and $y$ be points such that $x < y$ and $\Pi$ a 
path from $x$ to $y$. $\Pi$ is called {\bmi contracted}
if all links are maximal for $y$. 
\end{defn}
%%
\begin{lem}
For each $x$ and $y$ such that $x < y$ there exists exactly 
one contracted path from $x$ to $y$. 
\end{lem}
%%
The contracted paths are not necessarily the shortest paths 
and this is the reason that we cannot employ a definition 
of subjacency using $\sigma_S$. Notice that in order to 
define the notion of maximality we need to compare the link
$\auf u, v\zu$ with an alternative link $\auf u, v'\zu$. 
Such definitions are generally beyond the capacity of 
{\bf PDL}. Hence, in general we cannot define {\sl Shortest 
Steps\/} derivations. However, structures in which 
contracted paths are not minimal are rather contrived. 
It would therefore seem that if there are additional 
principles that conjure to exclude such pathological 
structures, we can actually define {\sl Subjacency\/} 
for derivations satisfying {\sl Shortest Steps}.

We note that while {\sl Freeze\/} is something that can be 
checked on a derivation by checking each step separately, 
{\sl Shortest Steps\/} can only be checked by comparing 
alternative derivations from the same structure. For example, 
suppose that in the second derivation of the preceding 
section there is no other place where to move the phrase 
{\sf die B\"ucher}. Then this step is the shortest one 
available at that moment.  This derivation would therefore 
satisfy {\sl Shortest Steps}. The crux is however that there 
is an alternative derivation that saves the phrase 
{\sf die B\"ucher} to move that long. {\sl Shortest Steps\/} 
is therefore a transderivational economy principle in the sense 
of the Minimalist Program. 
%%
\begin{figure}
\caption{The Shortest Steps Paradox}
\label{fig:paradox}
\begin{center}
\begin{picture}(27,25)
\put(8,23){\line(-1,-1){5}}
	\put(3,18){\line(-1,-2){1}}
	\put(3,18){\line(1,-2){1}}
	\put(2,16){\line(1,0){2}}
\put(8,23){\line(1,-1){15}}
\put(13,18){\line(-1,-1){5}}
	\put(8,13){\line(-1,-2){3}}
	\put(8,13){\line(1,-2){3}}
	\put(5,7){\line(1,0){6}}
	\put(9,11){\line(-1,-2){2}}
	\put(10,9){\line(-1,-2){1}}
		\put(11,9){\makebox(0,0){\tt D}}
\put(18,13){\line(-1,-1){5}}
	\put(13,8){\line(1,-2){2}}
	\put(13,8){\line(-1,-2){2}}
	\put(11,4){\line(1,0){4}}
	\put(14,6){\line(-1,-2){1}}
		\put(15,6){\makebox(0,0){\tt C}}
	%%
	\put(23,8){\line(-1,-2){3}}
		\put(24,8){\makebox(0,0){\tt B}}
	\put(23,8){\line(1,-2){3}}
	\put(20,2){\line(1,0){6}}
	\put(24,6){\line(-1,-2){2}}
		\put(25,6){\makebox(0,0){\tt A}}
	\put(25,4){\line(-1,-2){1}}
%%
\put(23,8){\line(-2,1){10}}
\put(13,13){\vector(-1,0){5}}
%%
\put(24,6){\line(-4,1){8}}
\put(16,8){\vector(-1,0){3}}
%%
\put(10,7){\line(0,-1){2}}
\put(10,5){\line(-1,0){7}}
	\put(6.5,5){\makebox(0,0){\sf X}}
\put(3,5){\vector(0,1){11}}
\end{picture}
\end{center}
\end{figure}
%%
\section{Decidability Issues}
%
%
%
The use of formal analytic tools can lie among other 
in nontrivial technical results, such as decidability 
results. Indeed, there are certain rather satisfying 
results concerning decidability of systems. However, 
the balance between expressivity on the one hand and 
the wish to maintain decidability is rather difficult 
to keep. A very early result is Peters and Ritchie 
\cite{petersritchie:power}, who have shown that 
transformational grammars with a regular grammar 
generating the deep--structures using very 
elementary transformations can generate 
any given recursively enumerable languages. 
This has been seen as a negative fact, since 
the claim that certain languages are generable 
by transformational grammars is then nearly 
vacuous. We will argue below that GB is different 
in this respect, though probably too weak to 
generate all himan languages.

The optimal case is provided by regular 
languages.
%%
\begin{thm}
It is generally decidably, given two regular grammars 
$G$ and $H$, whether $L(G) = L(H)$. 
\end{thm}
%%
The proof is not difficult. It uses certain constructions 
on automata. This property is lost already when we move 
to context--free languages. 
%%
\begin{thm}
It is in general undecidable, given two context--free 
grammars $G$ and $H$, whether $L(G) = L(H)$. 
\end{thm}
%%
In fact, there is also a rather powerful theorem on 
context--free languages, which is as follows. A 
{\it homomorphism\/} of languages is a map 
$h : A^{\ast} \pf B^{\ast}$, where $A$ and $B$ are 
the respective alphabets of the languages,  which 
commutes with concatenation. Moreover, $h(\varepsilon) 
= \varepsilon$. 
%%
\begin{thm}
Any recursively enumerable language is the homomorphic 
image of an intersection of two context--free languages. 
\end{thm}
%%
There are linguistic theories which assume that sentences 
have two different analysis trees. Examples are Lexical Functional 
Grammar and Autolexical Grammar; for the latter 
see \cite{sadock:autolexical}.
Let us call them {\it dual analysis grammars}. 
If these analysis trees are individually generated by 
context--free grammars $G$ and $H$, respectively, then 
call such a grammar {\it context--free}. If we additionally 
assume that there may be empty categories, then any recursively 
enumerable language possesses a context--free dual analysis 
grammar. 
%%
\footnote{This is not to say that Sadock assumes empty 
categories. If not, then a context free dual analysis 
grammar defines a language recognizable in cubic time. 
This is a much more restricted class of languages.}
%%
This shows how powerful certain theories may become. However, 
we have from \cite{rabin:mso} the following result.
%%
\begin{thm}[Rabin]
The MSO theory of any projection of a context--free set of trees 
is decidable. 
\end{thm}
%%
It follows that if we have just any two finitely axiomatized 
theories of projections of context--free sets, we can decide 
whether or not they define the same set. So, while on the string 
level matters are hopeless, on the structure level they are 
again as nice as we can hope for. One can also show that 
for two context--free grammars it is decidable whether they 
generated the same parenthesized strings (this is due to
McNaughton \cite{mcnaughton}).

Now let us move into the non context free case. Here matters 
are still unclear. \cite{rogers:studies} warns us that 
unlimited use of higher order devices can yield undecidability.
However, the structures that we have defined are rather 
constrained and we wish the launch the following
%%
\begin{conj}
The MSO theory of the set of preMDSs is decidable.
In particular the {\bmi PDL}--theory of the set of preMDSs
is decidable.
\end{conj}
%%
It would follow, we claim, that the theory of the full structures 
for GB is decidable (though we have not given evidence for that 
claim let alone defined these structures).  It seems that for all 
intents and purposes the {\bf PDL}--fragment is enough. Now, this 
is only the minimal logic. We still have to account for theories 
of sets of preMDS corresponding to certain possible human languages. 
However, if one follows the philosophy of GB, there is little 
variation to be expected, which mainly consist in alternative 
variants of defining barriers, bounding nodes etc and of course 
the lexicon. It seems therefore that the minimal logic is a generic 
case from which a general result can be established. 

Be matters as they are, there are reasons to believe 
that GB in this formulation is not strong enough to generate 
all possible human languages. The evidence is based on the 
contention that GB theories imply that human languages 
generate semilinear sets (see \cite{harrison:formal} 
for a definition and details). Space does not permit 
us to give evidence for this contention. Jens 
Michaelis \cite{michaelis:mildly} has recently proved this claim for 
Stabler's formalization of the Minimalist Program 
(see \cite{stabler:minimalism}). This 
gives some substance for our claim. Now, 
\cite{groenink:surface} as well as 
\cite{krachtmichaelis:semilinear} give evidence 
that human languages are not necessarily semilinear.
If we are right, then it follows that GB is restrictive 
enough to be decidable in all its parametric variants, but 
too weak to generate structures for all human languages. 
\bibliography{aiml98}
\end{document}

