I have some formula in predicate logic that contain predicate symbols and function symbols and I should define their meaning and the domain of discourse.
- $Q(x,y)$ is predicate symbol of arity 2
- $n$ is function symbol of arity 0 (a constant)
- $*$ is function symbol of arity 2
- other...
From other forumula it kinda looks like
- the domain of discourse could be all positive (w/o zero) rational (or even real) numbers
- $n$ could be one
- $*$ could be multiplication
Now I've hit this formula, which looks almost like the definition of divisibility on integers.
$\varphi\equiv\forall x \forall y (Q(x,y)\Leftrightarrow (y=n \lor \exists z (Q(x,z) \land y=x*z)))$
The problem is it is NOT a divisibility!
Let's say $y$ divides $x$, $x=6$ and $y=3$. Then for $z=2$ it holds $Q(6,2)$ as 2 divides 6, but $3=6*2$ does not hold!
Let's say $x$ divides $y$, $x=3$ and $y=6$. Then from $6=3*z$ we conclude $z=2$, but $Q(6,2)$ does not hold, as 6 does not divide 2!
So my question is, do you think there is an error in $\varphi$ and $y=x*z$ should correctly be $x=y*z$? If it is not an error, what exactly could this formula represent? Do I have to change my domain of discourse, function/predicate symbols?