Persistent finite axiomatizability, relational edition

Question

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.

Answer 1

Let me collect some partial results and some speculation that may be useful here.

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=}$.