A Two-Variable Fragment of English.
Controlled languages are regimented fragments of natural language designed to make the processing of natural language more efficient and reliable. This paper defines a controlled language, E2V, whose principal grammatical resources include determiners, relative clauses, reflexives and pronouns. We provide a formal syntax and semantics for E2V, in which anaphoric ambiguities are resolved in a linguistically natural way. We show that the expressive power of E2V is equal to that of the two-variable fragment of first-order logic. It follows that the problem of determining the satisfiability of a set of E2V sentences is NEXPTIME complete. We show that E2V can be extended in various ways without compromising these complexity results; however, relaxing our policy on anaphora resolution renders the satisfiability problem for E2V undecidable. Finally, we argue that our results have a bearing on the broader philosophical issue of the relationship between natural and formal languages.
Introduction
Controlled languages are regimented fragments of natural language
designed to make the processing of natural language more ecient
and reliable. Although work on controlled languages was originally
motivated by the need to produce uniform and easily translatable
technical documentation, attention has recently turned to their possible
application to system specications (Fantechi et al. (1994), Fuchs,
Schwertl and Torge (1999b), Fuchs, Schwertl and Schwitter (1999a),
Holt (1999), Holt and Klein (1999), Macias and Pulman (1995), Nelken
and Francez (1996), Vadera and Meziane (1994) ). This interest in
natural specication languages is motivated by the fact that many design
engineers and programmers nd formal specication languages|
usually, some variety of logic|alien and hard to understand. The hope
This paper was largely written during a visit to the Department of Computer
Science at the University of Zurich in 1999. The author wishes to thank David Bree,
Norbert Fuchs, Nick Player and an anonymous referee for their valuable comments
on this paper, and Michael Hess, Rolf Schwitter and Uta Schwertl for stimulating
discussions.
c
2001 Kluwer Academic Publishers. Printed in the Netherlands.
Ian Pratt-Hartmann
is that, by selecting a regimented subset of natural language, the precision
oered by formal specication languages can be combined with
the ease-of-understanding associated with natural language.
A new factor with important implications for the use of controlled
languages is the explosion of research into decidable fragments of logic.
Known decidable fragments include various prex classes (see Borger,
Gradel and Gurevich (1997) for a survey), the guarded fragment
(Andreka, van Benthem and Nemeti (1998), Gradel (1999)) and, most
importantly for the purposes of this paper, the two-variable fragment
(Mortimer (1975), Gradel and Otto (1999)). The relevance of this re-search
to controlled languages is clear: given a controlled language
which is mapped to some logic, the question naturally arises as to
whether that logic enjoys good computational characteristics; conversely,
given a logic whose computational characteristics are well-understood,
it would be useful to identify a controlled language which maps to it.
This paper provides a study in how to match a controlled language
to a decidable logic with known computational characteristics. The
controlled language in question, called E2V, is shown to have the expressive
power of the two-variable fragment of rst-order logic. The
grammar of E2V has been kept as simple as possible, in order to clarify
the logical issues involved; thus, E2V is certainly not being proposed
as a practically useful controlled language. However, the techniques
developed in this paper easily carry over to various salient extensions
of E2V; therefore, we claim, our results are of direct relevance to the
development of practically useful controlled languages. In addition, we
argue that these results have a bearing on the broader philosophical
issue of the relationship between natural and formal languages.
The plan of the paper is as follows. Section 2 introduces the syntax
and semantics of E2V; section 3 establishes upper bounds on its
section 4 establishes corresponding lower bounds; and
section 5 discusses the broader philosophical signicance of this work.
2. The syntax and semantics of E2V
E2V is a fragment of English coinciding, in a sense to be made precise
below, with the two-variable fragment of rst-order logic. Its key
grammatical resources include determiners, relative clauses, re
exives
and pronouns. Examples of E2V sentences are:
(1) Every artist despises every beekeeper
(2) Every artist admires himself
Two-Variable Fragment of English 3
(3) Every beekeeper whom an artist despises admires him
Every artist who employs a carpenter despises every beekeeper
who admires him.
The remainder of this section is devoted to a formal specication of the
syntax and semantics of E2V. The syntax determines which strings of
words count as E2V sentences, and the semantics determines how those
sentences are to be interpreted, by mapping them to formulas of rst-
order logic. The relatively formal nature of the presentation facilitates
the proofs of theorems in subsequent sections concerning the expressive
power of E2V and the computational complexity of reasoning within
it. Generally, the semantics of E2V is unsurprising, in that it interprets
E2V sentences in accordance with English speakers' intuitions. In
particular, sentences (1){(4) are mapped to the respective formulas:
Thus, when reading E2V, care must be taken to respect its particular
conventions regarding scope ambiguities and pronoun resolution. It is
not dicult to see that each of the formulas (5){(8) can be equivalently
written using only two-variables. We establish below that, given our
chosen conventions regarding scope ambiguities and pronoun resolu-
tion, this is true of all translations of E2V sentences. We note in passing
that formula (5) does not lie in the guarded fragment.
2.1. Syntax
The syntax of E2V has four components: a grammar, a lexicon, a
movement rule and a set of indexing rules.
Grammar
The grammar of E2V consists of a set of denite clause grammar (DCG)
rules, for example:
4 Ian Pratt-Hartmann
exive(A,I)
every
Re
does not
a) Grammar b) Closed-class lexicon

Figure

1. The syntax of E2V
with the labels IP, NP, etc. indicating categories of phrases in the
usual way. The variable expressions A, B and B/A in these rules unify
with semantic values, which represent the meanings of the phrases in
question; and the variables I and J unify with indices, which regulate
variable bindings in those meanings. Semantic values are explained in
detail in section 2.2; for the present, however, think of a semantic value
of the form B/A as a function which takes B as input and yields A as
output. Thus, the rst rule above states that the semantic value of an
IP consisting of an NP and a VP is obtained by applying the semantic
value of the NP to the semantic value of the VP.
The complete grammar for E2V is given in gure 1a. We mention
in passing that, in the presentation of E2V here, the issue of pronoun
agreement in person, case and gender has been ignored. Such details
are easily handled within the framework of DCGs, and need not be
discussed further.
Lexicon
The lexicon of E2V also consists of a set of DCG rules, and is divided
into two parts: the closed-class lexicon and the open-class lexicon. The
closed-class lexicon gives the meanings of those words in our English
fragment concerned with logical form, for example:
every
Re
Two-Variable Fragment of English 5
The rst of these rules assigns the semantic value A/(B/every(A,B))
to the determiner every. It helps to think of A/(B/every(A,B)) as a
function mapping two semantic values, A and B, to the more complex
semantic value every(A,B). The second rule assigns the semantic value
A/A to any of the re
exive pronouns itself, himself and herself. This
semantic value is in eect the identity function, re
ecting the fact that
the semantic force of a re
exive pronoun is exhausted by its eect on
the pattern of indexing in the sentence (discussed below). The third
rule assigns the semantic value A/(B/(rel(A,B))) to a (covert) comple-
mentizer. Again, it helps to think of A/(B/(rel(A,B))) as a function
mapping the semantic values A and B to the more complex semantic
value rel(A,B), indicating a relative clause. The complete closed-class
lexicon for E2V is given in gure 1b.
The open-class lexicon is an indenitely large set of DCG rules for
the terminal categories N and V. These rules determine the semantic
values of words of these categories: unary predicates for nouns and
binary-predicates for verbs. The open-class lexicon might contain the
following entries:
artist
Notice how, in open-class lexicon entries, the index variables appear
as arguments in the semantic values. We assume that the open- and
closed-class lexica are disjoint.
Together, the grammar and lexicon generate sentences via successive
expansion of nodes under unication of variables in the usual way.

