Decidability of Definability Issues in the Theory of Real Addition

• Autorzy: Bès Alexis , Choffrut Christian

Identyfikatory

DOI

10.3233/FI-222140

• Języki publikacji: EN

Abstrakty

EN

Given a subset of X ⊆ ℝn we can associate with every point x ∈ ℝn a vector space V of maximal dimension with the property that for some ball centered at x, the subset X coincides inside the ball with a union of lines parallel to V. A point is singular if V has dimension 0. In an earlier paper we proved that a 〈ℝ, +, <, ℤ〉-definable relation X is 〈ℝ, +, <, 1〉-definable if and only if the number of singular points is finite and every rational section of X is 〈R, +, <, 1〉-definable, where a rational section is a set obtained from X by fixing some component to a rational value. Here we show that we can dispense with the hypothesis of X being 〈ℝ, +, <, ℤ〉-definable by requiring that the components of the singular points be rational numbers. This provides a topological characterization of first-order definability in the structure 〈ℝ, +, <, 1〉. It also allows us to deliver a self-definable criterion (in Muchnik's terminology) of 〈ℝ, +, <, 1〉- and 〈ℝ, +, <,ℤ〉-definability for a wide class of relations, which turns into an effective criterion provided that the corresponding theory is decidable. In particular these results apply to the class of so-called k–recognizable relations which are defined by finite Muller automata via the representation of the reals in a integer basis k, and allow us to prove that it is decidable whether a k–recognizable relation (of any arity) is l–recognizable for every base l ≥ 2.

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2022
• Tom: Vol. 188 nr 1
• Strony: 15--39
• Opis fizyczny: Bibliogr. 24 poz.

Twórcy

autor

Bès Alexis

• Univ. Paris Est Creteil, LACL, F-94010 Creteil, France

autor

Choffrut Christian

• IRIF (UMR 8243), CNRS and Universit´e Paris 7 Denis Diderot, France

Bibliografia

• [1] Bès A. Expansions of MSO by cardinality relations. Logical Methods in Computer Science, 2013. 9(4). doi:10.2168/LMCS-9(4:18)2013.
• [2] Bès A, and Choffrut C. Theories of real addition with and without a predicate for integers. Logical Methods in Computer Science, 2021. 17(2):18. doi:10.23638/LMCS-17(2:18)2021.
• [3] Bieri H, and Nef W. Elementary set operations with d-dimensional polyhedra. Workshop on Computational Geometry, Springer, 1988 pp. 97-112. doi:10.1007/3-540-50335-8 28.
• [4] Boigelot B, and Brusten J. A generalization of Cobham’s theorem to automata over real numbers. Theor. Comput. Sci., 2009. 410(18):1694-1703. doi:10.1016/j.tcs.2008.12.051.
• [5] Boigelot B, and Brusten J, and Bruyère V. On the Sets of Real Numbers Recognized by Finite Automata in Multiple Bases. Logical Methods in Computer Science, 2010. 6(1):1-17. doi:10.2168/LMCS-6(1:6)2010.
• [6] Boigelot B, and Brusten J, and Leroux J. A Generalization of Semenov’s Theorem to Automata over Real Numbers. Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings, 2009 pp. 469-484. doi:10.1007/978-3-642-02959-2 34.
• [7] Boigelot B, and Brusten J, and Degbomont JF. Automata-Based Symbolic Representations of Polyhedra. Proc. LATA 2012, LNCS vol. 7183, 2012 pp. 3-20. doi:10.1007/978-3-642-28332-1 2.
• [8] Bruyère V, and Hansel G, and Michaux C, and Villemaire R. Logic and p-recognizable sets of integers. Bull. Belg. Math. Soc. Simon Stevin 1994. 1(2):191-238. doi:10.36045/bbms/1103408547.
• [9] Boigelot B, and Rassart S, and Wolper P. On the Expressiveness of Real and Integer Arithmetic Automata (Extended Abstract). Automata, Languages and Programming, 25th International Colloquium, ICALP’98, Aalborg, Denmark, July 13-17, 1998, Proceedings, 1998 pp. 152-163.
• [10] Bouchy F, and Finkel A, and Leroux J. Decomposition of decidable first-order logics over integers and reals 15th International Symposium on Temporal Representation and Reasoning. IEEE, 2008. doi:10.1109/TIME.2008.22.
• [11] Dolich A, and Goodrick J. Strong theories of ordered Abelian groups. Fundamenta Mathematicae 236, 2017 pp. 269-296.
• [12] Dolich A, and Miller C, and Steinhorn C. Structures having o-minimal open core. Transactions of the American Mathematical Society, 2020. 362(3):1371-1411. URL https://www.jstor.org/stable/40590872.
• [13] Feferman S, and Vaught RL. The first order properties of products of algebraic systems Fundam. Math. vol.47, 1959 pp. 57-103. ISSN: 0016-2736.
• [14] Ferrante J, and Rackoff C. A decision procedure for the first order theory of real addition with order. SIAM J. on Computing, 1975. 4(1):69-76. doi:10.1137/0204006.
• [15] Ginsburg S, and Spanier E. Semigroups, Presburger formulas, and languages. Pacific journal of Mathematics, 1966. 16(2):285296.
• [16] Hieronymi P. When is scalar multiplication decidable? Annals of Pure and Applied Logic, 2019. 170(10):1162-1175. doi:10.1016/j.apal.2019.05.001.
• [17] Milchior A. Büchi Automata Recognizing Sets of Reals Definable in First-Order Logic with Addition and Order Proceedings of TAMC 2017 pp. 440-454. doi:10.48550/arXiv.1610.06027.
• [18] Muchnik AA. The definable criterion for definability in Presburger arithmetic and its applications. Theor. Comput. Sci., 2003. 290(3):1433-1444. doi:10.1016/S0304-3975(02)00047-6.
• [19] Point F, and Wagner FO. Essentially periodic ordered groups. Annals of Pure and Applied Logic, 2000. 105(1-3):261-291. doi:10.1016/S0168-0072(99)00053-6.
• [20] Presburger M. Uber die Vollstandigkeit eines gewissen Systems der Arithmetic ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. Compte-Rendus du 1er Congrès des Mathèmaticiens des pays slaves, Warsaw, 1929.
• [21] Semenov AL. Presburgerness of predicates regular in two number systems (in Russian). Sibirsk. Mat. Zh., 18, (1977) 403-418, English translation, Siberian Math. J., 1977. 18:289-299.
• [22] Semenov AL, Soprunov S, and Uspensky VA. The Lattice of Definability. Origins, Recent Developments, and Further Directions. Computer Science - Theory and Applications - 9th International Computer Science Symposium in Russia, CSR 2014, Moscow, Russia, June 7-11, 2014 pp. 23-38. doi:10.1007/978-3-319-06686-8 3.
• [23] Walsberg E. Generalizing a theorem of Bès and Choffrut. arXiv preprint, 2020, URL https://arxiv.org/abs/2002.10508.
• [24] Weispfenning V. Mixed Real-Integer Linear Quantifier Elimination. Proceedings of the 1999 International Symposium on Symbolic and Algebraic Computation, ISSAC ’99, 1999 pp. 129-136. doi:10.1145/309831.309888.