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

AbstractIn Computer Science, n-tuples and lists are usual tools; we investigate both notions in the framework of first-order logic within the set of nonnegative integers. Gödel had firstly shown that the objects which can be defined by primitive recursion schema, can also be defined at first-order, using natural order and some coding devices for lists. Second he had proved that this encoding can be defined from addition and multiplication. We show this can be also done with addition and a weaker predicate, namely the coprimeness predicate. The theory of integers equipped with a pairing function can be decidable or not. The theory of decoding of lists (under some natural condition) is always undecidable. We distinguish the notions encoding of n-tuples and encoding of lists via some properties of decidability-undecidability. At last, we prove it is possible in some structure to encode lists although neither addition nor multiplication are definable in this structure