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

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

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

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

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

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

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

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

Запишите PA для теории арифметики Пеано и Con(PA) для утверждения арифметики, которое формализует утверждение «PA является непротиворечивым». Con(PA) может иметь вид «Никакое натуральное число n не является гёделевым номером доказательства в PA, что 0=1». ^[7] Теперь, непротиворечивость 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 ), но ω-непоследователен (как это доказывается , и c  ≠  n для каждого числа n ).${\displaystyle \существует x\,c=x}$

Σ ₁ -звуковые ω-несогласованные теории, использующие только язык арифметики, могут быть построены следующим образом. Пусть I Σ _n будет подтеорией PA с индукционной схемой, ограниченной Σ _n -формулами, для любого n  > 0. Теория I Σ _{n  + 1} конечно аксиоматизируема, пусть, таким образом , A будет ее единственной аксиомой, и рассмотрим теорию T  =  I Σ _n  + ¬ A . Мы можем предположить, что 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 ). С другой стороны, T доказывает формулу , потому что она логически эквивалентна аксиоме ¬ A . Следовательно, T является ω-несовместимой.${\displaystyle \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 ), следовательно, он удовлетворяет аналогу второй теоремы Гёделя о неполноте.

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

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

Из этого следует вывод .${\displaystyle P(0),P(1),P(2),\ldots }$${\displaystyle \forall x\,(N(x)\to P(x))}$

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

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

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

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

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

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

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

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

• Курт Гёдель (1931). «Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I». В Monatshefte für Mathematik . Переведено на английский язык как « О формально неразрешимых утверждениях Principia Mathematica и родственных системах» .