Непротиворечи́вость, свойство аксиоматической теории, состоящее в том, что в этой теории нельзя получить противоречие, т. е. доказать некоторое предложение и вместе с тем его отрицание или доказать заведомо абсурдное утверждение. Для широкого класса аксиоматических теорий (в частности, для тех, в основе которых лежит обычная логика) непротиворечивость имеет место тогда и только тогда, когда существует предложение, формулируемое в данной теории и недоказуемое в ней.

Понятие непротиворечивости и методы доказательства непротиворечивости аксиоматических теорий развивались и уточнялись вместе с развитием аксиоматического метода. Для т. н. материальных аксиоматик, т. е. аксиоматических теорий, в которых значения исходных терминов считаются заданными с самого начала, вопрос о непротиворечивости сколько-нибудь остро не стоял. Например, интуитивная убеждённость в непротиворечивости аксиоматической системы евклидовой геометрии основывается на «опыте», поскольку эти аксиомы – очевидные предложения о геометрических объектах. Построение неевклидовых геометрий и связанное с ним возникновение формальных аксиоматик впервые поставило проблему доказательства непротиворечивости аксиоматических теорий. Так, геометрия Лобачевского получается из евклидовой геометрии заменой аксиомы о параллельных другим постулатом, противоречащим тем интуитивным представлениям, в силу которых признаются истинными аксиомы Евклида. Поэтому непротиворечивость геометрии Лобачевского не усматривается непосредственно из «опыта» и требует своего обоснования. Первые результаты о непротиворечивости аксиоматических теорий были получены с помощью метода интерпретаций, который состоит в том, что исходным понятиям исследуемой теории сопоставляются некоторые конкретные математические объекты, причём аксиомы оказываются истинными утверждениями об этих объектах. Примером применения этого метода может служить интерпретация Клейна для системы аксиом геометрии Лобачевского. В этой интерпретации плоскость трактуется как внутренность круга на обычной евклидовой плоскости, а прямые – как хорды этого круга.

Другой метод доказательства непротиворечивости (метаматематический метод) был предложен Д. Гильбертом. Он связан с представлением аксиоматической теории в виде формальной системы. Утверждение о непротиворечивости некоторой формальной системы означает, что среди доказательств, возможных в этой системе, нет двух таких, одно из которых является доказательством некоторой формулы, а другое – доказательством её отрицания. Выдвинутая Гильбертом программа обоснования математики состояла в установлении непротиворечивости её разделов путём анализа доказательств в соответствующих формальных системах. Теория, объектами которой являются произвольные математические доказательства, называется теорией доказательств или метаматематикой. Примером применения метаматематического метода может служить предложенное в 1936 г. немецким математиком Г. Генценом доказательство непротиворечивости формальной системы арифметики.

Любое математическое доказательство непротиворечивости является относительным: оно лишь сводит вопрос о непротиворечивости одной теории к вопросу о непротиворечивости другой теории. Это особенно наглядно проявляется в методе интерпретаций. Объекты, служащие для интерпретации исходных понятий данной аксиоматической теории $T$, сами оказываются предметом рассмотрения некоторой другой математической теории $T'$, и полученное этим методом доказательство непротиворечивости теории $T$ действительно лишь в случае, если теория $T'$ непротиворечива. Таким образом, например, была установлена непротиворечивость геометрии Лобачевского в предположении непротиворечивости геометрии Евклида, а вопрос о непротиворечивости последней был сведён к проблеме непротиворечивости арифметики.

Метаматематический метод доказательства непротиворечивости не требует построения интерпретации для каждой конкретной теории. Оставаясь по сути своей относительным, метаматематическое доказательство непротиворечивости сводит вопрос о непротиворечивости данной теории к вопросу о надёжности метаматематики, объекты которой не зависят от содержания конкретной рассматриваемой теории. В этом состоит одно из главных преимуществ метаматематического метода перед методом интерпретаций. Программа Д. Гильберта предусматривала использование в метаматематике лишь таких понятий и методов, надёжность которых не вызывает сомнений.

Цель всякого доказательства непротиворечивости – свести вопрос о непротиворечивости данной теории к аналогичному вопросу для такой теории, непротиворечивость которой представляется более обоснованной. В этой связи большое значение имеет теорема Гёделя о неполноте, которая утверждает, что непротиворечивость аксиоматической теории, содержащей арифметику, невозможно доказать с помощью средств самой рассматриваемой теории. Таким образом, вопрос о непротиворечивости данной теории может быть решён лишь с привлечением средств некоторой более сильной теории.