# zbMATH — the first resource for mathematics

Theory of lists and its models. (Russian) Zbl 0646.68035
The simplest data type is that of a list. Two-type first order predicate language may formalize the notion of a list. We have atoms and lists, as the types. The function cons: Atom$$\times List\to List$$ appends an atom to a list. The theory of lists (LL) has the following axioms:
(1) ($$\alpha$$ (nil) $$\wedge (\forall x,b)$$ ($$\alpha$$ (x) $$\Rightarrow \alpha (cons(b,x))) \Rightarrow (\forall x)\alpha$$ (x),
(2) ($$\forall x)$$ ($$\forall b)$$ (nil$$\neq cons(b,x)),$$
(3) ($$\forall x,y,a,b)$$ $$(cons(a,x)=cons(b,y) \Rightarrow x=y \wedge a=b).$$
In the paper the following theorems are proved. Let LL(T) denote the theory of lists over the theory of atoms determined by the set of axioms of T plus the axioms (1)-(3). Then:
(i) if T is consistent, then LL(T) is consistent,
(ii) if LL(T) has a model with more than one atom, then LL(T) has continuum elementary equivalent countable models,
(iii) if T is complete, then LL(T) is complete.
If the theory of lists in augmented by functions “head”, “tail” and “error” with the relevant set of axioms, then the following theorem holds:
(iv) if T is complete, then the theory $$L^*(T)$$ of lists with functions “head”, “tail”, “error” has the property of quantifier elimination with respect to the type of list.
Reviewer: A.Kreczmar

##### MSC:
 68Q65 Abstract data types; algebraic specification 68Q60 Specification and verification (program logics, model checking, etc.) 03B10 Classical first-order logic 03C35 Categoricity and completeness of theories 03B70 Logic in computer science