Presburger definability and semilinear sets

This file formalizes the classical result that Presburger definable sets are the same as semilinear sets. As an application of this result, we show that the graph of multiplication is not Presburger definable.

Main Results

• presburger.definable_iff_isSemilinearSet: a set is Presburger definable in ℕ if and only if it is semilinear.
• presburger.definable₁_iff_ultimately_periodic: in the 1-dimensional case, a set is Presburger arithmetic definable in ℕ if and only if it is ultimately periodic, i.e. periodic after some number k.
• presburger.mul_not_definable: the graph of multiplication is not Presburger definable in ℕ.

References

• Seymour Ginsburg and Edwin H. Spanier, Bounded ALGOL-Like Languages
• [Seymour Ginsburg and Edwin H. Spanier, Semigroups, Presburger Formulas, and Languages][ ginsburg1966]
• Samuel Eilenberg and M. P. Schützenberger, Rational Sets in Commutative Monoids

theorem IsLinearSet.definable {α : Type u_1} {s : Set (α → ℕ)} {A : Set ℕ} [Finite α] (hs : IsLinearSet s) : A.Definable FirstOrder.Language.presburger s

theorem IsSemilinearSet.definable {α : Type u_1} {s : Set (α → ℕ)} {A : Set ℕ} [Finite α] (hs : IsSemilinearSet s) : A.Definable FirstOrder.Language.presburger s

theorem FirstOrder.Language.presburger.term_realize_eq_add_dotProduct {α : Type u_1} {A : Set ℕ} [Fintype α] (t : (presburger.withConstants ↑A).Term α) : ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v t = k + u ⬝ᵥ v

theorem FirstOrder.Language.presburger.isSemilinearSet_boundedFormula_realize {α : Type u_1} {A : Set ℕ} [Finite α] {n : ℕ} (φ : (presburger.withConstants ↑A).BoundedFormula α n) : IsSemilinearSet {v : α ⊕ Fin n → ℕ | φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)}

theorem FirstOrder.Language.presburger.isSemilinearSet_formula_realize_semilinear {α : Type u_1} {A : Set ℕ} [Finite α] (φ : (presburger.withConstants ↑A).Formula α) : IsSemilinearSet (setOf φ.Realize)

theorem FirstOrder.Language.presburger.definable_iff_isSemilinearSet {α : Type u_1} {A : Set ℕ} [Finite α] {s : Set (α → ℕ)} : A.Definable presburger s ↔ IsSemilinearSet s

A set is Presburger definable in ℕ if and only if it is semilinear.

theorem FirstOrder.Language.presburger.definable₁_iff_ultimately_periodic {A s : Set ℕ} : A.Definable₁ presburger s ↔ ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s

In the 1-dimensional case, a set is Presburger arithmetic definable in ℕ if and only if it is ultimately periodic, i.e. periodic after some number k.

theorem FirstOrder.Language.presburger.mul_not_definable {A : Set ℕ} : ¬A.Definable presburger {v : Fin 3 → ℕ | v 0 = v 1 * v 2}

The graph of multiplication is not Presburger definable in ℕ.