Figure

2 illustrates the parsing of sentence (1) using the DCG rules.
(The values x 1, x 2 for the index variables are explained below.) The
indeterminate nature of the open-class lexicon means that the English
fragment we are describing is in reality a family of fragments|one
for each choice of open-class lexicon. What these fragments have in
common is just the overall syntax and the xed stock of 'logical' words
in the closed-class lexicon. This is exactly the situation encountered in
logic, where fragments of rst-order logic are dened over a variable
signature of non-logical constants. We call an open-class lexicon a vo-
cabulary, and, for a given choice of vocabulary, we speak of the English
fragment E2V over that vocabulary.
6 Ian Pratt-Hartmann
despises
artist
Every
beekeeper
every

Figure

2. Phrase-structure of sentence (1).
Movement rule
The simplied grammar of E2V allows us to state the usual rule for
wh-movement with marginally less technical apparatus than usual. We
take one phrase to dominate another in a sentence of E2V if the second
is reachable from the rst by following zero or more downward links in
the phrase-structure of the sentence.
Denition 1. A phrase  of category NP c-commands a phrase
of
category RelPro in a parsed E2V sentence if the parent of  dominates
, but  itself does not dominate
The movement rule of E2V is:
Every phrase  of the form RelPro(A,I) moves to the position
immediately below a nearest phrase of form NP(empty,I) which c-commands
moreover, every node NP(empty,I) is the destination
of such a movement.
As usual, we speak of an NP from which a RelPro has been moved as a
trace NP. Figures 4 and 5 illustrate how this movement rule is applied
in the case of sentences (3) and (4).
It is important to uderstand the variables I and A mentioned in the
movement rule. The index variable I occurs twice: once in the moved
RelPro and once in the NP it is moved to. This is to be understood as
requiring that the index variables for these phrases must unify. Given
the further unications of indices forced by the grammar rules, the
movement rule thus has the eect of unifying the index variable of a
trace NP in a relative clause with the index variable of the NP which
that relative clause modies. By contrast, the variable A, representing
the semantic value of the moved RelPro, occurs only once in the move-
Two-Variable Fragment of English 7
ment rule. This means that the movement rule imposes no constraints
on A, and, in eect, does not care about the semantic value of the moved
RelPro. However, this semantic value has not been wasted, because the
rules
which (who, whom)
used in the construction of the relative clause force the semantic value
of a trace NP to be the identity function A/A. The combined eect
of these rules on the semantic values of relative clauses can be seen in
gures 4 and 5.
Indexing rules
In the grammar of E2V, most phrasal categories have exactly one index
variable; and in that case, we speak of the value of that variable during
parsing as being the index of the phrase in question. We insist that
every index variable in a phrase-structure tree of an E2V sentence be
assigned one of the values x 1, x 2, . For example, in the parse
displayed in gure 2, the NP every artist, the N 0 artist and the VP
despises every beekeeper all have x 1 as their index. (Two phrases with
the same index are said to be coindexed.) The assignment of values to
index variables must of course conform to the unications enforced by
the DCG rules. However, indices of NPs are additionally required to
obey a set of indexing rules, which function so as to regulate the use
of pronouns and re
exives. Sequences of words corresponding to parse
trees where the index variables cannot be assigned values in accordance
with the indexing rules fail to qualify as E2V sentences.
Within the transformational tradition, the use of Pronouns and
Re
exives is accounted for by binding theory; and that is the theory
which we adopt for E2V. No particular fealty to one linguistic school is
hereby implied: for our purposes, this strategy is simply a convenient
way to ensure that our grammar conforms to normal English usage.
The indexing rules are divided into two classes: the natural indexing
rules and an the articial indexing rules. The natural indexing rules
are:
I1: Indices of NPs must obey all the usual constraints of binding
theory
I2: No two Ns may be coindexed.
Readers unfamiliar with government and binding theory are referred
to a a standard text on the subject e.g. Cowper (1992), p. 171. Using the
standard technical terminology, these rules state that: a Re
exive must
8 Ian Pratt-Hartmann
artist
Every
admires
himself

Figure

