On arithmetical first-order theories allowing encoding and decoding of lists. (English) Zbl 0930.68032
Summary: 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, 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.
MSC:
| 68N17 | Logic programming |
References:
| [1] | Gaillard, F., La non-contradiction de la théorie des ensembles sans axiome d’infini, (Séminaire LLAIC1, 1 (1989-1990)), 71-86, French translation by |
| [2] | French translation: Acta Math. 2, 305-310.; French translation: Acta Math. 2, 305-310. |
| [3] | Cavailles, J., Philosophie mathématique, ((1962), Hermann: Hermann Paris), 177-249, french translation by · Zbl 0105.24408 |
| [4] | Cegielski, P., Definability, decidability and complexity, Ann. Math. Artificial Intelligence, 16, 311-341 (1996) · Zbl 0865.03007 |
| [5] | Church, A., An unsolvable problem of elementary number theory, Amer. J. Math., 58, 345-363 (1936), reprinted in M. Davis (1965) 88-107 · JFM 62.0046.01 |
| [6] | (Davis, M., The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions (1965), Raven Press: Raven Press New York) · Zbl 1099.03002 |
| [7] | also Report MR33 of the Computation Department of the Mathematical Centre, Amsterdam; reprinted in Rosen, Saul, Programming Systems and Languages, McGraw-Hill, New York, 19XX XV + 734 pp., pp. 221-227.; also Report MR33 of the Computation Department of the Mathematical Centre, Amsterdam; reprinted in Rosen, Saul, Programming Systems and Languages, McGraw-Hill, New York, 19XX XV + 734 pp., pp. 221-227. · Zbl 0093.13911 |
| [8] | Enderton, H. B., A Mathematical Introduction to Logic, ((1972), Academic Press: Academic Press New York), XIII + 295 · Zbl 0298.02002 |
| [9] | (Le théorème de Gödel (1989)), 105-143, Seuil · JFM 57.0054.02 |
| [10] | Gödel, K., (Collected Works, Vol. 3 (1995), Oxford University Press: Oxford University Press Oxford) |
| [11] | Gödel, K., Letter to Zermelo dated 12 October 1932, (Grattan-Guinness, Historia Mathematica, Vol. 6 (1979)), 294-304 |
| [12] | Gaillard, F.; Guillaume, M., (Fondements des mathématiques, 1 (1997)), 394, French translation by |
| [13] | Gaillard, F.; Guillaume, E.; Guillaume, M., (Fondements des mathématiques, vol. 2 (1997)), 395, French translation by |
| [14] | Korec, I., A list of arithmetical structures strongest with respect to the first order definability, (preprint 33 (1996), Mathematical Institute Slovak, Academy of Sciences: Mathematical Institute Slovak, Academy of Sciences Bratislava), Theoret. Comput. Sci., to appear · Zbl 0971.03035 |
| [15] | Langford, C. H., Some theorems on deducibility, Ann. Math., 28, 459-471 (1926) · JFM 53.0043.05 |
| [16] | Horowitz; Ellis, Programming Languages: A Grand Tour, ((1987), Computer Science Press: Computer Science Press Rockville, MD), 203-214 |
| [17] | Maurin, F., The theory of integer multiplication with order restricted to primes is decidable, Symbolic Logic, ((1994)), 184-195 |
| [18] | Zygmunt, J., History and Philosophy of Logic, vol. 12, 211-233 (1991), English translation and study by |
| [19] | Quine, W. V.O., Concatenation as a basis for arithmetics, Symbolic J. Logic, 11, 105-114 (1946) · Zbl 0063.06362 |
| [20] | Richard, D., The arithmetics as theories of two orders, Ann. Discrete Math., 23, 287-312 (1984) · Zbl 0555.03026 |
| [21] | Richard, D., Définissabilité en Arithmétique et méthode de codage ZBV appliquée à des langages avec successeur et coprimarité, (Thèse d’État (1985), Université Lyon-I), n.85-16 |
| [22] | Richard, D., Answer to a problem raised by J. Robinson: the arithmetic of positive or negative integers is definable from successor and divisibility, J. Symbolic Logic, 50, 135-143 (1985) |
| [23] | Richard, D., Equivalence of some questions in mathematical logic with some conjectures in number theory, (Mollin, Number Theory and Applications. Number Theory and Applications, NATO Asi Series Series C: Mathematical and Physical Sciences, vol. 265 (1988)), 529-545 · Zbl 0685.03040 |
| [24] | Richard, D., Definability in terms of the successor function and the coprimeness predicate in the set of arbitrary integers, J. Symbolic Logic, 54, 1253-1287 (1989) · Zbl 0701.03030 |
| [25] | Robinson, J., Definability and decision problems in arithmetic, J. Symbolic Logic. (Feferman, S., The Collected Works of J. Robinson (1996), American Mathematical Society: American Mathematical Society Providence, RI), vol. 14, 338-114 (1949), reprint in · Zbl 0034.00801 |
| [26] | Semenov, A., Mat. USSR-Izv., 22, 587-618 (1984), English translation in · Zbl 0541.03005 |
| [27] | Smorynski, C., The incompleteness theorem, (Barwise, J., Handbook of Mathematical Logic, CHD1 Logic, Studies in Logic, vol. 90 (1977)) · Zbl 0453.03018 |
| [28] | Smorynski, C., Logical Number Theory I, ((1991), Springer: Springer Berlin), X + 405 · Zbl 0759.03002 |
| [29] | Tarski, A., (Logique, Sémantique, Métamathématique 1923-1944, vol. 2 (1974), Armand Colin: Armand Colin Paris), 159-269, [Interesting result for us is Section 5, Theorem 1] · JFM 57.1318.03 |
| [30] | Turing, A.; Girard, J.-Y., La machine de Turing, ((1995)), 47-102, Seuil |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
