EDIT: immediately **after** bountying the question *(whoops ...)* I found, while looking for something else entirely, that Sauro Tulipani [gave an explicit algorithm](https://www.jstor.org/stable/2273991?refreqid=excelsior%3Abff6195c8445cbcfc1c488c4c2530272&seq=1#metadata_info_tab_contents) for producing a Horn sentence $\varphi\_p$ saying "There are not exactly $p$ objects" and $length(\varphi\_p)=O(p^5\log p).$ So my question should be rephrased as:



> 
> Is Tulipani's solution optimal?
> 
> 
> 


(From Tulipani's article I also learned that the construction mentioned below was originally due to Appel, and was rediscovered later by Blass independently.)




---


This question is motivated by Blass' paper [There are not exactly five objects](https://www.jstor.org/stable/2274177?seq=1#metadata_info_tab_contents). Briefly, Wilkie observed that a general semantic result implies that "There are not exactly $p$ objects" must be expressible by a Horn sentence$^\*$ in the equality-only language for each prime $p$, but actually finding such sentences is nontrivial. Blass' example is a bit long (with length exceeding $10^{10^{22}}$ in the case $p=5$); he goes on to say that a somewhat shorter example exists for $p=5$ (due to Morley) but that it doesn't obviously generalize to arbitrary primes.


I'm curious what the optimal length is, as a function of the index of the prime involved:



> 
> For $i\in\mathbb{N}$ let $H(i)$ be the length of the shortest Horn sentence equivalent to "There are not exactly $p\_i$ objects," where $p\_i$ is the $i$th prime. What can we say about the growth rate of $H$?
> 
> 
> 


In particular, it is consistent with my current understanding that Blass' construction is *asymptotically* optimal. I suspect that's not the case, but I don't have any actual evidence for that.


*(The tag "universal-algebra" is a bit tentative; my understanding is that, although not strictly equational, Horn logic is still of interest to UA, but I could easily be overestimating its relevance.)*




---


$^\*$That is: "a first-order sentence in prenex normal form whose matrix is a conjunction of conditionals in each of which the consequent is atomic or "false" and the antecedent is a conjunction of atomic formulas." The obvious first-order formulation $$\forall x\_1,...,x\_p[(\bigwedge\_{1\le i<j\le p}x\_i\not=x\_j)\rightarrow\exists y(\bigwedge\_{1\le i\le p}y\not=x\_i)]$$ is **not** a Horn sentence, so the problem is nontrivial.



How hard is it to say "not exactly $p$" with a Horn sentence?
I will show how to improve Tulipani’s construction from $O(p^5)$ symbols to $O(p^3)$ symbols, or $O(p^3\log p)$ bits.


Recall that Tulipani’s sentence is
$$H\_p=\forall\vec x\,\exists\vec s\,\exists\vec u\,\exists y\:\Bigl(G\_p(\vec x,\vec s,\vec u)\land\let\ET\bigwedge\ET\_i(y=x\_i\land u\_p=x\_0\to x\_1=x\_0)\Bigr),$$
where $G\_p(\vec x,\vec s,\vec u)$ is a Horn formula in variables $\{x\_i:0\le i<p\}$, $\{s\_{ij}:0\le i\le j<p\}$, $\{u\_i:2\le i\le p\}$, defined as the conjunction of
$$\begin{gather}
\tag1\label{assoc}\ET\_{i,j,k,h,r}(x\_h=s'\_{ij}\land x\_r=s'\_{jk}\to s'\_{hk}=s'\_{ir}),\\
\tag2\label{canc}\ET\_{i,j,k}(s'\_{ij}=s'\_{ik}\to x\_j=x\_k),\\
\tag3\label{zero}\ET\_is\_{0i}=x\_i,\\
\tag4\label{cyc}u\_2=s\_{11}\land\ET\_{2\le j<p}\ET\_i(u\_j=x\_i\to u\_{j+1}=s'\_{1i}),
\end{gather}$$
where $s'\_{ij}:=s\_{\min\{i,j\},\max\{i,j\}}$. The meaning of $G\_p$ is that given elements $\vec a,\vec b,\vec c$ of a model such that each $b\_{ij}$ belongs to the set $A=\{a\_i:i<p\}$, $G\_p(\vec a,\vec b,\vec c)$ is true iff the recipe
$$\tag+\label{add}a\_i+a\_j=a\_j+a\_i=b\_{ij},\qquad i\le j<p,$$
gives a well-defined operation $+$ on $A$ such that


* $(A,+)$ is an abelian group with zero element $a\_0$,
* $c\_j=ja\_1$ for each $j$.


The bottleneck here is the formula $\eqref{assoc}$ with $p^5$ conjuncts, which ensures (in view of $\eqref{zero}$) that $+$ is well defined, and associative.


First, I claim that one can replace $\eqref{assoc}$ with the two formulas
$$\begin{gather}
\tag{$1'$}\label{def}\ET\_{i,j,k}(x\_i=x\_j\to s'\_{ik}=s'\_{jk}),\\
\tag{$1''$}\label{nucl}\ET\_{i,j,h,r}(x\_h=s'\_{ij}\land x\_r=s'\_{j1}\to s'\_{h1}=s'\_{ir})
\end{gather}$$
with $O(p^4)$ symbols. Let $G'\_p$ denote $\eqref{def}\land\eqref{nucl}\land\eqref{canc}\land\eqref{zero}\land\eqref{cyc}$, and let $H'\_p$ be $H\_p$ with $G\_p$ replaced with $G'\_p$. It is easy to see that if $A=\{a\_i:i<p\}$ and $\vec b\in A$, then $G'\_p(\vec a,\vec b,\vec c)$ holds iff $\eqref{add}$ gives a well-defined operation on $A$ such that


* $(A,+)$ is a commutative loop with zero element $a\_0$,
* $a\_1$ belongs to the [nucleus](https://groupprops.subwiki.org/wiki/Nucleus)
$$N=\{z\in A:\forall x,y\in A\:(x+y)+z=x+(y+z)\},$$
* $c\_j=ja\_1$ for each $j$ (meaning a sum of $j$ copies of $a\_1$, whose bracketing does not matter because of the previous point).


Since $G\_p$ implies $G'\_p$, $H'\_p$ still holds in models of size $\ne p$.


The nucleus $N$ is associative, and it is a subgroup of $A$. If $\sim$ denotes the equivalence relation
$$a\sim b\iff N+a=N+b,$$
then the equivalence class of $a$ is $N+a$: on the one hand, if $a\sim b$, then $b\in N+b=N+a$ as $0\in N$. On the other hand, if $b=n+a$ with $n\in N$, then
$$N+b=N+(n+a)=(N+n)+a=N+a$$
using the definition of $N$ and the fact that it is a subgroup. Thus,
$$\{N+a:a\in A\}$$
is a partition of $A$ into sets of size $|N+a|=|N|$. As a consequence, $|N|$ divides $|A|$, and more generally, if $H$ is a subgroup of $N$, then $|H|$ divides $|A|$.


In particular, if $G'\_p(\vec a,\vec b,\vec c)$ where the $a\_i$ are pairwise distinct, then the order of the cyclic subgroup of $A$ generated by $a\_1$ divides $p=|A|$. This implies that $H'\_p$ fails in a model of size $p$ if we take for $\vec x$ a bijective enumeration of its elements, using the same argument as Tulipani.


This gives a sentence $H'\_p$ with $O(p^4)$ symbols. In order to further reduce it to $O(p^3)$, note that $\eqref{nucl}$ can be replaced with
$$\ET\_{i,j}\exists z\ET\_h\bigl((x\_h=s'\_{ij}\to s'\_{h1}=z)\land(x\_h=s'\_{j1}\to s'\_{ih}=z)\bigr).$$
If we want to keep $H'\_p$ in prenex normal form, we can introduce new variables $\{z\_{ij}:i,j<p\}$, expand the quantifier prefix of $H'\_p$ to $\forall\vec x\,\exists\vec s\,\exists\vec u\,\exists y\,\exists\vec z$, and replace $\eqref{nucl}$ with
$$\ET\_{i,j,h}\bigl((x\_h=s'\_{ij}\to s'\_{h1}=z\_{ij})\land(x\_h=s'\_{j1}\to s'\_{ih}=z\_{ij})\bigr).$$
This gives a sentence with $O(p^3)$ symbols, still using $O(p^2)$ variables.


A few more optimizations, which however do not change the $O(p^3)$ asymptotic:


* We can drop $\eqref{def}$. On the one hand, this only makes the sentence weaker, hence it continues to hold in models of size $\ne p$. On the other hand, the failure for models of size $p$ is achieved when the $x\_i$ are pairwise distinct, in which case $\eqref{def}$ holds automatically.
* We can drop $\eqref{zero}$ and the $s\_{0i}$ variables, putting $s'\_{0i}:=x\_i$ instead.
* We only use the $u\_j$ variables to compute $u\_p=px\_1$. If we count to $p$ using doubling rather than adding $1$ at each step, we only need the $O(\log p)$ variables $u\_j$ for $j=\lfloor p2^{-k}\rfloor$, $k\le\log\_2p-2$, and we can reduce the size of $\eqref{cyc}$ to $O(p\log p)$ symbols.


It’s hard to guess what the optimal size should be; the only lower bound I can think of is that using a straightforward pebble game argument, any sentence (Horn or otherwise) that distinguishes a set with $p$ elements from a set with $p+1$ elements needs to use more than $p$ distinct variables (and a fortiori needs quantifier rank more than $p$). This bound is tight for not-necessarily-Horn sentences, as exhibited in the question.


