Axiomatizing rectangular grids with no extra non-unary relations

Abstract

We construct a formula $\varphi$ which axiomatizes non-narrow rectangular grids without using any binary relations other than the grid neighborship relations. As a corollary, we prove that a set $A\subseteq \mathbb{N}$ is a spectrum of a formula which has only planar models if numbers $n\in A$ can be recognized by a non-deterministic Turing machine (or a one-dimensional cellular automaton) in time $t(n)$ and space $s(n)$, where $t(n)s(n)\le n$ and $t(n),s(n)=\Omega (\log (n))$.

9 pages, 1 figure