theorems of the deductive system. In the broad sense in which the term is used within logic, a theorem does not have to be true, since the theory that contains it may be unsound relative to a given semantics, or relative to the standard interpretation of the underlying language. A theory that is inconsistent has all sentences as theorems. The definition of theorems as sentences of a formal language is useful within proof theory, which is a branch of mathematics that studies the structure of formal proofs and the structure of provable formulas. It is also important in model theory, which is concerned with the relationship between formal theories and structures that are able to provide a semantics for them through interpretation. Although theorems may be uninterpreted sentences, in practice mathematicians are more interested in the meanings of the sentences, i.e. in the propositions they express. What makes formal theorems useful and interesting is that they may be interpreted as true propositions and their derivations may be interpreted as a proof of their truth. A theorem whose interpretation is a true statement about a formal system (as opposed to within a formal system) is called a metatheorem. Some important theorems in mathematical logic are: Compactness of first-order logic Completeness of first-order logic Gödel's incompleteness theorems of first-order arithmetic Consistency of first-order arithmetic Tarski's undefinability theorem Church-Turing theorem of undecidability Löb's theorem Löwenheim–Skolem theorem Lindström's theorem Craig's theorem Cut-elimination theorem Syntax and semantics The concept of a formal theorem is fundamentally syntactic, in contrast to the notion of a true proposition, which introduces semantics. Different deductive systems can yield other interpretations, depending on the presumptions of the derivation rules (i.e. belief, justification or other modalities). The soundness of a formal system depends on whether or not all of its theorems are also validities. A validity is a formula that is true under any possible interpretation (for example, in classical propositional logic, validities are tautologies). A formal system is considered semantically complete when all of its theorems are also tautologies. Interpretation of a formal theorem Theorems and theories See also List of theorems List of theorems called fundamental Formula Inference Toy theorem Notes References References External links Theorem of the Day Logical consequence Logical expressions Mathematical proofs Mathematical terminology Statements de:Theorem