Writing predicates - is the quantifier necessary?

Question

I'm taking a course in mathematical logic, it has recently covered quantifiers and now I find myself somewhat confused whether or not the existential quantifier is necessary - consider this example:

Disclaimer: Assume that our universe is the set of natural numbers

$x$ is an even number

Now, I can't really tell the difference between these two notations:
$$(\exists m)(x=2m)$$ And this: $$x=2m$$ Are they basically the same? If so, does it mean that we can always omit the existential quantifier?
Now, let's consider another example:

$x$ is prime

The same problem - I have two notations and can't choose which of them is the right one.
$$(\forall a)(a |x \Rightarrow ((a=1 \lor a=x) \land x\ne1)) $$ And $$a|x \Rightarrow ((a =1 \lor a=x) \land x\ne 1) \\ [1]$$ And finally, the last predicate:

$x$ is composite

Is it enough to write $$ \neg [1]$$ or it is necessary to write $$(\exists a)(\neg [1])$$ Do these predicates actually mean the same thing?

Answer 1

No, we cannot omit the existential quantifier.

How we read the formula:

$x=2m$ ?

As: "every $x$ is even" ? Or as: "some $x$ is even" ? Or as: "every $x$ is the double of every $m$" ? Or as: "some $x$ is the double of every $m$" ?

The "usual" convention is that we can omit the universal quantifier.

If we apply it, we read:

$\exists m \ (x = 2m)$

as: $\forall x \exists m \ (x=2m)$, i.e. as: "every number is even".

---

Regarding the second part of the question, if we write, for $x \ne 1$: $\text{Prime}(x)$ as $\forall a (a|x \to \ldots)$, clearly:

$\text{Comp}(x) \text { iff } \lnot \text {Prime}(x) \text { iff } \lnot \forall a (a|x \to \ldots) \text { iff } \exists x \lnot (a|x \to \ldots)$.

Answer 2

Notice how '$x$ is even' makes explicit reference to $x$, but not to $m$. That should be an indication already that in your formula you want $x$ as a free variable (i.e do not quantify the $x$) but not $m$, so use:

$$\exists m \ x = 2m$$

Also note that depending on how you quantify the $x$, you get a different statement:

$$\forall x \exists m \ x =2m$$

means that all numbers are even, while

$\exists x \exists m \ x=2m$

means that some number is even. (note that in both interpretations there is no longer a reference to $x$, again signaling that the $x$ has been quantified)

Likewise, the meaning of

$$x =2m$$

(which, by itself, reads as '$x$ is twice $m$' ... so now you do have an explicit reference to $m$, reflecting the fact that $m$ is a free variable)

depends on how $m$ is being quantified:

$$\exists m \ x=2m$$

clearly means that $x$ is even, while

$$\forall m \ x =2m$$

clearly means something different!

So yes, you really want to existentially quantify that $m$.

Same story for '$x$ is composite': it makes no reference to any $a$, and so you do need to quantify that $a$ and have only $x$ as a free variable. And also note that if you were to quantify the $a$ existentially, you don't get what you want.

Finally, for '$x$ is composite' it makes sense to just negate whatever you have for '$x$ is a prime' (and hence any quantificational issues will be taken care of automatically) ... if it weren't for the fact that $1$ is neither prime nor composite! So what you really want there is '$x$ is not $1$ and $x$ is not prime'

Answer 3

If so, does it mean that we can always omit the existential quantifier?

Not exactly, but there is a rigorous way of removing existential quantifiers. It is called skolemization, and follows a 3-step process:

1. Move all quantifiers outwards, giving you prenex normal form. This is typically pretty straightforward but may require minor restructuring of the formula.
2. Move existential quantifiers outside of universal quantifiers. If your expression is of the form $\forall x \exists y \phi(x, y)$, it is claiming that for each x, there is a y. You can rephrase that as there is a single function which maps x's to y's, which we write as $\exists f \forall x \phi(x, f(x))$. In this context, we call $f$ a skolem function.
3. Delete all existential quantifiers. The variables which were bound to those quantifiers become free. These free variables may then be unified with any suitable terms which satisfy the predicate.

Because we unbind the variables in step 3, this changes the meaning of the statement (instead of merely claiming that there is an $f$ or $y$ satisfies the requirement, we are claiming that $f$ or $y$ has some independent meaning which satisfies the formula). As a result, this is not a general-purpose technique, and must be used with care. However, the altered statement is equisatisfiable with the original, which makes it suitable for automated theorem proving and other contexts where satisfiability is the object of our investigation.

Unfortunately, we cannot stop at step 2, if we want to remain within first-order logic. Existential quantifiers over functions are only allowed in second-order logic; the formula shown in step 2 is ill-formed in first-order logic. It is quite possible to perform this transformation without taking that detour through second-order logic (by dropping the existential quantifier at the same time as we introduce the skolem function), but that's a little harder to follow.

In practice, skolemization is often combined with a conversion to conjunctive normal form, because that is a prerequisite to applying resolution.