According the the Godel's completeness theorem, a statement in first order logic is true if and only if it can be formally proved from the first order axioms. But what does it mean that a statement is true? Obviously, it cannot be by definition that true means provable in first order logic, because then the theorem would be trivial. So how is truth in this context defined? How do we know that something is true without referring to the completeness theorem? Clearly, to know that something is true, we must prove it. But in this context we are not allowed to prove it with first order logic, so what kind of logic is used to prove the truth? Is it some informal logic that cannot be formalized? Does this logic have a name?