Непротиворечивые NF-подобласти

По теореме Граббе [6], NFI доказуемо непротиворечива в арифметике третьего порядка. Подробные
сведения о (различных) доказательствах согласованности для NFI можно найти в [6] и [14].
Основная идея [6]: 133-135 заключается в использовании сводимости NFI к его фрагменту NFI

4

;

затем NFI

4

интерпретируется в соответствующую теорию типов до уровня 4, TI

4

, плюс Amb

(=так называемая схема типичной неоднозначности, см. [22]).

14

Эти шаги являются finitary и

адаптируем известные теоремы Гришина и Спекера. ТИ

4

+Amb показано непротиворечивым
с помощью Hauptsatz для логики второго порядка (которая эквивалентна в примитивной
рекурсивной арифметике 1-последовательности полной арифметики второго порядка, например, см. [11]:
280). Следовательно:

Теорема 7. NFI является непротиворечивым (в примитивной рекурсивной арифметике плюс 1 -согласованность

арифметики второго порядка).

Для того чтобы выполнить Крипке-подобную конструкцию в NF-системах и представить
синтаксис, мы будем по существу использовать однородную операцию спаривания Куайна, которая
требует экстенсиональности и существования копии натуральных чисел. Но нетрудно
проверить, что сопряжение Куайна действительно хорошо определено уже в NFI.

Это требует двух шагов. Прежде всего, коллекция Фрегеанских натуральных чисел является

набор в NFI. Определять:

∅ = {x / x = x};

V = {x / x = x};

0

= {∅};

a + 1 = {x ∪ {y} | x ∈ a ∧ y /

∈ икс};

Cl

Н

(y) ⇔ 0 ∈ y ∧ ∀ x(x → y → (x + 1)∈ y);

N = {x / ∀y (Cl

Н

(y) → x ∈ y)}.

Тогда NFI предоставляет существование

N; на самом деле, при рассмотрении, все вышеперечисленные наборы выше
являются слабо предикативными. Кроме того, мы имеем, доказуемо в NFI:

Лемма 8 (NFI).

Cl

Н

({x | ϕ (x)}) → N {{x | ϕ (x)};

(2)

(∀х)(х ∈ П ↔ Х = 0 ∨ (∃у ∈ Н)(Х = Y + 1));

(3)

∅ /

∈ N ∧ (∀x ∈ N) (V /

∈ икс);

(4)

(∀x ∈ N)(x + 1 = 0);

(5)

(∀x ∈ N) (∀y ∈ N) (x + 1 = y + 1 → x = y).

(6)

(В (2)

{x | ϕ (x)} должен быть слабо предикативным.)

14

В ТИ

4

,

{икс

я

| ϕ} существует, если i = 0, 1, 2 и ϕ содержит свободные или связанные переменные типа i + 1 не более.

276

А. Кантини

Ясно

N бесконечно по (4) выше.

15

Что касается доказательства, то (4) выполняется в объединении NFI+, так как

НФИ+Союз

≡ NF, и NF доказывает (4) согласно известному результату Спеккера [21].

С другой стороны, NFI +

Объединение подразумевает (4), по [6]. Утверждения (3), (2) с
аксиомами Пеано доказуемы в NFI(6) требует второй части (4)).

Определение 5 (однородное спаривание; [19]).

φ(a) = {y | y ∈ a ∧ y /

∈ N } {{y + 1|y ∈ a ∧ y ∈ N };

θ

1

(a) = {φ (x) / x ∈ a};

θ

2

(a) = {φ (x) ∪ {0} / x ∈ a};

(a, b) = θ

1

а) ∪ θ

2

(b);

Q

1

(a) = {z / φ (z) ∈ a};

Q

2

(a) = {z | φ(z) ∪ {0} ∈ a}.

Приведенные выше определения являются (самое большее) слабо предикативными, и поэтому Вселенная
множеств замкнута при соответствующих операциях, доказуемых в NFI.

Лемма 9 (NFI).

1.

φ (a) = φ(b) → a = b;

2. 0

/

∈ φ(a);

