Efficient elimination of Skolem functions in $\text{LK}^{\text{h}}$

Some model theory of $\operatorname{Th}(\mathbb{N},\cdot)$

'Skolem arithmetic' is the complete theory $T$ of the multiplicative monoid $(\mathbb{N},\cdot)$. We give a full characterization of the $\varnothing$-definable stably embedded sets of $T$, showing in particular that, up to the relation of having the same definable closure, there is only one non-trivial one: the set of squarefree elements. We then prove that $T$ has weak elimination of imaginaries but not elimination of finite imaginaries.

The $Π^1_1 \! \! \downarrow$ Löwenheim-Skolem-Tarski property of Stationary Logic

Fuchino-Maschio-Sakai~\cite{FuchinoEtAl_DRP_LST} proved that the Löwenheim-Skolem-Tarski (LST) property of Stationary Logic is equivalent to the Diagonal Reflection Principle on internally club sets ($\text{DRP}_{\text{IC}}$) introduced in \cite{DRP}. We prove that the restriction of the LST property to (downward) reflection of $Π^1_1$ formulas, which we call the $Π^1_1 \! \! \downarrow$-LST property, is equivalent to the \emph{internal} version of DRP from \cite{Cox_RP_IS}. Combined with results from \cite{Cox_RP_IS}, this shows that the $Π^1_1 \! \! \downarrow$-LST Property for Stationary Lo…

Skolem函数的有限塔界

Finite-tower bounds for Skolem functions

本文给出Skolem函数在有限指数塔下的最终序型上界，通过渐近展开与递归分解结合，证明整体序型为ε₀。

Parametric Presburger Arithmetic: Complexity of Counting and Quantifier Elimination

We consider an expansion of Presburger arithmetic which allows multiplication by $k$ parameters $t_1,\ldots,t_k$. A formula in this language defines a parametric set $S_\mathbf{t} \subseteq \mathbb{Z}^{d}$ as $\mathbf{t}$ varies in $\mathbb{Z}^k$, and we examine the counting function $|S_\mathbf{t}|$ as a function of $\mathbf{t}$. For a single parameter, it is known that $|S_t|$ can be expressed as an eventual quasi-polynomial (there is a period $m$ such that, for sufficiently large $t$, the function is polynomial on each of the residue classes mod $m$). We show that such a nice expression is …