ω-согласованная теория

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

Определение

теория T Говорят, что интерпретирует язык арифметики , если существует перевод арифметических формул на язык T так, что T способен доказать основные аксиомы натуральных чисел при этом переводе.

A T , который интерпретирует арифметику, является ω-несовместимым, если для некоторого свойства P натуральных чисел (определенного формулой на языке T ), T доказывает P (0), P (1), P (2) и т. д. (т.е. для каждого стандартного натурального числа n ) T доказывает, что P ( n выполняется), но T также доказывает, что существует некоторое натуральное число n такое, что P ( n ) не выполняется . Это не может вызвать противоречия внутри T, потому что T не сможет доказать для любого конкретного значения n , что P ( n ) неверен, а только то, что существует такое n . В частности, такое n обязательно является нестандартным целым числом в любой модели для T (поэтому Куайн назвал такие теории «численно инсегрегативными»).

T является ω-непротиворечивым, если оно не ω-непротиворечиво.

Существует более слабое, но тесно связанное с ним свойство Σ ₁ -надежности. Теория T является Σ ₁ -здравой (или 1-непротиворечивой , в другой терминологии). если каждое Σ ⁰ ₁ -предложение доказуемое в T верно в стандартной модели арифметики N (т. е. в структуре обычных натуральных чисел со сложением и умножением). Если T достаточно силен, чтобы формализовать разумную модель вычислений , Σ ₁ -корректность эквивалентна требованию, чтобы всякий раз, когда T доказывает, что машина Тьюринга C останавливается, тогда C действительно останавливается. Любая ω-непротиворечивая теория является Σ ₁ -корректной, но не наоборот.

В более общем смысле мы можем определить аналогичную концепцию для более высоких уровней арифметической иерархии . Если Γ — набор арифметических предложений (обычно Σ ⁰ _n для некоторого n ), теория 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 n доказательства (это просто прямая формулировка утверждения ¬Con(PA)).

В этом примере аксиома ¬Con(PA) равна Σ ₁ , следовательно, система PA + ¬Con(PA) на самом деле Σ ₁ -ненадежна, а не просто ω-несовместима.

обоснованные ω-

Пусть T будет PA вместе с аксиомами c ≠ n для каждого натурального числа n , где c — новая константа, добавленная в язык. Тогда T арифметически корректна (поскольку любая нестандартная модель PA может быть расширена до модели T ), но ω-несовместима (как это доказывает $\exists x\,c=x$и c ≠ n для каждого числа n ).

Σ ₁ -здравые ω-несогласованные теории, использующие только язык арифметики, могут быть построены следующим образом. Пусть I Σ _n — подтеория PA с индукционной схемой, ограниченной Σ _n -формулами, для любого n > 0. Теория I Σ _{n + 1} конечно аксиоматизируема, пусть, таким образом, A — ее единственная аксиома, и рассмотрим теорию T знак равно я Σ _п + ¬ А . Можно считать, что A является экземпляром индукционной схемы, имеющей вид

$\forall w\,[B(0,w)\land \forall x\,(B(x,w)\to B(x+1,w))\to \forall x\,B(x,w)].$

Если обозначить формулу

$\forall w\,[B(0,w)\land \forall x\,(B(x,w)\to B(x+1,w))\to B(n,w)]$

на P ( n ), то для каждого натурального числа n теория T (фактически даже чистое исчисление предикатов) доказывает P ( n ). С другой стороны, T доказывает формулу $\exists x\,\neg P(x)$, поскольку это логически эквивалентно аксиоме ¬ A . Следовательно, T ω-несовместимо.

Можно показать, что T является Π _{n + 3} -звуковым. Фактически, она Π _{n + 3} - консервативна по отношению к (очевидно обоснованной) теории I Σ _n . Рассуждение более сложное (оно опирается на доказуемость принципа Σ _{n + 2} - отражения для I Σ _n в I Σ _{n + 1} ).

необоснованные ω-

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

ω-логика

Не путать с Ω-логикой .

