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

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