stringtranslate.com

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

В классической дедуктивной логике непротиворечивой является теория , которая не приводит к логическому противоречию . [1] Теория непротиворечива , если не существует формулы, такой что и ее отрицание являются элементами множества следствий . Пусть будет множеством замкнутых предложений (неформально «аксиом») и множеством замкнутых предложений, доказуемых из некоторой (указанной, возможно, неявно) формальной дедуктивной системы. Множество аксиом непротиворечиво , когда не существует формулы, такой что и . Тривиальная теория (т. е. та, которая доказывает каждое предложение на языке теории) явно непротиворечива. Наоборот, во взрывной формальной системе (например, классической или интуиционистской пропозициональной или первопорядковой логике) каждая непротиворечивая теория тривиальна. [2] : 7  Непротиворечивость теории является синтаксическим понятием, семантическим аналогом которого является выполнимость . Теория выполнима, если у нее есть модель , т. е. существует интерпретация , при которой все аксиомы теории истинны. [3] Именно это и означало слово «согласованный» в традиционной аристотелевской логике , хотя в современной математической логике вместо этого используется термин «выполнимый» .

В надежной формальной системе каждая выполнимая теория непротиворечива, но обратное не верно. Если существует дедуктивная система, для которой эти семантические и синтаксические определения эквивалентны для любой теории, сформулированной в конкретной дедуктивной логике , логика называется полной . [ требуется цитирование ] Полнота исчисления высказываний была доказана Полом Бернайсом в 1918 году [ требуется цитирование ] [4] и Эмилем Постом в 1921 году [5] , в то время как полнота исчисления предикатов (первого порядка) была доказана Куртом Гёделем в 1930 году [6] , а доказательства непротиворечивости для арифметики, ограниченной относительно схемы аксиом индукции, были доказаны Аккерманом (1924), фон Нейманом (1927) и Гербрандом (1931). [7] Более сильные логики, такие как логика второго порядка , не являются полными.

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

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

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

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

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

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

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

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

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

Обозначение

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

Определение

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

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

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

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

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

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

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

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

Тогда для каждой -формулы :

если и только если [ необходима цитата ]

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

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

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

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

  1. [11]

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

Примечания

  1. ^ Тарский 1946 формулирует это следующим образом: «Дедуктивная теория называется последовательной или непротиворечивой, если никакие два утверждаемых утверждения этой теории не противоречат друг другу, или, другими словами, если из любых двух противоречащих предложений … по крайней мере одно не может быть доказано» (стр. 135), где Тарский определяет противоречивость следующим образом: «С помощью слова не образуется отрицание любого предложения; два предложения, из которых первое является отрицанием второго, называются противоречивыми предложениями » (стр. 20). Это определение требует понятия «доказательство». Гедель 1931 определяет это понятие следующим образом: «Класс доказуемых формул определяется как наименьший класс формул, который содержит аксиомы и замкнут относительно отношения «непосредственное следствие», т. е. формула c из a и b определяется как непосредственное следствие в терминах modus ponens или подстановки; см. Гедель 1931, ван Хейеноорт 1967, стр. 601. Тарский неформально определяет «доказательство» как «утверждения, следующие друг за другом в определенном порядке в соответствии с определенными принципами … и сопровождаемые соображениями, призванными установить их действительность [истинное заключение] для всех истинных посылок» – Рейхенбах 1947, стр. 68]" см. Tarski 1946, стр. 3. Kleene 1952 определяет понятие относительно либо индукции, либо (как парафраз) конечной последовательности формул, такой, что каждая формула в последовательности является либо аксиомой, либо "непосредственным следствием" предыдущих формул; " Говорят, что доказательство является доказательством своей последней формулы, и говорят, что эта формула (формально) доказуема или является (формальной) теоремой" см. Kleene 1952, стр. 83.
  2. ^ Карниелли, Вальтер; Конильо, Марсело Эстебан (2016). Параконсистентная логика: последовательность, противоречие и отрицание . Логика, эпистемология и единство науки. Том 40. Cham: Springer. doi :10.1007/978-3-319-33205-5. ISBN 978-3-319-33203-1. MR  3822731. Zbl  1355.03001.
  3. ^ Hodges, Wilfrid (1997). A Shorter Model Theory . New York: Cambridge University Press. p. 37. Пусть будет сигнатурой, теорией в и предложением в . Мы говорим, что является следствием , или что влечет , в символах , если каждая модель из является моделью . (В частности, если не имеет моделей, то влечет .) Предупреждение : мы не требуем, чтобы если то было доказательство из . В любом случае, с бесконечными языками не всегда ясно, что будет составлять доказательство. Некоторые авторы используют для обозначения того, что выводимо из в некотором конкретном формальном исчислении доказательств, и они пишут для нашего понятия вывода (обозначение, которое конфликтует с нашим ). Для логики первого порядка два вида вывода совпадают по теореме о полноте для рассматриваемого исчисления доказательств. Мы говорим, что является допустимым , или является логической теоремой , в символах , если является истинным в каждой -структуре. Мы говорим, что это согласовано , если истинно в некоторой -структуре. Аналогично, мы говорим, что теория согласована, если у нее есть модель. Мы говорим, что две теории S и T в L infinity omega эквивалентны, если у них одинаковые модели, т.е. если Mod(S) = Mod(T).


    (Обратите внимание на определение Mod(T) на стр. 30 ...)
  4. ^ van Heijenoort 1967, стр. 265 утверждает, что Бернейс определил независимость аксиом Principia Mathematica , результат, опубликованный только в 1926 году, но он ничего не говорит о том, что Бернейс доказал их непротиворечивость .
  5. ^ Пост доказывает как непротиворечивость, так и полноту исчисления высказываний PM, см. комментарий ван Хейеноорта и « Введение в общую теорию элементарных высказываний» Поста 1931 года в van Heijenoort 1967, стр. 264 и далее. Также Tarski 1946, стр. 134 и далее.
  6. ^ см. комментарий ван Хейеноорта и работу Гёделя 1930 года «Полнота аксиом функционального исчисления логики» в ван Хейеноорте 1967, стр. 582 и далее.
  7. ^ см. комментарий ван Хейеноорта и статью Эрбрана 1930 г. « О непротиворечивости арифметики» в ван Хейеноорте 1967 г., стр. 618 и далее.
  8. ^ Доказательство непротиворечивости часто предполагает непротиворечивость другой теории. В большинстве случаев эта другая теория — теория множеств Цермело–Френкеля с аксиомой выбора или без нее (это эквивалентно, поскольку эти две теории были доказаны как равнонепротиворечивые; то есть, если одна непротиворечива, то же самое верно и для другой).
  9. ^ Это определение не зависит от выбора из-за свойств замещаемости и максимальной согласованности .
  10. ^ общий случай во многих приложениях к другим областям математики, а также обычный способ рассуждения неформальной математики в исчислении и приложениях к физике, химии, технике
  11. ^ согласно законам Де Моргана

Ссылки

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