 The proofs which Turing and Church gave of these facts are constructive in the sense that they show how to effectively transform an individual instance of one of the models into a first-order formula such that the formula is valid if and only if the instance possesses the property in question—e.g., given a Turing machine \(T_i\) and input \(n \in \mathbb{N}\), we construct a formula \(\varphi_{i,n}\) such that the computation \(T_i(n)\) halts if and only if \(\varphi_{i,n}\) is valid. This method thus anticipates the definition of  many-one reducibility given in  Section 3.5.1  below.