Various feature descriptions are being employed in logic programming l
anguages and constraint-based grammar formalisms. The common notationa
l primitive of these descriptions are functional attributes called fea
tures. The descriptions considered in this paper are the possibly quan
tified first-order formulae obtained from a signature of binary and un
ary predicates called features and sorts, respectively. We establish a
first-order theory FT by means of three axiom schemes, show its compl
eteness, and construct three elementarily equivalent models. One of th
e models consists of the so-called feature graphs, a data structure co
mmon in computational linguistics. The other two models consist of the
so-called feature trees, a record-like data structure generalizing th
e trees corresponding to first-order terms. Our completeness proof exh
ibits a terminating simplification system deciding validity and satisf
iability of possibly quantified feature descriptions.