Непротиворечивость — свойство
формальной системы, состоящее в том, что не каждая формула этой системы доказуема в ней. Формальные системы, обладающие этим свойством, называются непротиворечивыми, или
формально непротиворечивыми. В противном случае формальная система называется
противоречивой, или
несовместной. Для широкого класса формальных систем, язык которых содержит знак отрицания,
эквивалентна свойству: «не существует такой формулы
, что
и
обе доказуемы». Класс формул данной формальной системы называется непротиворечивым, если не всякая формула этой системы выводима из данного класса. Формальная система называется
содержательно непротиворечивой, если существует
модель, в которой истинны все теоремы этой системы. Если формальная система содержательно непротиворечива, то она формально непротиворечива. Для формальных систем, основанных на классическом
исчислении предикатов, справедливо и обратное утверждение: в силу теоремы Гёделя о полноте классического исчисления предикатов, всякая такая непротиворечивая система имеет модель. Таким образом, один из способов доказательства непротиворечивости формальной системы состоит в построении модели. Другой, так называемый
метаматематический метод доказательства непротиворечивости, предложенный в начале 20 в.
Гильбертом, состоит в том, что утверждение о непротиворечивости некоторой формальной системы рассматривается как высказывание о доказательствах, возможных в этой системе. Теория, объектами которой являются произвольные математические доказательства, называется
теорией доказательств, или метаматематикой. Примером применения метаматематического метода может служить предложенное Генценом () доказательство непротиворечивости формальной системы арифметики.