In this paper we propose a deep revision of the classical ontological arguments of Anselm, Descartes, Leibniz and Spinoza. The introduction clarifies the concept of ontological argument and point out the important logic distinction between the validity of an argument and its soundness, where besides validity it is required that all premises are actually true. The following sections discuss in turn the arguments of Anselm, Descartes, Spinoza and Leibniz. In all cases we have translated the relevant passages of the original argument and formalized its hypothesis and conclusion. In some cases we reconstructed the whole argument and added as hypothesis all statements that served the authors to prove their thesis. By doing this we detached ourselves from what is traditionally considered the argument (for example, as seen in Logic and Theism [Sobel]) and most of the arguments become formally valid.We are aware of the fact that in this way we made explicit the hidden assumptions that made the argument valid while weakening its strength. The reason why is that the new hypothesis are hard to justify as in many cases they have philosophical import and they even committed the fallacy known as petitio principii. Very often the new hypothesis are existential statements, which clearly allow passing from a definition, which simply establishes a correspondence between properties, to an assumption of consistency, stating that certain sets are not empty. The paper includes the issues relevant to this study: the consideration of existence as a predicate, improper descriptions, existential import of universal statements, modal categories and the eventual modal collapse. We should highlight the effort of formalization for which we have used several logics: classical first order logic, higher order (with a description operator) and modal logic. We conclude by pointing out that the subject of ontological arguments still fascinate logicians and philosophers and received attention in the twentieth and the twenty first century.