# Is the following theory consistent?

Suppose, we have a first-order logic theory over a signature {=, $\times$} (where $\times$ is a binary function symbol, and = is the equality symbol), that contains following axioms: $$\forall x \forall y ( x \times (y \times y) = (x \times y) \times y)$$ $$\exists o \forall x (x \times o = o)$$ $$\exists e \forall x (x \times e = x)$$ $$\forall x \forall y \exists z (x \times z = y)$$ $$\exists x \exists y (\neg(x = y))$$ Is this theory consistent?

It is quite easy to prove that if it is, then every its model has to be infinite. Also, it is quite obvious that the following statements are logically implied by this theory: $$\neg \forall x \forall y ((y \times y) \times x = y \times(y \times x))$$ $$\neg \exists a \forall x (a \times x = a)$$ $$\neg \forall x \forall y \exists z (z \times x = y)$$ $$\neg \forall x \forall y (x \times y = y \times x)$$

However, I do not know how to proceed further…

Any help will be appreciated.

• Your last two rules are built into the semantics of first-order logic: "$=$" is a logical symbol, which always corresponds to actual equality. (Very old textbooks sometimes don't assume this, but modern sources do.) Commented Nov 4, 2017 at 17:24
• How about the standard interpretation? If that is a model, then the theory is consistent. Commented Nov 4, 2017 at 17:30
• @Bram28, Thank You, but those interpretations do not seem to be models, as 0 in them violates the fourth axiom (one can not divide by it). Commented Nov 4, 2017 at 17:40
• I think you left out an axiom asserting the existence of at least two elements - otherwise, the one-element structure satisfies those axioms. Commented Nov 4, 2017 at 17:44
• @Bram28 In fact, note that "$\times$" can't be commutative (once we rule out the one-element structure via an additional axiom): if it were, taking $x=o$ and $y\not=o$ (where $o$ is some element satisfying rule $2$) would violate rule $4$. Commented Nov 4, 2017 at 17:45

Your theory is consistent. Here is a model. I will write $*$ instead of $\times$ because it's easier to type.

The universe is the set $\{0,1,2,3,\dots\}$ of all nonnegative integers; $x*1=x$ for all $x;$ for $y\ne1$ we define $$x*y=\begin{cases} \ \ \ y\ \ \ \ \ \text{ if }\ x=y,\\ \lfloor y/2\rfloor\ \text{ if }\ x\ne y. \end{cases}$$

Clearly $x*1=x$ and $x*0=0$ for all $x.$

Given $x$ and $y,$ we can find $z$ such that $x*z=y;$ namely, if $y=0$ take $z=0;$ if $y\ne0$ choose $z\in\{2y,2y+1\}$ so that $z\ne x.$

To verify $x*(y*y)=(x*y)*y$ we consider three cases:

If $y=1$ then $x*(y*y)=x*(1*1)=x*1=x$ and $(x*y)*y=(x*1)*1=x*1=x.$

If $x=y$ then $x*(y*y)=y*(y*y)=y*y=y$ and $(x*y)*y=(y*y)*y=y*y=y.$

If $y\ne1$ and $x\ne y$ then $x*(y*y)=x*y=\lfloor y/2\rfloor$ and $(x*y)*y=\lfloor y/2\rfloor*y=\lfloor y/2\rfloor.$