On arithmetical first-order theories allowing encoding and decoding of lists

In Computer Science, n-tuples and lists are usual tools; we investigate bot h notions in the framework of first-order logic within the set of nonnegati ve integers. Godel had firstly shown that the objects which can be defined by primitive recursion schema, can also be defined at first-order, using na tural order and some coding devices for lists. Second he had proved that th is encoding can be defined from addition and multiplication. We show this c an be also done with addition and a weaker predicate, namely the coprimenes s predicate. The theory of integers equipped with a pairing function can be decidable or not. The theory of decoding of lists (under some natural cond ition) is always undecidable. We distinguish the notions encoding of n-tupl es and encoding of lists via some properties of decidability-undecidability . At last, we prove it is possible in some structure to encode lists althou gh neither addition nor multiplication are definable in this structure. (C) 1999 Elsevier Science B.V. All rights reserved.