A formalization of the Turing machines through first-order logic is proposed. In this formalization, Turing machines are defined in terms of first-order structures and, thus, the existence of non-standard elements in Turing machines, similar to those models of first-order arithmetic, is proved. This permits to invesigate some properties of Turing computability over non-standard natural numbers. Finally, some consequences of this approach for important problems related to Turing machines are analised, notably the Máté-Sureson's model-theoretical caracterization of the problem NP=?CoNP.