Последовательность - Consistency

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

Если существует дедуктивная система, для которой эти семантические и синтаксические определения эквивалентны любой теории, сформулированной в определенной дедуктивной логике , такая логика называется полной . Полнота сентенционного исчисления была доказана Павла Бернайс в 1918 году и Эмиля Post в 1921 году, в то время как полнота исчисления предикатов была доказана Куртом Геделем в 1930 году, и последовательность доказательство для арифметики ограниченной по отношению к схеме индукции аксиомы было доказано Ackermann (1924), фон Нейман (1927) и Хербранд (1931). Более строгие логики, такие как логика второго порядка , неполны.

Доказательство непротиворечивости является математическим доказательством , что конкретная теория непротиворечива. Раннее развитие математической теории доказательств было вызвано желанием предоставить доказательства конечной непротиворечивости для всей математики как часть программы Гильберта . На программу Гильберта сильно повлияли теоремы о неполноте , которые показали, что достаточно сильные теории доказательства не могут доказать свою собственную непротиворечивость (при условии, что они на самом деле непротиворечивы).

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

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

В теориях арифметики, таких как арифметика Пеано , существует сложная взаимосвязь между последовательностью теории и ее полнотой . Теория считается полной, если для каждой формулы φ на ее языке хотя бы одно из φ или ¬φ является логическим следствием теории.

Арифметика Пресбургера - это система аксиом для сложения натуральных чисел. Оно одновременно последовательное и полное.

Теоремы Гёделя о неполноте показывают, что любая достаточно сильная рекурсивно перечислимая теория арифметики не может быть одновременно полной и непротиворечивой. Теорема Гёделя применима к теориям арифметики Пеано (PA) и примитивно-рекурсивной арифметике (PRA), но не к арифметике Пресбургера .

Более того, вторая теорема Гёделя о неполноте показывает, что непротиворечивость достаточно сильных рекурсивно перечислимых теорий арифметики может быть проверена определенным образом. Такая теория непротиворечива тогда и только тогда, когда она не доказывает конкретное предложение, называемое гёделевским предложением теории, которое является формализованным заявлением о том, что теория действительно непротиворечива. Таким образом, непротиворечивость достаточно сильной, рекурсивно перечислимой и непротиворечивой теории арифметики никогда не может быть доказана в самой этой системе. Тот же результат верен для рекурсивно перечислимых теорий, которые могут описывать достаточно сильный фрагмент арифметики, включая теории множеств, такие как теория множеств Цермело – Френкеля (ZF). Эти теории множеств не могут доказать свое собственное предложение Гёделя - при условии, что они непротиворечивы, как принято считать.

Поскольку непротиворечивость ZF недоказуема в ZF, более слабое понятие относительная согласованность интересна в теории множеств (и в других достаточно выразительных аксиоматических системах). ЕслиT-теория,аA- дополнительнаяаксиома,T+Aназывается согласованным относительноT(или простоAсогласовано сT), если можно доказать, что еслиTсогласован, тоT+Aсогласован. Если обаи ¬согласуются сТ, тоназываетсянезависимымотТ.

Логика первого порядка

Обозначение

(Символ турникета) в следующем контексте математической логики означает «доказуемо из». То есть читается так: b доказуемо из a (в некоторой указанной формальной системе). См. Список логических символов . В остальных случаях символ турникета может означать подразумевает; позволяет получить. См .: Список математических символов .

Определение

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

Основные результаты

  1. Следующие варианты эквивалентны:
    1. Для всех
  2. Каждый выполнимый набор формул является непротиворечивым, причем набор формул выполним тогда и только тогда, когда существует такая модель , что .
  3. Для всех и :
    1. если нет , то ;
    2. если и , то ;
    3. если , то или .
  4. Позвольте быть максимально непротиворечивым набором формул и предположим, что он содержит свидетелей . Для всех и :
    1. если , то ,
    2. либо, либо ,
    3. если и только если или ,
    4. если и , то ,
    5. тогда и только тогда, когда есть такой термин , что .

Теорема Хенкина

Позвольте быть набор символов . Пусть - максимально непротиворечивый набор -формул, содержащий свидетелей .

Определите отношение эквивалентности на множестве -термов, если , где означает равенство . Обозначим через класс эквивалентности терминов, содержащих ; и пусть где - набор терминов, основанный на наборе символов .

Определить - структуру более , также называется термином-структура , соответствующая , по:

  1. для каждого символа -арного отношения определите, если
  2. для каждого -арного функционального символа определите
  3. для каждого постоянного символа определите

Определите назначение переменной по каждой переменной . Позвольте быть термин интерпретация, связанный с .

Затем для каждой формулы :

если и только если

Эскиз доказательства

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

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

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

Смотрите также

Сноски

использованная литература

внешние ссылки