EDIT: immediately after bountying the question (whoops …) I found, while looking for something else entirely, that Sauro Tulipani gave an explicit algorithm 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. 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.
Best Answer
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 $$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.