A First-Order Axiomatization of the Theory of Finite Trees

Rolf Backofen ?
DFKI Saarbrucken
Stuhlsatzenhausweg 3
66123 Saarbrucken, Germany

James Rogers
Institute for Research in Cognitive Science
Univ. of Pennsylvania
Philadelphia, PA 19104-6228, USA

and

K. Vijay-Shanker y
Dept. of Computer and Information Science
Univ. of Delaware
Newark, DE 19716, USA

Abstract. We provide first-order axioms for the theories of finite trees with bounded branching and finite trees with arbitrary (finite) branching. The signature is chosen to express, in a natural way, those properties of trees most relevant to linguistic theories. These axioms provide a foundation for results in linguistics that are based on reasoning formally about such properties. We include some observations on the expressive power of these theories relative to traditional language complexity classes.

Key words: Trees, First-Order Theories, Axiomatizations, Natural Language Syntax, EhrenfeuchtFra?ss?e Games

1. INTRODUCTION

There has been, over the last ten or fifteen years, a growing body of research in generative and computational linguistics that depends to a great extent on reasoning formally about trees. For example, there are a number of grammatical formalisms that have been proposed that manipulate logical descriptions of the trees representing the syntactic structure of strings rather than strings or the trees themselves (Marcus et al., 1983; Henderson, 1990; Vijay-Shanker, 1992). Parsing, in these formalisms, is a process of constructing a formula that characterizes the trees that yield a given input. Recognition is the question of whether that formula is satisfiable. These formalisms, then, presuppose a means of manipulating these formulae and determining their satisfiability. In other works a logical language is used to formalize the grammatical framework itself (Johnson, 1989; Stabler, Jr.,

? The research reported in this paper has been supported by the Bundesminister fur Forschung und Technologie under contract ITW 01 IV 101 K/1 (Verbmobil).
y Part of this work was done during the period when this author was at DFKI, Saarbrucken. This author would like to thank Prof. Dr. H. Uszkoreit and Prof. Dr. W. Wahlster for providing the facilities and a supportive environment.