Gödel’s completeness theorem for first-order logic implies that ZFC is consistent—i.e., no contradiction can be derived from it—if and only if it has a model. A model of ZFC is a pair \((M,E)\), where \(M\) is a non-empty set and \(E\) is a binary relation on \(M\) such that all the axioms of ZFC are true when interpreted in \((M,E)\), i.e., when the variables that appear in the axioms range over elements of \(M\), and \(\in\) is interpreted as \(E\). Thus, if \(\varphi\) is a sentence of the language of set theory and one can find a model of ZFC in which \(\varphi\) holds, then its negation \(\neg \varphi\) cannot be proved in ZFC. Hence, if one can find a model of \(\varphi\) and also a model of \(\neg \varphi\), then \(\varphi\) is neither provable nor disprovable in ZFC, in which case we say that \(\varphi\) is undecidable in, or independent of, ZFC.