1
$\begingroup$

I've been doing work with axioms, in particular representing common axioms using predicates only, where the predicates work like this: $$*(x,y,z) \ \text{true}\ \Leftrightarrow x * y = z$$

Many common axioms (say, the group axioms) are straightforward to express using predicates. For example, the closure property looks like this:

$$\forall x \forall y \exists z \ *(x,y,z).$$

Associativity is much less obvious. The usual way to express associativity is: $$\forall x \forall y \forall z \ \ x * (y * z) = (x * y) * z$$ but something like $x * (y * z)$ is not simple to express with predicates only; the answer is not to start nesting terms like $*(x, *(y,z), ....)$ since this confuses predicates with functions. I am looking for a first-order logic representation that uses only predicates and not function symbols. (Here for example is a similar question to mine, but all answers involve functions rather than regular boolean predicates.)

Here is what I have so far.

Assign new variables:$$ x * \underbrace{(y * z)}_{=u} = \underbrace{(x * y)}_{=v} * z$$ So we have

$$y * z = u$$ $$x*y = v$$ $$x * u = v * z$$

Let $w = x * u = v * z$.

The facts we have, in predicate notation, are

$$*(y,z,u)$$ $$*(x,y,v)$$ $$*(x,u,w)$$ $$*(v,z,w)$$

Associativity means that if the first three hold for some $w$, the last one must as well. So do we want something like this?

$$\forall x \forall y \forall z \forall u \forall v \exists w \ (*(y,z,u) \wedge *(x,y,v) \wedge *(x,u,w)) \rightarrow *(v,z,w) $$

(I've left out some obvious parentheses.)

There's a number of places where you could take issue with this. We only care about a single "correct" values of $u$ and $v$, so shouldn't they get existentially rather than universally quantified? Universal appears to be correct to me, since any bad values of $u,v$ simply make the antecedent false, which makes the whole claim true.

Is the order of quantification correct? Perhaps $w$ should be ahead of $u$ and $v$: $$\forall x \forall y \forall z \exists w \forall u \forall v \ ...$$ With six quantifiers my intuitions break down quickly.

I've tried numerous theorem prover experiments, changing the quantification, changing the operators, changing everything, and failed to come up with something satisfactory that works as associativity should.

$\endgroup$
0
$\begingroup$

You don't want $\exists w$ in your main formula, but $\forall w$. Otherwise you still have the problem you point out: the conditional can trivially be made true by picking a $w$ for which $*(x,u,w)$ is false.

In other words, you want all of the quantifiers to be universal quantifiers:

$\forall x \forall y \forall z \forall u \forall v \forall w ((*(y,z,u) \land *(x,u,w) \land *(x,y,v)) \rightarrow *(v,z,w))$

Moreover, I would insist on making the $*$ predicate functional in the sense that there is exactly one $z$ for which $*(x,y,z)$:

$\forall x \forall y \exists z \forall w (*(x,y,w) \leftrightarrow w=z)$

$\endgroup$
  • $\begingroup$ @mips Did you see my Answer? $\endgroup$ – Bram28 Nov 11 '18 at 2:41
  • $\begingroup$ Thanks! this is really helpful. Your version with six universal quantifiers was actually the first one I came up with, but I rejected after a few prover tests, where I tried it side-by-side with the usual $x *(y*z) = (x*y)*z$ and it failed to prove the things it should have proved (and possibly proved a few things that it shouldn't have). But adding the requirement you suggest seems to work. This was a subtle point that I failed to notice, I appreciate your help. $\endgroup$ – mips Nov 11 '18 at 4:25
  • $\begingroup$ @mips Ah, great ... I had a suspicion that was the issue :) Glad I could help. Good luck with your project! $\endgroup$ – Bram28 Nov 11 '18 at 4:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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