3. Phrase-structure of sentence (2), illustrating re
exive pronouns.
be A-bound within its minimal governing category; a Pronoun must be
A-free within its minimal governing category; and an R-expression must
be A-free. Because of the limited grammar of E2V, the ner points of
binding theory may be ignored here. We remark that, in E2V, the
minimal governing category of a Pronoun or Re
exive is always the
nearest IP dominating it.
Sentences (1){(3) illustrate the eect of rule I1. Consider rst sentence
(1), containing the two nouns artist and beekeeper. Its phrase-structure
is shown in gure 2. The requirement that an R-expression be
A-free forces the indices of these nouns to be distinct. The unications
enforced by the grammar rules then imply that the two indices of the
verb despises are distinct, and that the whole sentence has the semantic
value shown, up to renaming of indices. Consider now sentence (2),
containing the single noun artist and the re
exive pronoun himself. Its
phrase-structure is shown in gure 3. The requirement that a Re
ex-
ive be A-bound in its minimal governing category forces himself and
every artist to have the same index. The unications enforced by the
rules then imply that the two indices of the verb admires are
identical, and that the whole sentence has the semantic value shown,
up to renaming of indices. Consider nally sentence (3), containing the
two nouns artist and beekeeper as well as the pronoun him. Its phrase-structure
is shown in gure 4. The requirement that a pronoun be
A-free in its minimal governing category prevents him from coindexing
with beekeeper, but allows it to coindex with artist, resulting in the
semantic value shown.
The status of rule I2 is rather dierent. Though not part of standard
binding theory, it is consistent with it. That is: given an assignment of
indices to an E2V sentence obeying rule I1, we can always rename
indices of some NPs if necessary in such a way that rules I1 and I2
are both satised. (This is straightforward to verify.) As we shall see in
Two-Variable Fragment of English 9
Every
beekeeper
despises
whom
admires
some artist

Figure

4. Phrase-structure of sentence (3), illustrating pronouns and movement.
section 2.2, rule I2 allows us to state the semantics for E2V in a very
simple way.
Having dealt with the natural indexing rules, we move on to the
articial indexing rules. These are:
I3: Every pronoun must take an antecedent in the sentence in which
it occurs
I4: Every pronoun must be coindexed with the closest possible NP
consistent with rules I1{I3.
In I4, 'closest' means `closest in the phrase-structure', not 'closest in
the lexical order'.
These rules are articial in that they make no attempt to describe
natural English usage. In particular, rule I3 requires that all anaphora
be resolved intrasententially. Clearly, this constitutes a restriction on
normal English usage, and is introduced in order to simplify the language
we are studying. Rule I4 is rather more interesting. The eect
of this rule can be seen by examining sentence (4), containing the
nouns artist, beekeeper and carpenter, and the pronoun him. Its phrase-structure
is shown in gure 5. Rules I1{I3 permit the pronoun him
Ian Pratt-Hartmann
to coindex with either artist or carpenter (but not beekeeper), corresponding
to a perceived (anaphoric) ambiguity in the English sentence.
However, we see from gure 5 that the NP every artist who employs a
carpenter is closer to the pronoun in the phrase-strcuture than the NP
a carpenter is. Hence, rule I4 requires him to coindex with the former,
and results in the semantic value shown. Rule I4 does not change the
set of strings accepted by the fragment E2V; but it does ensure that
any accepted string has a unique indexation pattern up to renaming.
It also plays a crucial role in restricting the expressive power of E2V
to that of the two-variable fragment of rst-order logic.
We say that a string of words is an E2V-sentence (over a given
vocabulary) if, according to the above syntax, it is the list of terminal
nodes below an IP node with no parent.
2.2. Semantics
Having dened the set of E2V sentences over a given vocabulary, we
now turn to the translation of these sentences into rst-order logic.
We have already seen that the syntax of E2V assigns a semantic
value to every E2V sentence. This semantic value is a complex term
formed from the primitives occurring in the vocabulary by means of
the constructors some(A,B), every(A,B), rel(A,B) and not(A). For ex-
ample, we see from gures 2{5 that sentences (1){(4) are assigned the
respective semantic values:
artist(x 1)),
To complete the semantics for E2V, it suces to dene a function
mapping semantic values of E2V sentences to formulas of rst-order
logic. The key idea behind this translation is that indices x 1, x 2, . in
semantic values can simultaneously be regarded as variables x 1
in formulas. (The dierent styles of writing indices/variables help to
make semantic values and formulas more visually distinct.)
Denition 2. Let A be the semantic value of an E2V-sentence, and let
B be any (not necessarily proper) subterm of A. We dene the function
T from such subterms to formulas of rst-order logic as follows:
Two-Variable Fragment of English 11
artist
who
employs
a
carpenter
beekeeper
every
despises
who
admires
Every

Figure

5. Phrase-structure of sentence (4).
z is the
tuple of indices which are free variables in T(C) ^T(D) but which
do not occur in A outside B
z is
the tuple of indices which are free variables in T(C) ! T(D) but
which do not occur in A outside B
T5: Otherwise,
We then take the translation of the semantic value A to be simply
(A).
Under these translation rules, the semantic values (9){(12) of the
sentences (1){(4) translate to the formulas (5){(8). To see how this
translation works in detail, consider rst sentence (1) and its semantic
value (9). The simple subterms artist(x 1), beekeeper(x 2) and de-
spise(x 1,x 2) translate to the atomic formulas artist(x 1
and respectively, by rule T5. The complex subterm
then translates to the formula
by rule T2, because, of the two free variables in question, namely x 1 and
only the latter satises the condition that it does not occur outside
the subterm. Finally, the whole expression (9) translates to (5), again
by rule T2.
We note that, in some applications of rule (and indeed, with the
grammar as presented above, some applications of rule T2), the tuple
z may be empty, in which case, of course, 9v is understood to be absent
altogether. Consider sentence (3) and its semantic value (11). Here, the
subterm
translates to the (unquantied) formula
Two-Variable Fragment of English 13
by rule T1, because, of the two free variables in question, namely x 1
and x 2 , both occur in (11) outside the subterm. Suitable applications
of rules T2 and T3 generate the nal translation (7).
2.3. Further remarks on the syntax and semantics of E2V
Relation to DRT
An alternative and more general approach to the semantics of anaphoric
constructions found in E2V is provided by Discourse Representation
Theory (DRT) (Kamp and Reyle (1993)). Like the semantics presented
above, DRT in eect employs a two-stage approach in translating from
English to rst-order logic. First, English sentences are mapped to so-called
Discourse Representation Structures (DRSs)|a formal representation
language with nonstandard mechanisms for quantication|and
these DRSs can then be translated into formulas of rst-order logic in
accordance with the standard semantics for the DRS language. This
two-stage approach allows DRT to give an account of the variable-binding
encountered in sentence (3) very similar to that given in this
paper. An elegant and technical account of DRT-style semantics for a
fragment of English similar to E2V can be found in Muskens (1996).
The main dierence between our approach and that of DRT concerns
the point at which quantiers corresponding to indenite articles are in-
troduced. Our rule translates the indenite article as an existential
quantier provided that the variable which the quantier would bind is
not going to end up appearing outside its scope in the resulting formula.
The strategy of DRT, by contrast, is that the indenite article does not
introduce a quantier at all: rather, 'left-over' variables corresponding
to these determiners are gathered up by quantiers introduced in the
interpretation of DRSs.
For example, consider the sentence
Every artist who admires a beekeeper who berates a carpenter
despises himself.
On our approach, sentence (17) has the semantic value
beekeeper(x 2)),
admire(x 1,x 2)),
artist(x 1)),
despise(x 1,x 1))
which then translates to
14 Ian Pratt-Hartmann
By contrast, DRT would assign (17) the DRS
which then translates to
Formulas (19) and (21) are, of course, logically equivalent. How-
ever, there is a dierence in the way variables are used: our approach
quanties x 2 and x 3 as early as possible, while DRT does so as late as
possible. It turns out that this strategy of early quantication means
that we use variables more 'eciently' than DRT does; and that is why
the semantics presented here makes the expressiveness of E2V easier
to determine. Thus, we are not (as far as we know) taking issue with
DRT; rather, we are simply presenting the semantics of E2V in a form
which is more convenient for the issues at hand.
Accessibility
One respect in which our semantics for E2V fails to do justice to
English speakers' intuitions concerns pronoun accessibility. Consider
again sentence (3), repeated here as (22):
Every beekeeper whom an artist despises admires him.
Recall that we assume all anaphora to be resolved intrasententially,
so that the pronoun in this sentence takes the NP an artist as its an-
tecedent. However, the availability of this NP as an antecedent depends
on the fact that it is existentially quantied. Thus, in the sentence
Every beekeeper whom every artist despises admires him,
Two-Variable Fragment of English 15
the anaphora cannot be resolved intrasententially: the admired individual
must have been introduced by some earlier sentence in the discourse.
Thus, we might say that the NP every artist in (23) is inaccessible to
the pronoun which follows it. An adequate grammar for a restricted
fragment of English should rule out sentences in which pronouns are
required to take inaccessible antecedents. It is thus a defect of the above
grammar for E2V that sentence (23) is accepted, and|as the reader
may verify|translated into the same formula as sentence (22)!
Accessibility restrictions are discussed in detail within the frame-work
of DRT; and we have nothing to add to their proper treatment in
a grammar of English. However, this issue may be safely ignored for the
purposes of the present paper, because the argument in section 4 shows
that no reasonable accessibility restrictions could reduce the expressive
power of E2V. Thus, to simplify the proofs in the following sections,
we take E2V to include sentences such as (23), condent that their
eventual exclusion will make no dierence to our results.
Quantier scoping
Another respect in which E2V fails to do justice to English speak-
ers' intuitions is quantier rescoping. It is generally claimed that the
sentence
Every artist despises a beekeeper
is ambiguous between two choices for the scoping of the quantiers.
By contrast, the above semantics unambiguously assigns wide scope
to the universal quantier. We do not consider quantier rescoping in
this paper. Generally, proposals for controlled languages eliminate such
ambiguities by stipulating that quantiers scope in a particular way;
and this is the approach we take. Very roughly, the eect of the above
grammar rules is that the quantier introduced by the subject determiner
outscopes the quantier introduced by the object determiner,
and that the quantier introduced by any NP determiner outscopes
those introduced in any relative clauses within that NP. This policy
seems the most sensible default in those cases where a choice has to be
made.
Negation
The primary mechanism in E2V which provides negation is the category
Neg, whose sole member is the two-word phrase does not. For example,
the sentence
Some artist does not despise every beekeeper
is assigned the semantic value
Ian Pratt-Hartmann
which then translates to
A more sensitive account of the semantics of E2V would complicate
the rules regarding negation in two related respects. First, the eect of
negation on verb-in
ection should be taken into account; second, the
word does should be assigned category I, with the single word not taken
to be the representative of the category Neg. These changes can be
eected by adopting the following grammar rules for IP (with variables
suppressed for readability):
I
I
and by subjecting verbs in unnegated sentences to movement into the
I position, where they are joined to the in
ection.
Negation brings with it some additional complications concerning
scoping and the negative polarity determiner any. Again, scoping ambiguities
are resolved by at. Simplifying somewhat, the above translation
rules take the negation in a NegP to outscope quantication within the
NegP, but to be outscoped by quantication in the subject governing
that NegP, as in sentence (25). Again, this seems to be the most
reasonable default.
Negative polarity is ignored altogether in this paper. Thus for ex-
ample, E2V employs
Some artist does not despise a beekeeper,
rather than the less ambiguous-sounding
Some artist does not despise any beekeeper,
to express
Other negative sentences accepted by E2V are somewhat awkward, for
example:
Every artist does not despise a beekeeper,
which translates to
Two-Variable Fragment of English 17
In keeping with the general desire to remove ambiguity from controlled
languages, it might be important to consider fragments of English
from which sentences such as (28) and (31) are either replaced
by sentences involving negative polarity items or excluded altogether.
However, as with the issue of pronoun accessibility, so too with that of
negation, the restrictions in question can be ignored for the purposes of
the present paper. The argument in section 4 shows that no reasonable
restrictions on the use of negation could reduce the expressive power of
E2V. Thus, to simplify the proofs in the following sections, we take E2V
to include sentences such as (28) and (31), condent that their eventual
exclusion or modicatation will make no dierence to our results.
Our fragment E2V includes one further mechanism for introducing
negation, namely, the determiner no. This addition to the closed class
lexicon is a small concession to naturalness of expression. In fact, it
could be dropped from E2V without aecting its expressive power.
2.4. Implementation
The foregoing specication of E2V was couched in terms which permit
direct computer implementation. In particular, the DCG rules of the
grammar and lexicon in gure 1 map almost literally to Prolog code,
with some minimal extra control structure required to implement the
indexing rules I1{I4. The movement rule can be incorporated into
this DCG using standard argument-passing techniques, for example,
as described in Walker et al. (1987), pp. 351 . Implementation of
the translation rules T1{T5 is routine. All semantic values and rst-
order translations of E2V sentences given in this paper are the unedited
output of a Prolog program constructed in this way. This program also
incorporates standard DRT accessibility restrictions and enforces correct
verb-in
ections in negated and unnegated sentences, as discussed
in section 2.3. Inspection of this program shows that the rst-order
translation of an E2V sentence can in fact be computed in linear time.
Hence the complexity of translation from E2V is not an issue we shall
be concerned with in the sequel.
3. Expressiveness: upper bound
The main result of this section states that, essentially, the translations
of E2V-sentences remain inside the two-variable fragment of rst-order
logic. In the sequel, we denote the set of formulas of rst-order logic
by L, and the set of formulas of the two-variable fragment by L 2 . The
following notion captures what we mean by \essentially" in the sentence
before last.
Ian Pratt-Hartmann
Denition 3. If  2 L, we say that  is two-variable compatible (for
short: 2vc) if no proper or improper subformula of  contains more
than two
We have the following result.
Lemma 1. Every 2vc formula is equivalent to a formula of L 2 .
Proof. Routine.
The property of being a 2vc formula is not closed under the relation of
logical equivalence. For example, formulas (19) and (21) are logically
equivalent, but only the former is 2vc. Indeed, this example shows why
our approach to the semantics for E2V makes for an easier analysis of
expressive power than that of DRT.
The result we wish to establish in this section is:
Theorem 1. If  is an E2V-sentence with semantic value A, then T(A)
is a closed 2vc formula.
To avoid unnecessary circumlocutions, if  is a phrase with semantic
value B, then we say that  translates to the formula T (B). Our strategy
will be to show that, if  is any phrase in , then  translates to a 2vc
certain constraints. For clarity, we
henceforth display all possible free variables in formulas. Thus, (x; y)
has no free variables except for (possibly) x and y, (x) has no free
variables except for (possibly) x, and so on.
A word is in order concerning the treatment of negation in this
section. Inspection of the grammar rules concerning NEGP
and the translation rule
makes it clear that NEGP-phrases merely serve to insert negations into
the translations of E2V sentences, and have no other eect on their
quanticational structure. In establishing theorem 1, then, we omit
all mention of NEGP-phrases, since their inclusion would not aect
the results we derive. This omission applies to all the lemmas used to
derive theorem 1, and serves merely to keep the lengths of proofs within
manageable bounds.
The following terminology will prove useful:
Two-Variable Fragment of English 19
Denition 4. Let  and
be phrases in an E2V sentence and Y a
category (e.g. or VP). Then
is said to be a maximal Y
(properly) dominated by  if
is a Y (properly) dominated by  and
no other phrase which is a Y (properly) dominated by  dominates
A phrase  of category X or VP) is said to be pronomial
if a maximal NP dominated by  expands to a Pronoun.
A VP  is said to be re
exive if the maximal NP dominated by
expands to a Re
exive.
A VP  is said to be trace if the maximal NP dominated by  expands
to a RelPro which has been subjected to movement.
The following examples should help to clarify these denitions (t indicates
a moved RelPro):
pronomial VP admires him
pronomial N 0 beekeeper whom he despises t
beekeeper who t admires him
re
exive VP despises himself
trace VP admires t
We also need some terminology to deal with so-called donkey-sentences.
For the purposes of E2V, we may dene:
Denition 5. A pronomial E2V sentence|that is, one where the object
of the main verb is a pronoun|is called a donkey sentence, and
the pronoun in question is called its donkey pronoun. In addition, a
phrase  of category X or VP) is said to be donkey if it
is a maximal phrase of category X dominated by the subject NP of a
donkey sentence.
The paradigm donkey-sentence is:
Every farmer who owns a donkey beats it.
Within this sentence, the following donkey phrases occur:
donkey N 0 farmer who t owns a donkey
donkey IP t owns a donkey
donkey VP owns a donkey.
It is clear that a donkey sentence contains exactly one donkey N 0 , IP
and VP. We remark that a phrase may be both pronomial and donkey,
for example, the italicized N 0 in the sentence:
Every farmer who owns a donkey which likes him beats it,
Ian Pratt-Hartmann
which, incidentally, translates to the 2vc formula:
Finally, the following notation will be useful:
Denition 6. If  is a phrase of category N 0 or VP, we write ind() to
denote the index of . If  is a phrase of category IP, but not a sentence,
we write ind() to denote the index of the NP which is moved out of
by the movement rule, and we refer to ind() informally as the index
of .
A word of warning is in order about the notation ind(). According to
the grammar of E2V, if  is an IP, then  has no index. Yet denition 6
nevertheless allows us to write ind() for a non-sentence IP . We have
adopted this notation to re
ect the fact that, from a semantic point of
view, the index of the NP moved out of  is always a free variable in
the translation of . Doing so helps to simplify many of the lemmas
which follow.
Denition 7. Let  and
be phrases in an E2V sentence and Y a
category (e.g. or VP). Then  is said to be a minimal Y
(properly) dominating
if  is a Y (properly) dominating
and no
other phrase which is a Y (properly) dominating
is dominated by .
With this terminology behind us, we prove some auxiliary lemmas
about the grammar and translation rules.
Lemma 2. If  is a non-sentence IP, then ind() is also the index of
the minimal NP (or N 0 ) dominating .
Proof. By the unications of index variables forced by the movement
rule and the grammar rules.
Lemma 3. If  is a re
exive VP, then  translates to an atomic
formula of the form d(x; x), where
Proof. By the grammar rule
with its left sister. By rule I1, the left sister of  coindexes with the
re
exive in . Hence the semantic value of  will be a simple term of
the form d(x; x). The result then follows from T5.
Lemma 4. If  is either an N 0 , a non-sentence IP or a VP, and is
pronomial, then  translates to a 2vc formula (x; y) where
and y is the index of the pronoun contained in .
Two-Variable Fragment of English 21
d)
g: CP(A/rel(d(x,y),A),x)
d:
b:
a)
g:
c)
trace
b:
g: NP(A/A,x)
g: V(c(x,y),x,y)
trace
Pronoun
Pronoun
Pronoun

Figure

6. Structures of some pronomial, non-sentence phrases. The letters x and y
stand for indices.
Proof. If  is a VP, then  must have the structure shown in gure 6a).
Certainly,
translates to an atomic formula c(x; y), where
and y is the index of the pronoun. Then  also translates to c(x; y).
If  is a non-sentence IP, then  must have one of the two possible
structures shown in gure 6b) and c). From denition 6, ind() is the
index of the trace NP. It is then immediate that  translates to an
atomic formula of either of the forms c(x; y) or c(y; x), where
and y is the index of the pronoun contained in .
If  is an N 0 , then  must have the structure shown in gure 6d), where
the IP  is also pronomial. Let
). By lemma 2,
Certainly,
translates to some atomic formula c(x)
and by the result just obtained  translates to an atomic formula of
one of the forms d(x; y) or d(y; x). Then  translates to d(x;
or
We remark that lemma 4 holds whether or not  is donkey.
Lemma 5. Let  be either of the phrases depicted in gure 7, with
pronomial. Then the index of the pronoun in
is also the index of .
22 Ian Pratt-Hartmann
Det Det
a) b)
b:
IP
b:
g: g:
trace

Figure

7. Statement of lemma 5.
b:
Det g: N'
e:
IP
Pronoun
IP or VP
d:

Figure

8. Proof of lemma 6.
Proof. In case a), rule I4 forces the pronoun in
to coindex with the
minimal NP dominating . (There must be such an NP, because an NP
has been moved out of .) The result then follows from lemma 2. In case
b), the left-sister of  is either a full NP (expanding to a Det and N 0 )
or an NP trace which coindexes with the minimal NP dominating .
Either way, I4 forces the pronoun in
to coindex with this NP. Again,
the unications of index variables enforced by the grammar rules and
(if applicable) the movement rule ensure that  also coindexes with
this NP.
Lemma 6. Let  be an E2V sentence,  be a non-donkey phrase of
category IP or VP properly dominated by , and
a maximal N 0
properly dominated by . Then ind(
does not occur outside  in the
semantic value of .
Proof. Refer to gure 8. It is easy to check using the grammar rules that
any index occurring outside  is the index of some NP occurring outside
Two-Variable Fragment of English 23
, so that if ind(
occurs outside , it does so as the index of some
N, Re
exive or Pronoun. Rule I2 rules out the rst possibility, and I1
rules out the second. It follows that ind(
can occur outside  only
if it is the index of a pronoun . In fact, the minimal NP dominating
must be the antecedent of . Since
and hence  must precede ,
must have a minimal dominating NP, say ". By rules I2 and I4, no
full NP (expanding to a Det and N 0 ) other than " can intervene on the
path between  and
. It is then easy to see that  must be a donkey
pronoun, and that the minimal NP dominating
is its antecedent. This
contradicts the supposition that  is not donkey.
We are now ready to state the main lemma underlying theorem 1.
Lemma 7. For every phrase  such that  is either an N 0 , a non-
sentence IP or a non-trace VP, we have:
a) if  is non-donkey and non-pronomial, then  translates to a 2vc
b) if  is donkey, then  translates to a 2vc formula (x; y) where
and y is the index of the donkey pronoun.
Proof. We proceed by induction on the number of N 0 , IP or VP nodes
properly dominated by  in the phrase-structure tree for the sentence
in question.
We have three cases to consider, depending on whether  is (i) an
an IP or (iii) a VP.
(i) Let  be an N 0 , with of the lemma
are then established as follows:
a) Suppose  is non-pronomial and non-donkey. Then  is either a
single noun and so translates to, say, b(x), or is of the form depicted
in gure 9a). Since  is non-pronomial and non-donkey, so is . By
by inductive hypothesis  translates
to a 2vc formula (x). Since ind(
translates to an
atomic formula, say c(x), whence  translates to c(x) ^ (x) by
T3 as required.
Suppose  is donkey. Then  must be of the form depicted in
gure 9a), with  also donkey. By lemma 2
by inductive hypothesis  translates to a 2vc formula (x; y), where
y is the index of the donkey pronoun. Again,
translates to an
atomic formula, say c(x), whence  translates to c(x) ^ (x; y) by
T3 as required.
Ian Pratt-Hartmann
(ii) Let  be a non-sentence IP, with prevents the
subject of an IP from being a re
exive; furthermore, an IP with a pronoun
subject cannot fall under either of the cases a) or b) of the lemma.
Hence, we have two sub-cases to consider, depending on whether the
subject or the object of the IP is a trace, as depicted in gure 9b) and
c), respectively. Note: in gure 9c){e), we use the notation Q(S,T) to
denote any of some(S,T), every(S,T) and every(S,not(T)), where S and
are semantic values.
We consider rst the sub-case of gure 9b). From denition 6,
x is the index of the trace in . And by the phrase structure rules, we
have ind(
clauses a) and b) of the lemma
as follows:
a) Suppose  is non-pronomial and non-donkey. Then so is
. By
inductive hypothesis,
translates to a 2vc formula (x). But then
so does .
Suppose  is donkey. Then so is
. By inductive hypothesis,
translates to a 2vc formula (x; y), where y is the index of the
donkey pronoun. But then so does .
Next, we consider the sub-case of gure 9c). From denition 6,
x is the index of the trace in . Let
certainly,  translates
to some atomic formula d(y; x). Furthermore, from its position
in the phrase-structure,
is certainly not donkey. Suppose in addition
that it is not pronomial. Then, by inductive hypothesis,
translates to
some 2vc formula (y), which we may write as (y; x). Suppose on the
other hand that
is pronomial. Then by lemma 4, it translates to a
z is the index of the pronoun contained in
Moreover, by lemma 5, Hence
translates to (y; x).
We now establish clauses a) and b) of the lemma as follows:
a) Suppose  is non-pronomial and non-donkey. By lemma 6 then, y
does not occur outside . Depending on whether the determiner
in question is a, every or no, by T1, T2 and (possibly) T4,
translates to one of 9y(
Suppose  is donkey. By rule I4, y must be the index of the donkey
pronoun, so that both x and y occur outside . By similar
reasoning to case a),  translates to one of (
(iii) Let  be a non-trace VP, with
is re
exive, it translates to an atomic formula b(x; x). Moreover, no
Two-Variable Fragment of English 25
donkey VP can be re
exive (otherwise the donkey pronoun would have
no antecedent). For the purposes of establishing clauses a) and b) of
the lemma then, we may assume that  is not re
exive. Furthermore,
if  is donkey, then it cannot be pronomial, for then there would be
no antecedent for the pronoun in . Again, then, for the purposes of
establishing clauses a) and b) of the lemma, we may assume that  is
not pronomial, so we can take  to have the form depicted in gure 9d).
translate to the atomic formula c(x; y). By its
position in the phrase-structure,  is not donkey. If, in addition,  is not
pronomial, by inductive hypothesis, it translates to a 2vc formula (y),
which we may write as (y; x). If, on ther other hand,  is pronomial,
by lemma 4, it translates to a 2vc formula (y; z), where z is the index
of the pronoun contained in . Moreover, by lemma 5,
Hence  translates to (y; x). We now establish clauses a) and b) of
the lemma as follows:
a) Suppose  is not pronomial, and not donkey. By lemma 6, y does not
occur outside . Depending on whether the determiner in question
is a, every or no, by T1, T2 and (possibly) T4,  translates to
one of 9y(
:c(x; y)), as required.
Suppose  is donkey. By rule I4, y must be the index of the donkey
pronoun, so that x and y both occur outside . By similar
reasoning to case a),  translates to one of (
Now we can return to the main theorem of this section.
Proof of theorem 1. Let the sentence  have the structure shown in
gure 9e), and let
rst that  is non-
donkey. Then
and  are non-pronomial and non-donkey, and  is
certainly non-trace. By lemma 7,
and  translate to 2vc formulas
(x) and (x) respectively. Since  has no parent, by T1 and T2 and
(possibly) T4, it translates to one of 9x((x)^ (x)), 8x((x) ! (x))
or
Suppose on the other hand that  is donkey. By lemma 7,
translates
to a 2vc formula (x; y), where y is the index of the donkey pronoun.
By lemma 4,  translates to a formula (x; y). Again, since  has
no parent, by T1 and T2 and (possibly) T4, it translates to one of
26 Ian Pratt-Hartmann
a) b) c)
d) e)
RelPro
C'
trace
Det d:
Det
d:
b:
g:
b:
b:
d:
g:
b:
g:
a:
g:
IP(T)
Det N'(S,y)
g:
d:
trace

Figure

9. Proofs of lemma 7 and theorem 1. The letters S and T stand for semantic
values.
The following result gives us an upper complexity bound for E2V-
Theorem 2. (Borger, Gurevich and Gradel (1997) corollary 8.1.5) The
problem of deciding the satisability of a sentence in L 2 is in NEXP-
TIME.
Corollary 1. The problem of determining the satisability of a set E
of E2V sentences is in NEXPTIME.
4. Expressiveness: lower bound
In the previous section, we showed that the English fragment E2V does
not take us beyond the expressive power of the two-variable fragment.
In this section, we show that, with two minor semantic stipulations, we
essentially obtain the whole of the two-variable fragment.
The rst semantic stipulation concerns the expression of identity.
The identiy relation is not expressible in E2V, and so we need to single
out a verb|eqs|which will be mapped to the identity relation. That
is, we have the lexicon entry
Two-Variable Fragment of English 27
eqs.
The second semantic stipulation concerns the expression of the universal
property. All noun-phrases in E2V contain common nouns, which
automatically restricts quantication in sentence-subjects. It is therefore
convenient to single out a noun|thing|which expresses the property
possessed by everything. That is, we have the lexicon entry
thing.
For ease of reading, we will perform the usual contractions of every
thing to everything, some thing to something etc. We note that both
semantic stipulations can be dropped without invalidating corollaries 2
and 3 below.

Table

I. Some formulas of L 2 and their E2V-translations
Everything bees everything which ays it
Everything which ays something bees itself
Everything which something ays bees itself
Everything which bees itself ays everything
Everything ays everything which bees itself
Everything which ays something eqs a bee
Everything which something ays eqs a bee
everything
Everything ays every bee
Nothing bees something which it ays
Everything bees everything which it ays
8x8ya(x;y) Everything ays everything
8x9ya(x;y) Everything ays something
Everything ays everything which it does not bee
Everything which bees something which it cees
ays it
To understand how E2V can essentially express the whole of the
two-variable fragment, we need to establish an appropriate notion of
expressive equivalence.
Denition 8. Let ;  0 2 L. We say that  0 is a denitional equivalent
of  if  0 structure A interpreting only the non-logical
primitives of  such that A j= , there is a unique expansion B of A
such that B
It is obvious that, if  0 is a denitional equivalent of , then  is
satisable if and only if  0 is satisable. We show that, for any closed
28 Ian Pratt-Hartmann
formula  in the two-variable fragment, a set E of E2V sentences can
be found such that E translates to a set of formulas whose conjunction
is a denitional equivalent of .
First, we establish an easy result about the two-variable fragment.
Lemma 8. There is a function f : computable in polynomial
time and space, such that, for all  2 L 2 , f() is a denitional
equivalent of  consisting of a conjunction of formulas of the forms
found in the left-hand column of table I, where the a, b and c are
relation-symbols of the indicated arity.
Proof. Let  2 L 2 . Using the well-known transformation due to Scott
(see, e.g. Borger, Gurevich and Gradel (1997), lemma 8.1.2), we can
compute, in polynomial time and space, a formula  0 of the form
where the  i (0  i  m) are quantier-free, such that  0 is a deni-
tional equivalent of . Using the same technique, we may then compute,
again in polynomial time and space, a formula  00 which is a conjunction
of formulas of the forms found in the left-hand column of table I,
such that  00 is a denitional equivalent of  0 . Details of this second
transformation may be found in Pratt-Hartmann (2000), lemma 8, but
are completely routine.
Theorem 3. Let  be in L 2 . Then we can compute, in polynomial
time and space, a set E of sentences in E2V, such that E translates to
a set of sentences whose conjunction is a denitional equivalent of .
Proof. Compute f() as in lemma 8. The formulas in the left-hand
column of table I are, modulo some trivial logical manipulation, the
translations of the corresponding E2V sentences in the right-hand col-
umn. (This fact has been veried using the Prolog implementation
mentioned in section 2.4.) Thus, we can read o the E2V translations
of each conjunct in f() from table I.
At this point, we are in a position to return to remarks made in
section 2.3 concerning possible restrictions of (or modications to) E2V.
In particular, we claimed that imposing standard pronoun accessibility
restrictions (thus outlawing certain currently legal E2V sentences)
would not reduce the fragment's expressive power. That this is so follows
immediately from consideration of table I, since all the sentences
occurring there are perfectly acceptable English sentences in which
anaphora can be resolved intrasententially, and so could not possibly
violate any (reasonable) accessibility restrictions.
Two-Variable Fragment of English 29
Similarly, we claimed in section 2.3 that banning some very awkward
negative sentences or insisting on the use of negative polarity determiners
would also not aect the expressive power of E2V. But we see that
the only faintly objectionable piece of English in table I occurs in the
row
Nothing bees something which it ays
where, arguably, something should be replaced by anything. But any
reasonable modication of E2V along these lines must surely assign
the meaning 8x8y(a(x; y) ! :b(x; y)) to the sentence Nothing bees
anything which it ays, in which case, the proof of theorem 3 would
proceed as before. Thus, no reasonable|i.e. linguistically motivated|
modication of the way negative sentences are treated in E2V could
lead to a reduction in expressive power.
The following well-known result gives us a lower complexity bound
for E2V-satisability:
Theorem 4. The problem of deciding the satisability of a formula in
A proof can be found in Borger, Gurevich and Gradel (1997), theorem
6.2.13. What these authors actually show is that the domino
problem for a toroidal grid of size 2 n can be polynomially reduced to
the satisability problem for L 2 . But the former problem is known to
be NEXPTIME-hard.
This gives us an immediate bound for the complexity of reasoning
in E2V:
Corollary 2. The problem of determining the satisability of a set E
of E2V sentences is NEXPTIME hard.
In fact, if complexity (rather than expressive power) is all we are interested
in, we could do much better than this. Referring to denition 8,
dropping the requirement that the expansion B be unique still guarantees
that  and  0 are satisable over the same domains. By taking
care to move negations inwards in the  i in formula (36), we can optimize
the transformations in the proof of lemma 8 so that the resulting
conjunction  00 makes no use of the formulas below the horizontal line
in table I, while still guaranteeing that  and  00 are equisatisable.
Since there is no mention of the word not in the corresponding E2V
translations, we have:
Denition 9. Denote by E2V 0 the fragment of English dened in exactly
the same way as for E2V, but with all grammar rules involving
NegP removed.
Ian Pratt-Hartmann
Corollary 3. The problem of determining the satisability of a set E
of E2V 0 sentences is NEXPTIME hard.
Of course, E2V 0 still contains the negative determiner no.
We remark that theorem 4 also holds for the two-variable fragment
without equality. It is then routine to show that the assumptions that
thing denotes the universal property and eqs expresses the identity
relation can both be dropped without invalidating corollary 3. We
remark in addition that theorem 4 applies only when no restrictions are
imposed on the non-logical primitives that may occur in formulas of L 2 .
For formulas of L 2 over a xed signature, the satisability problem is in
NP. Corresponding remarks therefore apply to E2V when interpreted
over a xed vocabulary.
It is natural to ask what happens when the articial indexing rule
I4 is removed. In this case, additional patterns of indexing are allowed
for a given string of words in E2V, resulting in increased expressive
power. Consider again sentence (4), repeated here as (37),
Every artist who employs a carpenter despises every beekeeper
who admires him.
As we remarked above, rules I1{I3 allow the pronoun to coindex with
either artist or carpenter, while rule I4 forbids the latter possibility.
But what if we abolished I4 and allowed all (intrasentential) anaphoric
references conforming to the usual rules of binding theory? For sentence
(37), this would result in the possible semantic value:
artist(x 1)),
Let us apply the standard translation rules T1{T5 to this semantic
value. (Our translation rules in no way depend on the adoption of
rule I4.) The result is the formula
We mention in passing that the Prolog implementation discussed in
section 2.4 has been so written that the rst solution it nds corresponds
to an indexing pattern conforming to I1{I4, and that subsequent
solutions, obtainable by backtracking in the normal way, are those for
other indexation patterns, if any, conforming only to I1{I3.
Formula (39) is clearly not 2vc. Does this make a dierence? Unfor-
tunately, it does: Pratt-Hartmann (2000) shows that the satisability
Two-Variable Fragment of English 31
problem for E2V without rule I4 is undecidable. Actually, that paper
establishes a slightly stronger result: even if all negative items
(the determiner no and the rules for NegP) are removed from the
grammar, without rule I4, the problem of determining whether one
set of sentences entails another is also undecidable. The techniques
used are similar to those employed in this section, though somewhat
long-winded. Here, we simply state without proof:
Theorem 5. If the indexing rule I4 is removed from E2V, the problem
of determining the satisability of a set of E2V sentences (with specied
indexing patterns) is undecidable.
We conclude that the articial indexing rule I4 really is essential in
enforcing decidability.
Many useful extensions to E2V could be straightforwardly implemented
without essential change to the corresponding logical frag-
ment. Extensions in this category include proper nouns, intransitive
verbs, (intersective) adjectives, as well as some special vocabulary|
most obviously, the verb to be. Other useful extensions would be equally
straightforward to implement, but would, however, yield a fragment of
logic for which the satisability problem has higher complexity. The
most salient of these is the extension of the closed-class lexicon to
include the determiner the (interpreted, say, in a standard Russellian
fashion), and possibly also counting determiners such as at least four,
at most seven, exactly three etc. Such expressions will not in general
translate into the two-variable fragment, but they will translate into
the fragment C 2 , which adds counting quantiers to the two-variable
fragment. The satisability problem for this language is shown by Pa-
cholski, Szwast and Tendera (1999) to be decidable in nondeterministic
doubly exponential time. These examples suggest a programme of work:
for a host of grammatical constructions, provide a semantics which is
amenable to the kind of analysis of expressive power undertaken above
for our original fragment E2V.
5. Natural language and formal languages
Let us say that an argument in E2V is a nite (possibly empty) set
of E2V sentences (the premises) paired with a further E2V sentence
(the conclusion). Informally, an argument is said to be valid if the
conclusion must be true whenever the premises are true. Assuming that
our semantics is a faithful account of the meanings of E2V sentences, we
may take an argument to be valid if and only if the translations of the
premises entail the translation of the conclusion, in the usual sense of
Ian Pratt-Hartmann
entailment in rst-order logic. We take this claim to be uncontentious.
Therefore, the validity of arguments in E2V is certainly decidable. The
question then arises as to the most ecient practical way of determining
the validity of arguments in E2V automatically.
The most obvious strategy is as follows: translate the relevant E2V
sentences into rst-order logic as specied in section 2; then use a
known algorithm for solving satisability problems in the two-variable
fragment. Of particular interest are algorithms based on ordered resolution
(see, for example, de Nivelle (1999), de Nivelle and Pratt-
Hartmann (2001)); such an approach enjoys the obvious engineering
advantage that it can be implemented as a heuristic in a general-purpose
resolution theorem-prover. These observations suggest that
the best way to decide the validity of arguments in E2V is to pipe
the output of an E2V parser to a resolution theorem-prover equipped
with suitable heuristics.
Historically, however, the strategy of translating natural language
deduction problems into rst-order logic and then using standard logical
techniques to solve them has always had its dissenters. Two observations
encourage this dissent: (i) that the syntax of rst-order
logic is unlike that of natural language|particularly in its treatment
of quantication|and (ii) that standard theorem-proving techniques
are unlike the kinds of reasoning patterns which strike people as most
natural. It is then but a small step to the idea that we might obtain a
better (i.e. more ecient) method of assessing the validity of arguments
if we reason within a logical calculus whose syntax is closer to that of
natural language. This idea is attractive because it suggests a naturalistic
dictum: treat the syntax of natural language with the respect it is
due, and your inference processes will run faster.
The purest manifestation of this school of thought is to give an
account of deductive inference in terms of proof-schemata which match
directly to patterns of (analysed) natural language sentences. Examples
of such natural-language-schematic proof systems are Fitch (1973),
Hintikka (1974) and Suppes (1979), as well as the work of the 'tra-
ditional' logicians such as Englebretsen (1981) and Sommers (1982).
However, it is certainly possible to accept the usefulness of translation
to a formal language, while maintaining that such a language should
be more like natural language than rst-order logic. Thus, for example,
Purdy (1991) presents a language he calls LN , a variable-free syntax
with slightly less expressive power than ordinary rst-order logic.
(Satisability in LN remains undecidable, however.) Purdy provides
a sound and complete proof procedure for LN and a grammar mapping
sentences from a fragment of English to formulas in LN . He also
Two-Variable Fragment of English 33
shows how his proof procedure can be used to solve various deductive
problems in|as he claims|a natural fashion.
The trouble with all of these systems, however, is that no hard
evidence is adduced to support their claimed superiority to the obvious
alternative of reasoning with rst-order logic translations. The work of
Purdy just cited provides a good illustration. It is clear that the very
simple natural language fragment he provides does not have the same
expressive power as LN . Indeed, Purdy's English fragment is, with some
trivial additions, less expressive than our E2V, and linguistically rather
unsatisfactory (for example, relative clauses can only have subject- and
never object-traces). It is worth remarking that the example inference
problems he gives to illustrate the 'naturalness' of his proof procedure
cannot be parsed by his grammar. We conclude that the case for LN as
an appropriate formalism for solving natural language reasoning problems
has not been established. The same goes for all of the alternative
schemes mentioned above: vague and unsubstantiated claims about the
psychological naturalness of certain reasoning procedures have little
merit.
McAllister and Givan (1992) present a much more restricted logical
language involving a construction similar to the 'window' operator of
Humberstone (1983; 1987), and specically motivated by the quantica-
tion patterns arising in simple natural language sentences. Determining
satisability in this language is shown to be an NP-complete problem|
and indeed to be solvable in polynomial time given certain restrictions.
(We remark that the computational complexity of similar, but more
expressive, languages is explored in Lutz and Sattler (2001).) McAllister
and Givan do not present a grammar corresponding to their
fragment, though it would not be dicult to write a parser for simple
sentences involving nouns (common and proper), transitive verbs, relative
clause constructions and the determiners some and every. Whether
any linguistically natural fragment of natural language could be given
which expresses the whole of McAllister and Givan's formal language
is unclear. However, McAllister and Givan's work has the great merit
of establishing a precise claim about the computational advantage of
restricting attention to their natural-language-inspired formalism.
The complexity results presented above show that no fragment of
English translating into McAllister and Givan's formalism could equal
the expressive resources of E2V. As McAllister and Givan point out,
they seem to have captured a fragment of English from which all
anaphora has been removed. Moreover, our results give us reason to
believe that no analogous natural-language-inspired formalism could
confer any computational advantages when it comes to fragments of
natural language as expressive as E2V. Section 3 establishes that we
34 Ian Pratt-Hartmann
can determine the validity of E2V arguments in nondeterministic exponential
time by adopting the straightforward strategy of translating the
relevant sentences into rst-order logic; however, section 4|and speci-
cally table I|tells us that determining the validity of arguments in E2V
is NEXPTIME-hard anyway, so that it is dicult to see how an alternative
representation language would confer any computational benet,
at least in terms of (worst case) complexity analysis. Finally, and on
a more practical note, it is important to bear in mind the diculty
of developing any reasoning procedure for the alternative formalism
which could compete with the impressive array of well-maintained and
-documented software already available for theorem-proving in rst-
order logic. Thus, we remain skeptical as to whether formal languages
whose syntax is inspired by natural language|or whose syntax just
deviates from rst-order logic in some other way|really constitute
more ecient representation languages for natural-language deduction
than does rst-order logic.
6. Conclusion
This paper has provided a study in how to match a controlled language
with a decidable logic whose computational properties are well-
understood. The controlled language we chose, E2V, was shown to
correspond in expressive power exactly to the two-variable fragment
of rst-order logic. Two features of this study deserve emphasis. The
rst is logical rigour: the syntax and semantics of E2V were presented
in such a way that results about its expressive power and computational
complexity could be established as theorems. Logical rigour
is important in the context of controlled languages, because software
support for such languages must be shown to be robust and reliable.
The second feature is conservativity: our presentation of the syntax
and semantics of E2V borrowed heavily from accepted linguistic theory
(especially in the treatment of anaphora); and our chosen logical
representation language was|in contrast to some previous work on
natural language deduction|standard rst-order logic. Conservativity
is important, because of the obvious benets of relying on well-attested
linguistic theories and well-maintained, ecient theorem-proving software

The ultimate goal of this research is to provide useable tools for natural
language system specication. Before that goal is achieved, many
questions remain to be answered, not least questions of a psychological
nature concerning the practical utility of such tools. However, the work
reported here is at least a step towards this goal. At the very least,
Two-Variable Fragment of English 35
we have demonstrated that work in formal semantics, mathematical
logic and computer science has now reached the stage where relatively
expressive controlled languages can be precisely specied and their
computational properties rigorously determined.



--R



A Consice Introduction to Syntactic Theory.


Three Logicians.











From Discourse to Logic: Introduction to Modeltheoretic Semantics of Natural Language






Linguistics and Philosophy 19(2)




The Logic of Natural language.


Knowledge Systems and Prolog: A Logical Approach to Expert Systems and Natural language Processing.
Addison Wesley.
--TR

--CTR
Ian Pratt-Hartmann, Fragments of Language, Journal of Logic, Language and Information, v.13 n.2, p.207-223, Spring 2004
controlled languages;two-variable fragment;logic;specification;natural language