ω-непротиворечивая теория

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

Определение [ править ]

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

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

T является ω-согласованным, если не ω-несовместным.

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

В более общем плане мы можем определить аналогичную концепцию для более высоких уровней арифметической иерархии . Если Γ - это набор арифметических предложений (обычно Σ ⁰_n для некоторого n ), теория T является Γ-здравой, если каждое Γ-предложение, доказуемое в T , истинно в стандартной модели. Когда Γ - это множество всех арифметических формул, Γ-правильность называется просто (арифметической) надежностью. Если язык T состоит только из языка арифметики (в отличие, например, от теории множеств), то звуковая система - это система, модель которой можно представить как набор ω, обычный набор математических натуральных чисел. Случай общего T иной, см. Ω-логику ниже.

Σ _п -soundness имеет следующую вычислительную интерпретацию: если теория доказывает , что программа С помощью Е _{п -1} - оракул привалов, тогда C фактически останавливается.

Примеры [ править ]

Последовательные, ω-несовместимые теории [ править ]

Напишите PA для теории арифметики Пеано и Con (PA) для утверждения арифметики, которое формализует утверждение «PA непротиворечиво». Con (PA) может иметь вид «Для любого натурального числа n , n не является числом Гёделя доказательства из PA, что 0 = 1». (В этой формулировке 0 = 1 вместо прямого противоречия; это дает тот же результат, потому что PA определенно доказывает ¬0 = 1, поэтому, если бы он доказал, что 0 = 1, мы получили бы противоречие, и, с другой стороны, если бы PA доказывает противоречие, затем доказывает все , в том числе 0 = 1.)

Теперь, если предположить, что PA действительно непротиворечиво, отсюда следует, что PA + ¬Con (PA) также непротиворечиво, поскольку если бы это было не так, PA доказал бы Con (PA) ( reductio ), что противоречит второй теореме Гёделя о неполноте . Однако PA + ¬Con (PA) не является ω-согласованным. Это потому, что для любого конкретного натурального числа n PA + ¬Con (PA) доказывает, что n не является гёделевским числом доказательства того, что 0 = 1 (PA сам доказывает этот факт; дополнительное предположение ¬Con (PA) не является нужный). Тем не менее, PA + ¬Con (PA) доказывает , что для некоторого натурального числа п , п является число Геделя такого доказательства (это просто прямая переформулировкой претензии ¬Con (PA)).

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

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

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

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

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

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

{\ displaystyle \ 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 ). С другой стороны, Т доказывает формулу , потому что это логически эквивалентно аксиоме ¬ A . Следовательно, T ω-несовместна. $\exists x\,\neg P(x)$

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

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

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

ω-логика [ править ]

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

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

Из вывода .

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 является рекурсивно аксиоматизируем , ω-непротиворечивость имеет следующую характеристику, в связи с Крейгом Smoryński : ^[5]

T является ω-согласованным тогда и только тогда, когда согласовано.

T+\mathrm {RFN} _{T}+\mathrm {Th} _{\Pi _{2}^{0}}(\mathbb {N} )

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

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

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

Заметки [ править ]

^ WVO Куайн (1971), Теория множеств и ее логика .
^ Сморински, "Теоремы о неполноте", Справочник по математической логике , 1977, с. 851.
^ Определение этого символизма можно найти в арифметической иерархии .
^ Дж. Барвайз (редактор), Справочник по математической логике , Северная Голландия, Амстердам, 1977.
^ Smoryński, Крэйг (1985). Самостоятельная ссылка и модальная логика . Берлин: Springer. ISBN 978-0-387-96209-2.Рецензия на Boolos, G .; Сморинский, К. (1988). «Саморефлексия и модальная логика». Журнал символической логики . 53 : 306. DOI : 10,2307 / 2274450 . JSTOR 2274450 .

Библиография [ править ]

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

[quine-1] WVO Куайн (1971), Теория множеств и ее логика .

[2] Сморински, "Теоремы о неполноте", Справочник по математической логике , 1977, с. 851.

[3] Определение этого символизма можно найти в арифметической иерархии .

[4] Дж. Барвайз (редактор), Справочник по математической логике , Северная Голландия, Амстердам, 1977.

[5] Smoryński, Крэйг (1985). Самостоятельная ссылка и модальная логика . Берлин: Springer. ISBN 978-0-387-96209-2.Рецензия на Boolos, G .; Сморинский, К. (1988). «Саморефлексия и модальная логика». Журнал символической логики . 53 : 306. DOI : 10,2307 / 2274450 . JSTOR 2274450 .

[1]