Gödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic. The completeness theorem applies to any first order theory: If T is such a theory, and φ is a sentence (in the same language) and any model of T is a model of φ, then there is a (first-order) proof of φ using the statements of T as axioms. One sometimes says this as "anything true is provable".