 That this property does not hold in PA follows from the fact that PA proves \(\exists x (A(x) \vee \forall y \neg A(y))\). Consider, for example, the case that \(A(x)\) is the formula \(T(e,e,x)\), where \(T\) is the decidable Kleene predicate expressing that \(x\) is the code of a terminating computation of the program with code \(e\) on input \(e\). If for every \(e\) there would exist a number \(n\) such that \({\bf PA}\vdash T(e,e,n) \vee \forall y \neg T(e,e,y)\), then by checking whether \(T(e,e,n)\) holds it would be decided whether a program \(e\) terminates on input \(e\). This, however, is in general undecidable. 