 But if \(A(x)\) abbreviates \(\exists y(y\gt x \oldand B(y)),\) then in order to assert \(\forall x (A(x) \vee \neg A(x))\) intuitionistically we would need an effective (cf.  the Church-Turing thesis)  method to determine whether or not there is a pair of twin primes larger than an arbitrary natural number \(x,\) and so far no such method is known. An obvious semi-effective method is to list the prime number pairs using a refinement of Eratosthenes’ sieve (generating the natural numbers one by one and striking out every number \(y\) which fails to satisfy \(B(y)\)), and if there is a pair of twin primes larger than \(x\) this method will eventually find the first one. However, \(\forall x A(x)\) expresses the Twin Primes Conjecture, which has not yet been proved or disproved, so in the present state of our knowledge we can assert neither \(\forall x (A(x) \vee \neg A(x))\) nor \(\forall x A(x) \vee \neg \forall x A(x).\)