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?

  • $\begingroup$ yes they are equivalent $\endgroup$ – sashas May 8 '15 at 18:44
  • $\begingroup$ 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. $\endgroup$ – Jordan Glen May 8 '15 at 18:49
  • 2
    $\begingroup$ The first definition seems to classify $1$ as prime. $\endgroup$ – André Nicolas May 8 '15 at 19:11
  • 1
    $\begingroup$ @AndréNicolas: So does the second definition. $\endgroup$ – TonyK May 8 '15 at 19:22
  • 1
    $\begingroup$ 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. $\endgroup$ – 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.


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.