Is there a finitely axiomatizable class of structures whose equality-free theory is not finitely axiomatizable?

Question

This was originally an MSE question, but I was told to ask it on MathOverflow. Does there exist a class $C$ of $L$-structures for a finite signature $L$, which is finitely axiomatizable in first-order logic with equality, but whose equality-free theory $Th(C)$ is not finitely axiomatizable?

---

Non-OP edit: To clarify, the question is whether the finite $\mathsf{FOL}$-axiomatizability of $Th_\mathsf{FOL}(C)$ necessarily implies the finite $\mathsf{FOL_{w/o=}}$-axiomatizability of $Th_{\mathsf{FOL_{w/o=}}}(C)$, regardless of whether the $\mathsf{FOL}$-deductive closure of $Th_{\mathsf{FOL_{w/o=}}}(C)$ coincides with $Th_\mathsf{FOL}(C)$ or not. (That is, we don't care whether $Mod(Th_{\mathsf{FOL_{w/o=}}}(C))\not=C.$)

Answer 1

EDIT: As pointed out by Emil Jerabek in the comments, the argument for relational languages fails in the last step. However, the question is already answered by the example with function symbols.

EDIT: If function symbols are allowed, then this can happen. Let $L=\left\{P, f, a\right\}$, where $P$ is a property symbol, $f$ is a unary function symbol and $a$ is a proper name. Let $C$ be the class of models axiomatized by $P(a)$ and $a=f(a)$.

The equality-free theory of $C$ is axiomatized by $T =\left\{P(a), P(f(a)), P(f(f(a))), ...\right\}$.

In fact, if $M$ is a model of $T$, then a model $N$ of $P(a)\wedge(a=f(a))$ can be obtained from $M$ by taking a quotient (identifying all elements corresponding to $a$, $f(a)$, $f(f(a))$, ... in $M$). The canonical mapping from $M$ to $N$ is elementary for equality-free formulas. Since $N$ is in $C$, $M$ satisfies any equality-free sentence in $C$.

However, $T$ is not finitely axiomatizable.

+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

If $L$ is relational (and finite), then finite axiomatizability with equality implies finite axiomatizability without equality.

Since $L$ is finite, let $\phi_1(x,\bar{z})$, ..., $\phi_n(x,\bar{z})$ be all atomic formulas (with the exception of equality formulas) in the variables $x$, $\bar{z}=(z_1,...,z_k)$, in which $k+1$ is the greatest relational arity in $L$.

Consider the formula $I(x,y)$ saying that $x$ and $y$ satisfy the same atomic relations:

$\forall\bar{z}((\phi_1(x,\bar{z})\leftrightarrow\phi_1(y,\bar{z}))\wedge...\wedge(\phi_n(x,\bar{z})\leftrightarrow\phi_n(y,\bar{z})))$.

[edit: In the compact notation sugested in the comments,

$I(x,y)$ is $\forall\bar{z}\bigwedge_{i=1}^{n}(\phi_i(x,\bar{z})\leftrightarrow\phi_i(y,\bar{z}))$.]

Now, let $A$ be an axiom for $Th_{FOL}(C)$. We may assume that $\bar{z}$ does not occur in $A$. Suppose that $\psi$ is an equality-free sentence such that $\psi\in Th_{FOL}(C)$. Therefore,

$A\vdash\psi$.

If $A_I$ is obtained from $A$ by replacing all occurrences of the form $u=v$ by $I(u,v)$, then

$A_I, \forall x,y(x=y\leftrightarrow I(x,y))\vdash\psi$, by a standard result on equivalence.

Since the equality axioms are consequences of $\forall x,y(x=y\leftrightarrow I(x,y))$, we have that

$A_I, \forall x,y(x=y\leftrightarrow I(x,y))\vdash\psi$ in first-order logic without equality also. Hence,

$A_I\vdash\psi$ in first-order logic without equality by the standard conservativity result on definitional extensions.

Since $A$ implies $A_I$, we conclude that $A_I$ is an axiom for $Th_{FOL_{w/o=}}(C)$.