The theorem can be expressed more generally in terms of logical consequence. We say that a sentence "s" is a syntactic consequence of a theory "T", denoted formula_1, if "s" is provable from "T" in our deductive system. We say that "s" is a semantic consequence of "T", denoted formula_2, if "s" holds in every model of "T". The completeness theorem then says that for any first-order theory "T" with a well-orderable language, and any sentence "s" in the language of "T",