The property of a formal system requiring that not every formula of the system is provable in it. Formal systems having this property are called consistent or formally consistent. In the opposite case the formal system is called contradictory or inconsistent. For the broad class of formal systems whose language contains the negation symbol $\neg$, consistency is equivalent to the property that "there is no formula $\phi$ such that both $\phi$ and $\neg\phi$ are provable". A class of formulas of a given formal system is called consistent if not every formula of the system is deducible from the given class. A formal system is called satisfiable if there is a model in which all theorems of the system are true. If a formal system is satisfiable, then it is consistent. For formal systems based on classical predicate calculus the converse is also true: by the Gödel completeness theorem for classical predicate calculus, every such consistent system has a model. Thus, one of the methods of proving the consistency of a formal system consists in constructing a model. Another (meta-mathematical) method, put forward at the beginning of the 20th century by D. Hilbert, consists in the fact that the assertion of the consistency of a certain formal system can be regarded as a statement on the proofs that are possible in this system. A theory whose objects are arbitrary mathematical proofs is called a proof theory or a meta-mathematics. An example of the application of a meta-mathematical method is the proof due to G. Gentzen of the consistency of the formal system of arithmetic (see Gentzen formal system).