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

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

Определение

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

A 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 другой, см. ω-логику ниже.

Σ _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 ). $\exists x\,c = x$

Σ ₁ -здравые ω-несогласованные теории, использующие только язык арифметики, могут быть построены следующим образом. Пусть 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 доказывает формулу , поскольку она логически эквивалентна аксиоме ¬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 ) справедлива подходящая версия условий выводимости Гильберта – Бернейса – Лёба , следовательно, он удовлетворяет аналог второй теоремы Гёделя о неполноте.

ω-логика

Концепция теорий арифметики, целые числа которых являются истинными математическими целыми числами, отражена в ω-логике . ^[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 является ω-непротиворечивым тогда и только тогда, когда непротиворечиво.

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

Здесь – множество всех Π ⁰₂ -предложений, действительных в стандартной модели арифметики, – принцип равномерного отражения для 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 Quine (1971), Теория множеств и ее логика .
^ ab SC Клини, Введение в метаматематику (1971), стр.207. Bibliotheca Mathematica: Серия монографий по чистой и прикладной математике Vol. Я, Вольтерс-Нордхофф, Северная Голландия 0-7204-2103-9, Эльзевир 0-444-10088-1.
^ Сморинский, «Теоремы о неполноте», Справочник по математической логике , 1977, с. 851.
^ Флойд, Патнэм, Примечание к «печально известному абзацу» Витгенштейна о теореме Гёделя (2000)
^ Х. Фридман, «Приключения в незавершенности Гёделя» (2023), стр.14. По состоянию на 12 сентября 2023 г.
^ Определение этого символизма можно найти в арифметической иерархии .
^ В этой формулировке вместо прямого противоречия используется 0=1; это дает тот же результат, потому что PA определенно доказывает ¬0=1, поэтому, если бы он также доказал 0=1, мы получили бы противоречие, а с другой стороны, если PA доказывает противоречие, то он доказывает что угодно , включая 0= 1.
^ Дж. Барвайз (редактор), Справочник по математической логике , Северная Голландия, Амстердам, 1977.
^ Смориньски, Крейг (1985). Самореференция и модальная логика. Берлин: Шпрингер. ISBN 978-0-387-96209-2.Рассмотрено в Булосе, Г.; Сморинский, К. (1988). «Самореференция и модальная логика». Журнал символической логики . 53 :306. дои :10.2307/2274450. JSTOR 2274450.

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

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