In logica matematica, una teoria formale si dice coerente (o non contraddittoria, talvolta anche consistente, per assonanza con l’inglese consistent) se in essa è impossibile dimostrare una contraddizione. A priori si distiguono due livelli di consistenza: consistenza sintattica se nella teoria non si possono dimostrare contemporaneamente una formula ben formata e la sua negazione; consistenza semantica se la teoria ammette almeno un modello. Si dimostra che per una teoria del primo ordine ciascuno dei due tipi di consistenza implica l’altro. Dimostrare una delle due implicazioni è semplice mentre dimostrare che una teoria sintatticamente consistente ammette sempre un modello è la parte non banale della dimostrazione e richiede l’utilizzo dell’assioma della scelta per famiglie numerabili di insiemi. Un esempio semplice di teoria del primo ordine non consistente è dato dalla teoria che ha un unico simbolo predicativo P e come unico assioma: :