By a result of Julia Robinson, we know that the first order theory of the field of rational numbers is undecidable, and in fact the same holds for any number field. In view of this, it is suggested by analogies studied by Vojta and others that the first order theory of meromorphic functions over a complete algebraically closed field should also be undecidable. Three cases naturally arise: the archimedean case, the non-archimedean case in characteristic zero, and the non-archimedean case of positive characteristic. In this talk I will discuss the main ideas in the proof of undecidability of the third case --the other two remain open. The proof uses Nevanlinna theory, and I will explain what one obtains in the number theoretical side of Vojta's analogy applied to this proof.