A non-sequential arithmetical theory with pairing

Abstract

Albert Visser has shown that Robinson's $\mathsf{Q}$ and Gregorczyk's $\mathsf{TC}$ are not sequential by showing that these theories are not even poly-pair theories, which, in a strong sense, means these theories lack pairing. In this paper, we use Ehrenfeucht-Fraïssé games to show that the theory $\mathsf{Q}+\Theta$ we obtain by extending Robinson's $\mathsf{Q}$ with an axiom $\Theta$ which says that the map $\pi (x,y)=(x+y{)}^2+x$ is a pairing function is not sequential; in fact, we show that this theory is not even a Vaught theory. As a corollary, we get that the tree theory $\mathsf{T}$ of [Kristiansen & Murwanashyaka, 2020] is also not a Vaught theory.