In his ontological proof, Gödel states (Axiom 1)
If a property is positive, then its negation is not positive.
What does he meant by this term? I have come across authors who replace this notion of positiveness with that of truth, but I doubt very much that this is what Gödel originally meant. Are there any sources on the subject?
"Positive" is what Leibniz and other proponents of the ontological argument called qualities that make something "better" than it is without them (Anselm spoke of "good" as in summum bonum). In particular, Leibniz defined "perfections" ascribed to God as "simple, positive qualities in the highest degree", see What makes Leibniz's definition of perfection unintelligible? and references there. The doctrine is much criticized, and not just for vagueness and relativity of "positive". For example, Norman Malcolm writes the following in Anselm's Ontological Arguments:
"The doctrine that existence is a perfection is remarkably queer. It makes sense and is true to say that my future house will be a better one if it is insulated than if it is not insulated; but what could it mean to say that it will be a better house if it exists than if it does not? My future child will be a better man if he is honest than if he is not; but who would understand the saying that he will be a better man if he exists than if he does not? Or who understands the saying that if God exists He is more perfect than if He does not exist? One might say, with some intelligibility, that it would be better (for oneself or for mankind) if God exists than if He does not - but that is a different matter."
Gödel was generally fascinated by Leibniz, see Why did Gödel believe that there was a conspiracy to suppress Leibniz's works?, and according to Oppy's Gödel: The Third Degree his version of the argument derives from Leibniz's:
"Gödel was interested in philosophy; in particular, he was a great admirer of Gottfried Leibniz. His interest in ontological arguments sprang from reflection upon Leibniz’s attempts to improve René Descartes ontological arguments. In the eleventh century, in his Proslogion, St. Anselm gave a derivation of the existence of that than which no greater can be conceived. In the seventeenth century, Descartes gave various derivations of the existence of a being that possesses all perfections. Leibniz refined Descartes’ argument by providing a derivation of its implicit premise: that it is possible for something to have all perfections.
[...] In the early 1940s, Gödel produced the first of several derivations that aimed to formalize Leibniz’s development of Cartesian ontological arguments. There is no evidence that Gödel showed his derivations to anyone until the early 1970s, when, under the mistaken belief that he was on his deathbed, he showed some of the relevant notebooks to Dana Scott. With Gödel’s permission, Scott copied out one of the derivations, which began to circulate privately."
Positivity is a property of unary predicates that Gödel defines implicitly, i.e. he writes axioms for positive properties. These include the one you cite and consequences of positive axioms being positive, so if any positive property were unsatisfiable all properties would be positive, a contradiction.
Similarly, Sobel showed Gödel's axioms imply there are no contingent statements. This is cited as a criticism of the "definition". As any mathematician familiar with the notion of axioms-as-definitions can tell you, it's a form of "definition" that can imply false statements, or even contradictions.
Sobel described this aspect of the axioms as "modal collapse". It is similar to the proves-too-much problem with Mally's deontic axioms, which imply a statement is morally obligatory iff it's true, or else that all or no statements are obligatory.
