# Persistent finite axiomatizability, relational edition

Say that a finitely axiomatizable first-order theory $$T$$ (in a finite language $$\Sigma$$) is persistently finitely axiomatizable iff the set $$T_{\mathsf{w/o=}}$$ of equality-free $$T$$-theorems is finitely axiomatizable in first-order logic without equality.

Building on this earlier question, I would like to ask:

Is there a finitely axiomatizable relational theory which is not persistently finitely axiomatizable?

Here are the only two relevant facts I currently know:

• One natural attempt for proving a negative answer is the following. Let $$I(x,y)\equiv\bigwedge_{R\in \Sigma} \forall \overline{u},\overline{v}(R(\overline{u},x,\overline{v})\leftrightarrow R(\overline{u},y,\overline{v})).$$ Then we might expect to have $$\vdash A\leftrightarrow A_I$$ for all first-order sentences $$A$$, where $$A_I$$ is gotten from $$A$$ by replacing "$$s=t$$" with "$$I(s,t)$$" throughout. However, this breaks down: consider e.g. $$A\equiv \exists x,y(x=y\wedge \neg I(x,y))$$. (This counterexample was pointed out by Emil Jerabek.)

• If we allow function symbols we get a positive answer; this was observed by Rodrigo Freire, answering the above-linked original question.

1. The set $$T_{w/o=}$$ is axiomatized by $$A_I$$ in some cases. For example, if $$A$$ is preserved under quotient by the congruence defined by $$I(x,y)$$. For, from the argument in the answer of the original question, it is enough to prove that $$\vdash A\rightarrow A_I$$ under our assumption. Let $$M\models A$$. Then $$M/I\models A$$. However, $$M/I\models \forall x,y(x=y\leftrightarrow I(x,y))$$, hence $$M/I\models A_I$$. Since quotient maps are elementary for equality-free formulas, $$M\models A_I$$. If equality occurs only positively in $$A$$, then we are in this case, for example.
2. However, $$T_{w/o=}$$ is not axiomatized by $$A_I$$ in general and replacing $$I(x,y)$$ by another (equality-free) definable congruence $$J(x,y)$$ will not work. In fact, since $$I$$ and $$J$$ are both congruences, $$\vdash J(x,y)\wedge J(x,x)\rightarrow(I(x,x)\leftrightarrow I(y,x))$$, hence $$\vdash J(x,y)\rightarrow I(x,y)$$, and conversely.
3. The existential second-order formula $$\exists R; (C(R)\wedge A_R)$$, axiomatizes $$T_{w/o=}$$, where $$R$$ is a relation symbol, $$C(R)$$ is the conjunction of the equality axioms for $$R$$ and $$A_R$$ is obtained from $$A$$ by replacing $$=$$ by $$R$$. This follows from the fact that if $$\phi$$ is equality-free and $$\vdash A\rightarrow \phi$$ in $$FOL$$, then $$\vdash (C(R)\wedge A_R)\rightarrow\phi$$ in $$FOL$$ without equality, and $$\vdash\exists R;(C(R)\wedge A_R)\rightarrow\phi$$ in existential second-order logic. This works for general finite signatures, and we know that $$T$$ may not be persistently finitely axiomatizable in the presence of function symbols.
4. The following example shows that nonuniform replacements of $$x=y$$ in $$A$$ work in some cases where no uniform replacement seems to work. Let $$P$$ be a relation symbol and $$T$$ be axiomatized by the following sentence $$A$$: $$\exists x,y;(x\neq y)\wedge \forall x,y(x\neq y\rightarrow Pxy)$$. The simplest finite axiomatization of $$T_{w/o=}$$ that I could think is the following $$A^*$$: $$\exists x,y;(Pxy)\wedge\forall x,y(\neg I(x,y)\rightarrow Pxy)$$. It is easy to see that these axioms are in $$T_{w/o=}$$. Conversely, let $$M$$ be a model of $$A^*$$. If $$M\models\exists x,y;\neg I(x,y)$$, then $$M/I\models A$$, for $$I(x,y)$$ is equivalent to $$x=y$$ in $$M/I$$ and the equality-free $$A^*$$ is preserved under quotients. Therefore, $$M/I\models T_{w/o=}$$, and so $$M\models T_{w/o=}$$ On the other hand, if $$M\models\forall x,y(I(x,y))$$, then, from $$M\models A^*$$, it follows that $$M\models\forall x,y (Pxy)$$. In this case, $$M/I$$ contains only one element which satisfies the formula $$Pxx$$. The model $$M/I$$ is also the quotient of a two-element model $$N$$ in which $$P$$ is interpreted as the total relation $$N\times N$$. We have that $$N\models A$$, hence both $$N$$ and $$M$$ satisfy $$T_{w/o=}$$. Note that $$A_I$$ will not do the job in this example, for $$A_I$$ is not in $$T_{w/o=}$$ (the problem is the negative occurrence of $$x=y$$ in the first conjunct of $$A$$).
5. The natural strategy of eliminating equality in $$A$$ runs into some difficulty, because we don't know what to do with the negative occurrences of the equality (the positive occurrences may be replaced by $$I$$). The only alternative strategy that I can think of is one based on Fraïsséan methods, which can be adapted to logic without equality. The idea is that for some quantifier rank $$q$$ (supposed to be the quantifier rank of $$A_I$$) the conjunction of the (finitely many up to equivalence) sentences $$\psi\in T_{w/o=}$$ of quantifier rank $$q$$ is an axiom for $$T_{w/o=}$$.