Twin primes are pairs of numbers $p$ and $p+2$ such that both are primes—for instance, $5$ and $7$, $11$ and $13$, $41$ and $43$. The Twin Prime Conjecture says that there are infinitely many twin primes.
Let $\text{TwinPrime}(n)$ be a predicate that is true if $n$ and $n+2$ are twin primes. Which of the following formulas, interpreted over positive integers, expresses that there are only finitely many twin primes?
- $\forall m \cdot \exists n \cdot m \leq n \text{ and not(TwinPrime}(n))$
- $\exists m \cdot \forall n \cdot n \leq m \text{ implies TwinPrime}(n)$
- $\forall m \cdot \exists n \cdot n \leq m \text{ and TwinPrime}(n)$
- $\exists m \cdot \forall n \cdot \text{TwinPrime}(n) \text{ implies }n \leq m$