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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.