Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Definable sets in Skolem arithmetic

Łukasz Kamiński

Abstract

In this note, we present a characterization of sets definable in Skolem arithmetic, i.e., the first-order theory of natural numbers with multiplication. This characterization allows us to prove the decidability of the theory. The idea is similar to that of Mostowski; however, our characterization is new, and the proof relies on different combinatorial tools. The main goal of this note is to provide a simpler decidability proof than those previously known.

Definable sets in Skolem arithmetic

Abstract

In this note, we present a characterization of sets definable in Skolem arithmetic, i.e., the first-order theory of natural numbers with multiplication. This characterization allows us to prove the decidability of the theory. The idea is similar to that of Mostowski; however, our characterization is new, and the proof relies on different combinatorial tools. The main goal of this note is to provide a simpler decidability proof than those previously known.

Paper Structure

This paper contains 7 sections, 3 theorems, 3 equations.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Definable sets
  4. Closure properties
  5. Conclusion

Key Result

Lemma 1

Let $G = (L \cup R, E)$ be a bipartite graph. If there is a matching of $L' \subseteq L$ and a matching of $R' \subseteq R$ then there is a matching of $L' \cup R'$.

Theorems & Definitions (4)

  • Lemma 1: HLT17
  • Theorem 2
  • Theorem 4
  • proof