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.
Tuttavia, ad un livello più avanzato, si intende, secondo l'uso che ne fa anche [[Kurt Gödel]], per ''consistenza'' la completezza degli [[assiomi]], ovvero la possibilità che un dato [[insieme]] di assiomi possa escludere qualsivoglia [[contraddizione]] ''a priori'', e per ''coerenza'' la non contraddizione dei [[Teorema|teoremi]] sviluppati a partire da un dato insieme di assiomi rispetto ad essi. Kurt Gödel, in risposta a quanti come [[David Hilbert]] a cavallo fra Ottocento e Novecento avevano lanciato l'idea di un sistema matematico in grado di provare da solo la propria consistenza e coerenza, una cui applicazione sarebbe stata una macchina produttrice di teoremi, dimostra nei suoi [[teoremi di incompletezza di Gödel|teoremi di incompletezza]] come non esista alcun sistema logico completamente consistente e coerente, e che quindi la logica, anzi ''le'' logiche, siano intrinsecamente innumerevoli, quindi costruibili (come i [[software]]) esclusivamente dalle menti pensanti (quali gli esseri umani) in grado innanzitutto di notarne le inevitabili contraddizioni e anche stabilire di volta in volta insiemi diversi di assiomi.<ref>La dimostrazione del teorema è molto semplice da spiegare. Data la proposizione, ammissibile in qualsiasi sistema logico, ''Questo teorema non è dimostrabile'', se è dimostrabile non si dimostra e se non è dimostrabile si dimostra. Ciò implica che qualsiasi insieme di presupposti non è completamente né completo (''consistente'') né logico (''coerente'')</ref>
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 (logica matematica)|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 [[insieme numerabile|numerabili]] di insiemi.
L'esempio più semplice di teoria del primo ordine ''non'' consistente è dato dalla teoria che ha un unico simbolo predicativo ''p'' e come unico assioma:▼
▲L'Un esempio più semplice di teoria del primo ordine ''non'' consistente è dato dalla teoria che ha un unico simbolo predicativo ''pP'' e come unico assioma:
