Относительная согласованность PA и некоторые теории типов

Для теории типов под последовательностью я подразумеваю, что у нее есть тип, который не заселен. Из сильной нормализации лямбда-куба следует, что система $F$ и система $F_\omega$ согласованы. MLTT + индуктивные типы также имеют доказательство нормализации. Однако все они должны быть достаточно мощными, чтобы построить модель PA, которая доказывает, что PA согласуется с этими теориями. Система $F$ является достаточно мощным , поэтому я ожидаю , что это будет в состоянии доказать непротиворечивость PA путем построения модели с использованием Чёрча. MLTT + IT имеет индуктивный тип с натуральными числами и должен также обеспечивать последовательность.

Все это подразумевает, что доказательства нормализации для этих теорий не могут быть усвоены в PA. Так:

1. Могут ли система , система F ω и MLTT + IT на самом деле доказать согласованность PA?$F$$F_\omega$
2. Если они могут, то какая метатеория необходима для доказательства нормализации для систем , F ω и MLTT + IT?$F$$F_\omega$
3. Есть ли хороший справочник для теории доказательств теорий типов в целом или для некоторых из этих теорий типов в частности?

Краткий ответ на ваш вопрос 1 - нет , но, возможно, по незаметным причинам.

Прежде всего, система и F ω не может выразить теорию первого порядка арифметики , и даже меньше , консистенция P A .$F$$F_\omega$ $\mathrm{PA}$

Во-вторых, и это действительно удивительно, действительно может доказать согласованность обеих этих систем! Это делается с использованием так называемой не относящейся к доказательству модели , которая интерпретирует типы как множества ∈ { ∅ , { ∙ } } , где ∙ - некоторый фиктивный элемент, представляющий обитателя непустого типа. Тогда можно записать простые правила эксплуатации → и ∀ на таких типах довольно легко получить модель для системы F , в которой тип ∀ X . X интерпретируется как $\mathrm{PA}$$\in\{\varnothing,\{\bullet\}\}$$\bullet$$\rightarrow$$\forall$$F$$\forall X.X$$\varnothing$, Можно сделать то же самое для , немного более осторожно интерпретируя более высокие виды как пространства конечных функций.$F_\omega$

Здесь есть очевидный парадокс, когда может доказать согласованность этих, казалось бы, мощных систем, но не (как я сейчас покажу) нормализацию.$\mathrm{PA}$

Недостающий ингредиент здесь - реализуемость . Реализуемость - это способ заставить определенные программы соответствовать определенным предложениям, обычно в арифметике. Я не буду вдаваться в подробности, но если программа реализует предложение ϕ , записанное как p ⊩ ϕ , то у нас есть определенное доказательство для ϕ , в частности, если p нормализует, то p ⊮ ⊥ . У нас есть:$p$$\phi$$p\Vdash \phi$$\phi$$p$$p\not\Vdash\bot$

Теорема: если - теорема арифметики 2- го порядка P A 2 , то существует некоторый замкнутый член t системы F, такой что t ⊩ $\phi$$\mathrm{PA}_2$$t$$F$

$$t\Vdash\phi$$

Эта теорема может быть доказана в , и поэтому P A ⊢ F  нормализует ⇒ P A 2  непротиворечив и аргумент Геделя применим (и P A не может доказать нормализацию системы F ). Полезно отметить , что обратная импликация, так что мы имеем точную характеристику доказательства теоретико-мощность , необходимая для доказательства нормализации системы F .$\mathrm{PA}$

$$\mathrm{PA}\vdash F\mbox{ is normalizing}\Rightarrow\mbox{$\mathrm{PA}_2$ is consistent}$$ $\mathrm{PA}$$F$$F$

Аналогичная история существует для системы , которая, как мне кажется, соответствует более высокой арифметике P A ω .$F_\omega$$\mathrm{PA}_\omega$

---

Наконец, у нас есть сложный случай MLTT с индуктивными типами. Здесь снова возникает несколько тонкая проблема. Конечно, здесь мы можем выразить непротиворечивость , так что это не проблема, и нет никакой не относящейся к доказательству модели, поскольку мы можем доказать, что тип N a t имеет по крайней мере 2 элемента (бесконечное количество различных элементов , на самом деле).$\mathrm{PA}$$\mathrm{Nat}$

Однако мы сталкиваемся с удивительным фактом интуиционистских теорий высшего порядка: , версия Гейтинга арифметики высшего порядка консервативна над H $\mathrm{HA}_\omega$$\mathrm{HA}$ ! В частности, мы не можем доказать согласованность (что эквивалентно согласованности H A ). Интуитивная причина этого заключается в том, что интуитивистские функциональные пространства не позволяют количественно определять произвольное подмножество N , поскольку все определяемые функции N → N должны быть вычислимыми.$\mathrm{PA}$$\mathrm{HA}$$\mathbb{N}$$\mathbb{N}\rightarrow \mathbb{N}$

В частности, я не думаю, что вы можете доказать непротиворечивость если добавляете в MLTT только натуральные числа без юниверсов. Я верю, что добавление вселенных или «более сильных» индуктивных типов (например, порядковых типов) даст вам достаточно силы, но, боюсь, у меня нет ссылок на это. С вселенными, аргумент кажется довольно простым , хотя, так как у вас есть достаточно теории множеств построить модель Н А .$\mathrm{PA}$$\mathrm{HA}$

---

Наконец, ссылки на теорию доказательств систем типов: здесь, на мой взгляд, действительно есть пробел в литературе, и я бы с удовольствием отнесся ко всем этим предметам (на самом деле, я мечтаю написать это сам когда-нибудь!). В это время:

• Не относящаяся к доказательству модель объясняется здесь Микелом и Вернером, хотя они делают это для исчисления конструкций, что несколько усложняет ситуацию.

• Аргумент реализуемости изложен в классических Доказательствах и Типах Жирара, Тейлора и Лафона. Я думаю, что они также рисуют не относящуюся к доказательству модель и много полезных вещей помимо этого. Вероятно, это первая ссылка для чтения.

• Аргумент консервативности гейтинговой арифметики высшего порядка можно найти в неуловимом втором томе « Конструктивизма в математике » Троельстры и ван Далена (см. Здесь ). Оба тома чрезвычайно информативны, но довольно сложны для чтения новичку, ИМХО. Это также несколько избегает «современных» предметов теории типов, что неудивительно, учитывая возраст книг.

---

Дополнительный вопрос в комментариях был о точной силе согласованности / силе нормализации MLTT + Индуктивы. У меня нет точного ответа здесь, но, конечно, ответ зависит от количества вселенных и природы разрешенных индуктивных семейств. Ратхен исследует этот вопрос в превосходной статье «Сила некоторых теорий типа Мартина-Лофа» .

$\cal{T}$$\cal{U}$

$$\mathrm{PA}\vdash\mathrm{Con}(\cal{T})\Rightarrow\mathrm{Con}(\cal{U})$$

тогда вообще

$$\mathrm{PA}\vdash \mbox{1-$\mathrm{Con}$}(\cal{T})\Rightarrow\mathrm{Norm}(\cal{U})$$

$\mathrm{Con}$$\mathrm{Norm}$

$\mathrm{HA}_\omega$

Что касается MLTT с индукцией-рекурсией или индукцией-индукцией, я не знаю, какова ситуация, и AFAIK, проблема точной прочности согласованности все еще остается открытой.