# Are these two definitions of prime numbers equal?

In Coq for instance, prime numbers are defined ${n\ is\ prime} \doteq \forall a\in \mathbb{N}: a|n \rightarrow (a=1 \vee a=n)$

Definition prime n := forall a, divides a n -> a = 1 \/ a = n.


I was experimenting with another defintion which I thought was equivalent,

Definition prime' n := ~ (exists a b, a < n /\ b < n /\ a * b = n).


or ${n\ is\ prime} \doteq \neg \exists a,b\in \mathbb{N}:a<n\wedge b<n\wedge a b = n$

My question is, are these two definitions not equal?

I was not able to prove this in Coq. (I could prove that prime n -> prime' n but note the other way around. With the second definition, I wasn't even able to prove that 0 is not prime.)

Can you point out them mistake in the second definition?

• yes they are equivalent – sashas May 8 '15 at 18:44
• You refer to "x is prime $\equiv \lnot \exists a, b \in \mathbb N\cdots$" but then you use $n$ and not $x$. Keep the variables consistent. – Jordan Glen May 8 '15 at 18:49
• The first definition seems to classify $1$ as prime. – André Nicolas May 8 '15 at 19:11
• @AndréNicolas: So does the second definition. – TonyK May 8 '15 at 19:22
• Keep in mind that Coq uses constructive logic (without the law of excluded middle) by default. Some definitions that are equivalent in classical logic won't be equivalent in Coq. I didn't think about it too hard, but I don't think that is your problem here, just something to keep in mind. – Mike Haskel May 9 '15 at 5:07

If you rule out $0$ as a part of your second definition, then your definitions will be equivalent. However, they will both be incorrect, since both will allow $1$ to be a prime number! You must also rule out $1$ as part of both definitions to make them correct and equivalent.