5

Is there a theory $T$ that can be finitely axiomatized in first-order logic with equality, which can also be axiomatized in first-order logic without equality, but not finitely axiomatized in first-order logic without equality?

user107952
  • 20,508
  • I mean to ask, is there a first-order-with-equality theory that can be finitely axiomatized with formulas involving equality, and can be axiomatized but not finitely so with formulas not involving equality? That is really what I am asking. – user107952 Aug 24 '20 at 20:59

1 Answers1

3

No: by the compactness theorem, if $T$ and $T'$ are equivalent theories and $T$ is finite, then a finite subset of $T'$ is equivalent to $T$ and $T'$. (Proof: Let $\varphi$ be the conjunction of the finitely many sentences in $T$. Then $T'\cup \{\lnot\varphi\}$ is inconsistent. By compactness, a finite subset of $T'$ implies $\varphi$ and hence implies all of $T'$.)

So taking $T$ to be a finite theory in first-order logic with equality and $T'$ to be an equivalent theory which does not use $=$, it follows that $T'$ is finitely axiomatizable in first-order logic without equality (by a finite subset of $T'$).

Alex Kruckman
  • 76,357
  • I now see that this answer has essentially the same content as the previously deleted answer by Noah Schweber. In response to hardmath's comment on Noah's answer: For the purposes of comparing theories in first-order logic with and without equality, we can work in first-order logic with equality, and just view a theory without equality as one which happens to not mention the $=$ symbol. Then the argument in my answer (in particular the application of the compactness theorem) occurs in first-order logic with equality, so the infinite "schema of equality" (substitution) isn't relevant. – Alex Kruckman Sep 05 '20 at 12:47
  • In that situation you mean that neither axiomatization uses equality, so effectively equality plays no role in the formulation of the problem. I think there is a more interesting (to me anyway) interpretation, though I grant your interpretation is reasonable (and seems Acceptable to the OP). – hardmath Sep 05 '20 at 16:40
  • @hardmath I don't understand your comment. The finite theory $T$ does use equality. The theory $T'$ does not. From their equivalence (in FO with equality), it follows that a finite subset of $T'$ is also equivalent. – Alex Kruckman Sep 05 '20 at 16:47
  • @hardmath If this is different from the more interesting interpretation you have in mind, could you explain what that interpretation is? – Alex Kruckman Sep 05 '20 at 16:48