 This elimination rule also corresponds to a common inference. Suppose that a mathematician assumes or somehow concludes that there is a natural number with a given property \(P\). She then says “let \(n\) be such a natural number, so that \(Pn\)”, and goes on to establish a sentence \(\phi\), which does not mention the number \(n\). If the derivation of \(\phi\) does not invoke anything about \(n\) (other than the assumption that it has the given property \(P)\), then \(n\) could have been any number that has the property \(P\). That is, \(n\) is an arbitrary number with property \(P\). It does not matter which number \(n\) is. Since \(\phi\) does not mention \(n\), it follows from the assertion that something has property \(P\). The provisions added to \((\exists\)E) are to guarantee that \(t\) is “arbitrary”.