Title: Theory / Unimportant / Math / Logic / Model theory / Natural arithmetic / The definable criterion for definability in Presburger arithmetic and its applications
Tags: hasSeenConjDef fromAlgorithm hasNotNewEffectReturnsMeaning

Name: A period of \(A\) in \(W\)
Definition: Some \(v\in\mathbb Z^n\) such that, \(x,x+v\in W\) implies \(x\in A\iff x+v\in A\)
Page: 2
Variables: \(A,W\subseteq\mathbb Z^n\)
Kind: 1

Name: Presburger arithmetic
Definition: elementary theory of integers with addition and order.
Page: 2
Kind: 1

Definition: [$]\sum_i\abs{x_i}[/$]
Page: 2
Variables: \(\vec x\in\mathbb Z^n\)
Context: Presburger Arithmetic, Muchnic
Notation: [$]\abs{\vec x}[/$]
Kind: 1

Name: The \((i,l)\)-section of \(A\)
Definition: the set of \(\langle x_1,\dots,x_{i-1},x_{i+1},\dots, x_n\rangle\in\mathbb Z^{n-1}\) such that \(\langle x_1,\dots,x_{i-1},l,x_{i+1},\dots, x_n\rangle\in A\)
Page: 2
Variables: \(A\subseteq\mathbb Z^n\)
\(1\le i\le n\),
\(l\in\mathbb Z\)
Notation: \(A_{i,l}\)
Kind: 1

Name: A section of \(A\)
Definition: Some \(A_{i,l}\)
Page: 2
Variables: \(A\subseteq\mathbb Z^n\)
Kind: 1

Name: A set of possible period of \(A\)
Definition: for every \(k>0\),
Page: 2
Variables: \(A\subseteq\mathbb Z^n\)
\(V\subseteq \)
Index: 1
Kind: def
Definition2: there exists \(l(k)\)
Conjdef: A set \(V\subseteq\mathbb Z^n\) such that
Definition3: such that for every \(\vec x\in\mathbb Z^n\) with [$]\abs{x}>l[/$]
Definition4: there exists \(\vec v(k,\vec x)\in V\)
Definition5: such that \(A\) is \(\vec v(k,\vec x)\)-periodic in the \(k\)-neighborhood of \(\vec x\)
Hide remaining def: yes

Smaller0: \(A\) is Presburger definable
Greater0: \(A\) is \(V\)-periodic, where \(V\) is the set of vectors of length at most \(k\) for some \(k\)
Page: 2,4
Section: 2
Variables: \(A\subseteq\mathbb Z^n\)
Index: 1,4
Kind: theo
Smaller to greater: iff
Prefix Greater: (
Greater1: \(A\) admits a finite set of possible periods
Connect Greater0: or
Greater2: each section of \(A\) is Presburger-definable
Connect Greater1: )and

Name: The boundary of \(A\) in the direction \(v\)
Definition: The set of \(\vec x\in A\) such that \(\vec x+\vec v\not\in A\)
Page: 2
Variables: \(A\subseteq\mathbb Z^n\)
\(\vec v\in\mathbb Z^n\)
Notation: \(\mathrm{Bd}(A,v)\)
Kind: 1

Smaller0: all sections of \(A\) are Presburger-definable
Greater0: all sections of \(\mathrm{Bd}(A,v)\) are Presburger-definable
Page: 4
Section: 1
Variables: \(v\in\mathbb Z^n\)
\(A\subseteq\mathbb Z^n\)
Index: 0
Kind: Lem

Smaller0: \(A\) is \(V\)-periodic
Greater0: \(V\setminus\{v,-v\}\)-periodic
Page: 4
Section: 1
Variables: \(v\in V\subseteq\mathbb Z^n\)
\(A\subseteq\mathbb Z^n\)
Kind: Lem
Prefix Greater: \(\mathrm{Bd}(A,v)\) is
Construction: each ball is either \(v\) periodic,, in which case \(\mathrm{Bd}(A,v)\) is empty. Otherwise, it is \(v'\) periodic for \(v'\in V\setminus\{v,-v\}\)

Question: \(A\) can be defined using all of
Answer: Presburger arithmetic
Page: 4
Section: 1
Variables: \(v\in V\subseteq\mathbb Z^n\setminus\{0\}\)
\(A\subseteq\mathbb Z^n\)
Answer2: \(\mathrm{Bd}(A,v)\) and \(\mathrm{Bd}(A,-v)\)
Index: 2
Kind: Lem
Answer3: a finite number of sections of \(A\)
Name: Muchnik construction
Construction: Take \(x\in\mathbb Z^n\). Let \(u_i=x+iv\).
To decide whether \(x\in A\),
consider whether it satisfies one of the following case:
-whether there is some \(i<0\) such that \(u_i\in\mathrm{Bd}(A,-v)\), or whether for each \(i<0\), \(u_i\in A\).
Same question for \(i>0\) and \(\mathrm{Bd}(A,v)\).
Each of those four cases are definable
If there is some \(i\) as above in the boundary as above, then boundary is enough to state that \(x\in A\).
Otherwise, \(u_i\) intersects a section (for example, one with a vector in \([0,v_i]\).

Definition: \(\phi_{n-1}(A_{i,l})\) for each \(i,l\)
Page: 4
Section: 1
Variables: \(A\) a \(n\)-ary symbol
Notation: \(\phi_n(A)\)
Index: 2
Kind: Theo
Definition2: there exists \(n>0\) such that \(A\) is \(V\)-periodic, with \(V\) the set of vectors of modulus at most \(n\)
Conjdef: The conjonction of
Intuition: Formula stating that \(A\) is Presburger-definable

Page: 4
Implementation: encode \(\phi_n(A)\), using classical automata convention, and using \(\mathcal A\) to encode \(A\)
Section: 1
Effect: whether \(\mathcal A\) accepts a Presburger-definable set
Variables: \(\mathcal A\) an automaton reading number in base \(b\) with \(n\)-dimensions
Index: 3
Kind: Theo