On Arithmetical First-Order Theories allowing Encoding and Decoding of Lists
Patrick Cégielski, Denis Richard · 1998
In 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, also can be defined at first-order, using natural order and some coding devices for lists. Secondly 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 decidabilityundecidability. At last, we prove it is possible in some structure to encode lists although neither addition nor multiplication are definable in this structure. Résumé On utilise couramment en informatique les n-uplets et les listes sur un ensemble donné; nous étudions ces deux notions dans le cadre de la logique du premier ordre et pour l’ensemble des entiers naturels. Gödel a montré que les objets définis par un schéma de récurrence primitive sont définissables au premier ordre avec la relation d’ordre et le codage des listes, eux-mêmes définissable avec l’addition et la multiplication; nous montrerons que ce codage peut également s’effectuer avec l’addition et un prédicat plus faible que la multiplication, à savoir la coprimarité. On montre aussi que les notions de n-uplets et de listes se distinguent par des arguments de décidabilitéindécidabilité. La théorie des entiers munis d’une fonction de couplage peut-être-ou non- décidable. Par contre la théorie du décodage des listes, soumise à une certaine condition naturelle, est toujours indécidable. On montre enfin qu’il existe des structures dans lesquelles on peut coder les listes sans pour autant que l’addition (et donc l’ordre) et la multiplication ne soient définissables.