language of is not a theorem of . is said to be maximally consistent if is consistent and for every formula , implies . is said to contain witnesses if for every formula of the form there exists a term such that , where denotes the substitution of each in by a ; see also First-order logic. Basic results The following are equivalent: For all Every satisfiable set of formulas is consistent, where a set of formulas is satisfiable if and only if there exists a model such that . For all and : if not , then ; if and , then ; if , then or . Let be a maximally consistent set of formulas and suppose it contains witnesses. For all and : if , then , either or , if and only if or , if and , then , if and only if there is a term such that . Henkin's theorem Let be a set of symbols. Let be a maximally consistent set of -formulas containing witnesses. Define an equivalence relation on the set of -terms by if , where denotes equality. Let denote the equivalence class of terms containing ; and let where is the set of terms based on the set of symbols . Define the -structure over , also called the term-structure corresponding to , by: for each -ary relation symbol , define if for each -ary function symbol , define for each constant symbol , define Define a variable assignment by for each variable . Let be the term interpretation associated with . Then for each -formula : Sketch of proof There are several things to verify. First, that is in fact an equivalence relation. Then, it needs to be verified that (1), (2), and (3) are well defined. This falls out of the fact that is an equivalence relation and also requires a proof that (1) and (2) are independent of the choice of class representatives. Finally, can be verified by induction on formulas. Model theory In ZFC set theory with classical first-order logic, an inconsistent theory is one such that there exists a closed sentence such that contains both and its negation . A consistent theory is one such that the following logically equivalent conditions hold See also Cognitive dissonance Equiconsistency Hilbert's problems Hilbert's second problem Jan Łukasiewicz Paraconsistent logic ω-consistency Gentzen's consistency proof Proof by contradiction Footnotes