Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Axiomatization of Büchi arithmetic

Konstantin Kovalyov

Abstract

In this paper we introduce an axiomatization of Büchi arithmetic, i.e., of the elementary theory of natural numbers in the language with addition and function $V_p(a) = p^k$ such that $p^k | a$ and $p^{k + 1} \nmid a$.

Axiomatization of Büchi arithmetic

Abstract

In this paper we introduce an axiomatization of Büchi arithmetic, i.e., of the elementary theory of natural numbers in the language with addition and function such that and .

Paper Structure

This paper contains 5 sections, 10 theorems, 11 equations.

Table of Contents

  1. Introduction
  2. Notations and conventions
  3. Axiomatization
  4. A model-theoretic proof of completeness
  5. A syntactic proof of completeness

Key Result

Theorem 1

A set $A \subseteq \mathbb{N}^k$ is definable in $(\mathbb{N}, S, +, 0, V_p)$ iff the set of $p$-ary expansions of elements of $A$ is recognizable by a finite automaton.

Theorems & Definitions (18)

  • Theorem 1: Buchi, bruyare
  • Theorem 2: VILLEMAIRE, haase
  • Theorem 3: zapryagaev
  • Proposition 1.1
  • Definition 2.1
  • Theorem 2.1
  • proof
  • Theorem 2.2
  • Lemma 3.1
  • proof
  • ...and 8 more