Концепция теорий арифметики, целые числа которых являются истинными математическими целыми числами, отражена в ω-логике . Пусть T — теория на счетном языке, включающая унарный символ-предикат N , предназначенный для хранения только натуральных чисел, а также заданные имена 0, 1, 2, ..., по одному для каждого (стандартного) натурального числа (которое могут быть отдельными константами или постоянными терминами, такими как 0, 1, 1+1, 1+1+1, ... и т. д.). Обратите внимание, что сам T может относиться к более общим объектам, таким как действительные числа или множества; таким образом, в модели T объекты, удовлетворяющие N ( x ), - это те, которые T интерпретирует как натуральные числа, не все из которых обязательно должны быть названы одним из указанных имен.

систему ω-логики входят все аксиомы и правила обычной логики предикатов первого порядка, а также для каждой T -формулы P ( x ) с заданной свободной переменной x бесконечное В ω-правило вида:

От $P(0),P(1),P(2),\ldots$ сделать вывод $\forall x\,(N(x)\to P(x))$.

То есть, если теория утверждает (т. е. доказывает) P ( n ) отдельно для каждого натурального числа n , заданного его указанным именем, то она также утверждает P коллективно для всех натуральных чисел одновременно через очевидный конечный универсально квантифицированный аналог бесконечного числа предшественники правила. Для теории арифметики, то есть теории с предполагаемой областью применения натуральных чисел, такой как арифметика Пеано , предикат N является избыточным и может быть опущен в языке, при этом следствие правила для каждого P упрощается до $\forall x\,P(x)$.

ω-модель T - это модель T , область определения которой включает натуральные числа и чьи указанные имена и символ N стандартно интерпретируются соответственно как эти числа и предикат, имеющий в качестве области определения только эти числа (отсюда нет нестандартных чисел). . Если N отсутствует в языке, то то, что было бы областью применения N , должно быть областью применения модели, т. е. модель содержит только натуральные числа. (Другие модели T область определения N могут интерпретировать эти символы нестандартно; например, даже не обязательно должна быть счетной.) Эти требования делают ω-правило обоснованным в каждой ω-модели. Как следствие теоремы об исключении типов , справедливо и обратное: теория T имеет ω-модель тогда и только тогда, когда она непротиворечива в ω-логике.

Существует тесная связь ω-логики с ω-непротиворечивостью. Теория, непротиворечивая в ω-логике, также является ω-непротиворечивой (и арифметически корректной). Обратное неверно, поскольку непротиворечивость в ω-логике — гораздо более сильное понятие, чем ω-непротиворечивость. Однако справедлива следующая характеристика: теория является ω-непротиворечивой тогда и только тогда, когда ее замыкание при невложенных применениях ω-правила непротиворечиво.

принципами

Если теория T , рекурсивно аксиоматизируема ω-согласованность имеет следующую характеристику, предложенную Крейгом Смориньским :

T является ω-непротиворечивым тогда и только тогда, когда $T+\mathrm {RFN} _{T}+\mathrm {Th} _{\Pi _{2}^{0}}(\mathbb {N} )$ согласуется.

Здесь, $\mathrm {Th} _{\Pi _{2}^{0}}(\mathbb {N} )$ — множество всех Π ⁰ ₂ – предложения, действительные в стандартной модели арифметики, и $\mathrm {RFN} _{T}$ — принцип равномерного отражения для T , состоящий из аксиом

$\forall x\,(\mathrm {Prov} _{T}(\ulcorner \varphi ({\dot {x}})\urcorner )\to \varphi (x))$

для каждой формулы $\varphi$с одной свободной переменной. В частности, конечно аксиоматизируемая теория T на языке арифметики является ω-непротиворечивой тогда и только тогда, когда T + PA $\Sigma _{2}^{0}$-звук.

Библиография

• Курт Гёдель (1931). «О формально неразрешимых теоремах Principia Mathematica и родственных им систем I». В ежемесячных журналах по математике . Переведено на английский язык как « О формально неразрешимых утверждениях Principia Mathematica и родственных системах» .