Полнота/необоснованность логики второго порядка

Набросок доказательства

1) Мы определяем синтаксис для SOL и соответствующий дедуктивный аппарат, добавляя аксиомы и правила для управления количественной оценкой второго порядка (см., например , van Dalen, Logic and Structure (2013), Ch.5 ).

2) Определяем «стандартную» семантику для языка.

3) Определим понятие стандартно допустимого , естественным образом расширяя понятие ВОЛС.

Затем доказываем:

Теорема обоснованности : каждая теорема исчисления предикатов второго порядка стандартно верна.

4) Мы рассматриваем версию аксиом Пеано для ФОЛ плюс аксиому индукции ; важно отметить, что в версии SOL индукция — это формула, а не схема аксиом .

5) Пусть AR2 будет конъюнкцией аксиом первого порядка формальной арифметики плюс аксиома второго порядка математической индукции.

Мы доказываем, что:

Любые две стандартные интерпретации M и M' , являющиеся моделями AR2 , изоморфны .

6) Пусть L2A — язык второго порядка для арифметики (с нелогическими константами формальной арифметики: ноль, последующий элемент, сложение, умножение).

Пусть N будет стандартной интерпретацией L2A с набором натуральных чисел в качестве области определения и обычными интерпретациями нелогических констант.

Докажем (используя 5), что:

Пусть B — любая формула языка арифметики. Тогда B истинно в N тогда и только тогда, когда AR2 ⇒ B стандартно верно .

7) Докажем, что:

Множество SV стандартно корректных формул языка L2A не является эффективно перечислимым.

Предположим, что SV эффективно перечислимо. Тогда по 6 мы могли бы эффективно перечислить множество TR всех истинных формул арифметики первого порядка, перебрав SV , найдя все формулы вида AR2 ⇒ B , где B — формула арифметики первого порядка, и перечислив те формулы Б. _ Тогда теория TR была бы разрешима (что не так), поскольку для любой замкнутой формулы C мы могли бы эффективно перечислять TR до тех пор, пока не появится либо C , либо ее отрицание.

8) Из 7 получаем, что множество всех стандартно верных формул не является эффективно перечислимым.

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

9) Не существует эффективной формальной системы, теоремы которой являются стандартно действительными формулами L2A .

Если бы существовала такая система аксиом, мы могли бы перечислить стандартно верные формулы L2A , противоречащие 7.

10) Неполнота стандартной семантики : не существует эффективной формальной системы, все теоремы которой являются стандартно действительными формулами.

Если бы существовала такая система аксиом, мы могли бы перечислить множество всех стандартных правильных формул, противоречащих 8.

Последний факт четко отличает логику второго порядка от логики первого порядка, поскольку теорема Гёделя о полноте говорит нам, что существует эффективная формальная система, все теоремы которой являются логически верными формулами первого порядка.

Это сложное доказательство.

Предположим, у нас есть исчисление предикатов первого порядка и базовая арифметика. Мы можем кодировать логические утверждения численно. (Например, к тому моменту, когда кто-либо прочитает ее, вся эта запись представляется строкой битов.) Теперь, предположив, что у нас есть жесткая логическая система с аксиомами и правилами вывода, мы можем доказать некоторые утверждения, и мы можем доказать, что некоторые не может быть доказано. Например, при наличии разумных аксиом и правил вывода можно доказать, что «3 — простое число», но нельзя доказать, что «3 — составное число». У нас есть три класса предложений: одни мы можем доказать истинными, другие мы можем доказать ложными и те, которые мы пока не можем доказать ни тем, ни другим способом.

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

Доказуемость — это числовое отношение. Можно выразить численно, если предложение может быть доказано. Таким образом, доказуемость является числовым отношением, и мы можем выразить это отношение в предложении, которое мы можем превратить в невообразимо большое число, которое мы также можем назвать N. Мы также можем создать число U, представляющее дополнение доказуемости.

Зная U, мы можем построить число P. (Представьте, что мы придумали его, пока вы в туалете, поскольку я не помню деталей.) Когда мы расшифровываем P, мы читаем, что утверждение P недоказуемо.

Теперь есть две возможности. P может быть истинным, и в этом случае у нас есть истинное утверждение, которое нельзя доказать, поэтому логическая система неполна. Оно может быть ложным, и в этом случае оно доказуемо, и мы можем доказать ложное суждение, поэтому логическая система несостоятельна.

Теперь мы можем добавить правила, чтобы исправить это, чтобы P было либо доказуемо истинным, либо доказуемо ложным. В этот момент мы изменили то, что такое доказуемость, поэтому мы получили гораздо большее, невообразимо большое число N1, и, таким образом, получили U1 и придумали новое P1, которое говорит: «Утверждение P1 недоказуемо даже с нашими новыми правилами». , и мы вернулись к тому, с чего начали.