Введение

Непротиворечивость теории

В классической дедуктивной логике непротиворечивая теория – это теория, которая не приводит к логическому противоречию. Отсутствие противоречия может быть определено как в семантических, так и в синтаксических терминах. Семантическое определение гласит, что теория непротиворечива, если у неё есть модель, то есть существует интерпретация, при которой все формулы в теории истинны. Это значение используется в традиционной аристотелевской логике, хотя в современной математической логике вместо этого используется термин "выполнимость". Синтаксическое определение гласит, что теория непротиворечива, если не существует такой формулы, чтобы и она, и её отрицание были элементами множества следствий. Пусть Γ – множество замкнутых предложений (неформально "аксиомы"), а T – множество замкнутых предложений, доказуемых из Γ в некоторой (определённой, возможно, неявно) формальной дедуктивной системе. Множество аксиом Γ является непротиворечивым, когда не существует такой формулы φ, что φ ∈ T и ¬φ ∈ T.

Если существует дедуктивная система, для которой эти семантические и синтаксические определения эквивалентны для любой теории, сформулированной в конкретной дедуктивной логике, то эта логика называется полной. Пол Бернайс в 1918 году и Эмиль Пост в 1921 году доказали полноту исчисления высказываний, а Курт Гёдель в 1930 году доказал полноту исчисления предикатов, а доказательства непротиворечивости для арифметики, ограниченной относительно схемы аксиомы индукции, были доказаны Акерманом (1924), фон Нейманом (1927) и Гербрандом (1931). Более сильные логики, такие как логика второго порядка, не являются полными. Доказательство непротиворечивости – это математическое доказательство того, что конкретная теория непротиворечива. Раннее развитие теории математических доказательств было обусловлено стремлением предоставить конечно обоснованные доказательства непротиворечивости для всей математики в рамках программы Гильберта. На программу Гильберта сильно повлияли теоремы о неполноте, которые показали, что достаточно сильные теории доказательств не могут доказать свою непротиворечивость (при условии, что они непротиворечивы). Хотя непротиворечивость может быть доказана с помощью теории моделей, она часто доказывается чисто синтаксическим способом, без необходимости ссылаться на какую-либо модель логики. Устранение отсечений (или, эквивалентно, нормализация базового исчисления, если оно существует) подразумевает непротиворечивость исчисления: поскольку нет доказательства ложности без отсечений, нет противоречия в общем случае.

Последовательность и полнота в арифметике и теории множеств

В теориях арифметики, таких как арифметика Пеано, существует сложная взаимосвязь между последовательностью теории и её полнотой. Теория считается полной, если для каждой формулы φ в её языке хотя бы одна из формул φ или ¬φ является логическим следствием теории. Арифметика Пресбургера — это система аксиом для натуральных чисел относительно операции сложения. Она является как последовательной, так и полной. Теоремы о неполноте Гёделя показывают, что любая достаточно сильная рекурсивно перечислимая теория арифметики не может быть одновременно полной и последовательной. Теорема Гёделя применима к теориям арифметики Пеано (PA) и примитивной рекурсивной арифметики (PRA), но не к арифметике Пресбургера. Более того, вторая теорема о неполноте Гёделя показывает, что последовательность достаточно сильных рекурсивно перечислимых теорий арифметики может быть проверена определённым образом. Такая теория последовательна тогда и только тогда, когда она не доказывает конкретное предложение, называемое Гёделевым предложением теории, которое является формализованным выражением утверждения о том, что теория действительно последовательна. Таким образом, последовательность достаточно сильной, рекурсивно перечислимой, последовательной теории арифметики не может быть доказана внутри самой этой системы. Тот же результат справедлив для рекурсивно перечислимых теорий, способных описать достаточно сильный фрагмент арифметики, включая теории множеств, такие как теория множеств Цермело — Френкеля (ZF). Эти теории множеств не могут доказать собственное Гёделево предложение, при условии, что они последовательны, что обычно принимается. Поскольку последовательность ZF не доказуема в ZF, более слабое понятие независимости интересно в теории множеств (и в других достаточно выразительных аксиоматических системах). Если T — теория, а A — дополнительная аксиома, то T + A считается последовательной относительно T (или просто, что A согласуется с T), если можно доказать, что если T последовательна, то T + A также последовательна. Если как A, так и ¬A согласуются с T, то A считается независимой от T.

Обозначение

В контексте математической логики символ "турникет" означает "доказуемо из". То есть, ⊢ читается: "b доказуемо из a" (в некоторой заданной формальной системе).

Определение

Набор формул в логике первого порядка называется согласованным (обозначается ) если не существует формулы , такой что и . В противном случае набор формул называется несогласованным (обозначается ). Набор формул называется просто согласованным, если для любой формулы из этого набора, ни сама формула, ни её отрицание не являются теоремами этого набора. Набор формул называется абсолютно согласованным или пост-согласованным, если хотя бы одна формула на языке этого набора не является теоремой этого набора. Набор формул называется максимально согласованным, если он согласован и для любой формулы , из следует . Говорят, что набор формул содержит свидетели, если для каждой формулы вида существует терм , такой что , где обозначает замену каждой переменной в на . См. также логику первого порядка.

Схема доказательства

Есть несколько моментов, которые необходимо проверить. Во-первых, нужно удостовериться, что это действительно отношение эквивалентности. Затем необходимо проверить, что (1), (2) и (3) определены корректно. Это следует из того факта, что это отношение эквивалентности, и также требует доказательства независимости (1) и (2) от выбора представителей класса. Наконец, можно проверить индукцией по формулам.

Теория моделей

В теории множеств ZFC с классической логикой первого порядка, несовместимая теория – это такая, для которой существует замкнутое предложение, содержащее как само это предложение, так и его отрицание. Согласованная теория – это такая, для которой выполняются следующие логически эквивалентные условия.