3.

θ

я

а) = θ

я

(b) → a = b, где i = 1, 2;

4.

Q

я

((икс

1

, икс

2

)) = икс

я

, где

i = 1, 2;

5.

(x, y) = (u, v) → x = u ∧ y = v;

6. the map

x, y − → (x, y) сюръективно и ⊆ -монотонно в каждой переменной.

Доказательство зависит от свойств:

N и последующая операция [19]. В

в частности, мы ниже используем тот факт, что операция сопряжения Куайна является

⊆- монотонно в

оба аргумента. Это видно на примере инспекции: определение понятия

(a, b) является положительным в a,

б.

16

Лемма 10 (неподвижная точка). Пусть...

A (x, a) - формула, которая является положительной в a. Предполагать

тот

Один

(a) = {x | A (x, a)}

является слабо предикативным, где

x, a даны типы i, i +1 соответственно. Тогда NFI доказывает

существование множества

c типа i + 1, такие что:

15

Действительно, если

∅ /

∈ N, то никакое натуральное число а-ля Фреге-Рассел не сводится к пустому множеству, т. е. E., существуют

произвольные большие конечные множества.

16

Напомним, что формула

A (x, a) положительно в a, если каждое свободное вхождение a в отрицание нормально

форма из

А находится в атомах вида t ∈ a, которые имеют префикс четного числа отрицаний и

где

один /

∈ F V (t).

О Расселовском парадоксе о Пропозициях и истине

277

•

Один

c) ⊆ c;

•

Один

(a) ⊆ A ⇒ c ⊆ A.

Доказательство является стандартным: обратите внимание, что набор

c: = {x / ∀d(

Один

d) ⊆ d → x ∈ d)}

является слабо предикативным.

17

Определение 6. NFI (pair) (NFP(pair), NF (pair)) - это теория, которая расширяет NFI (NFP,
NF соответственно) с новым символом двоичной функции

(−,−) для упорядоченного спаривания и

соответствующая новая аксиома:

∀x∀y∀u v v ((x, y) = (u, v) → x = u ∧ y = v)

Понятно, что условие стратификации поднимается до нового языка,
оговаривая, что

t, s в (t, s) получают один и тот же тип.

Стратегическая роль однородного спаривания уточняется двумя результатами эквивалентности.

Ниже пусть

С

1

≡ С

2

обозначим отношение, которое имеет место между двумя формальными теориями

С

1

,

С

2

всякий раз, когда они взаимно интерпретируемы.

Предложение 6. НФ

≡ СФ

3

(пара).

Доказательство этого утверждения было независимо предложено Антонелли и Холмсом.

Основное наблюдение состоит в том, что NFP

3

(пара) доказывает существование множества

E, где

E: = ∃y(y = E) и E = {{{x}, y} | x ∈ y}. Но по Гришину [13], NF ≡ NF

3

+ Ми.

Мы можем легко распространить это предложение на подсистемы NFI, NFP.

Предложение 7. NFP

≡ ПОРОШКООБРАЗНЫЙ ПЕНОГАСИТЕЛЬ

3

(пара) и NFI

≡ NFI

3

(пара).

Доказательство. Пусть...

⇔ ∃ y (y = {u / | u=∅}).

По теореме Гришина и [6], NFI

≡ NFI

3

+, (соответственно NFP ≡ NFP

3

+).

Но NFP

3

(пара) доказывает, что

M = {({x}, y) | x ∈ y} - множество и

∀х∃на∀Х(Х ∈ а ↔ ∃Q(Кью ∈ Х ∧ (∀З ∈ х)((Д, з) ∈ м))).

(7)

Выбирать

s = {{x} | x ∈ V } в (7); тогда NFP

3

(пара) доказывает, что существует множество

Я такой что

(∀x) (x ∈ I x x=∅).

Из этого следует, что мы можем свободно использовать однородную операцию сопряжения, когда мы работаем

в NF и NFI.

17

Аналогичный аргумент показывает, что NFI обосновывает существование наибольшей неподвижной точки из

Один

.

278

А. Кантини