Введение

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

Определение

Теория T называется интерпретирующей язык арифметики, если существует перевод формул арифметики на язык T, такой, что T способна доказать основные аксиомы натуральных чисел при этом переводе. Теория T, интерпретирующая арифметику, называется ω-несовместимой, если для некоторого свойства P натуральных чисел (определенного формулой на языке T) T доказывает P(0), P(1), P(2) и так далее (то есть для каждого стандартного натурального числа n, T доказывает истинность P(n)), но T также доказывает, что существует натуральное число n, для которого P(n) ложно. Теория T называется ω-совместимой, если она не является ω-несовместимой. Существует более слабое, но тесно связанное свойство – Σ1-корректность. Теория T называется Σ1-корректной (или 1-совместимой, в другой терминологии), если каждое Σ01-предложение, доказуемое в T, истинно в стандартной модели арифметики N (то есть в структуре обычных натуральных чисел с операциями сложения и умножения). Если T достаточно сильна для формализации разумной модели вычислений, то Σ1-корректность эквивалентна требованию, что всякий раз, когда T доказывает остановку машины Тьюринга C, машина C действительно останавливается. Каждая ω-совместимая теория является Σ1-корректной, но не наоборот. В более общем случае можно определить аналогичное понятие для более высоких уровней арифметической иерархии. Если Γ – это множество арифметических предложений (обычно Σ0n для некоторого n), то теория T называется Γ-корректной, если каждое Γ-предложение, доказуемое в T, истинно в стандартной модели. Когда Γ – множество всех арифметических формул, Γ-корректность называется просто (арифметической) корректностью. Если язык T состоит только из языка арифметики (в отличие, например, от теории множеств), то корректная система – это система, модель которой можно рассматривать как множество ω, обычное множество математических натуральных чисел. Случай с общей теорией T отличается, см. логику ω ниже. Σn-корректность имеет следующую вычислительную интерпретацию: если теория доказывает остановку программы C, использующей оракул Σn−1, то программа C действительно останавливается.

Согласованные, ω-несогласованные теории

Напишите PA для теории арифметики Пеано, а Con(PA) — для утверждения арифметики, формализующего утверждение "PA является непротиворечивой". Con(PA) может иметь вид "Не существует натурального числа n, являющегося числом Гёделя доказательства в PA равенства 0=1". Теперь, непротиворечивость PA влечет за собой непротиворечивость PA + ¬Con(PA). Действительно, если бы PA + ¬Con(PA) была противоречивой, то сама PA доказала бы ¬Con(PA) → 0=1, а доказательство от противного в PA привело бы к доказательству Con(PA). Согласно второй теореме о неполноте Гёделя, PA была бы противоречивой. Следовательно, предполагая, что PA непротиворечива, PA + ¬Con(PA) также непротиворечива. Однако, она не была бы ω-согласованной. Это связано с тем, что для любого конкретного n, PA, и, следовательно, PA + ¬Con(PA), доказывает, что n не является числом Гёделя доказательства равенства 0=1. Однако, PA + ¬Con(PA) доказывает, что существует натуральное число n, являющееся числом Гёделя такого доказательства (это просто прямое перефразирование утверждения ¬Con(PA)). В этом примере аксиома ¬Con(PA) имеет класс Σ1, следовательно, система PA + ¬Con(PA) на самом деле является Σ1-некорректной, а не просто ω-несогласованной.

Арифметически неточные, ω-последовательные теории

Пусть ωCon(PA) — арифметическое предложение, формализующее утверждение "PA является ω-согласованной". Тогда теория PA + ¬ωCon(PA) является необоснованной (в точности, Σ3-необоснованной), но ω-согласованной. Доказательство аналогично первому примеру: для "предиката доказуемости" ωProv(A) = ¬ωCon(PA + ¬A) выполняется подходящая версия условий доказуемости Гильберта — Бернайса — Лёба, следовательно, она удовлетворяет аналогу второй теоремы о неполноте Гёделя.