Является ли ZF Финитно приводимым?

Karl-Georg Niebergall

Абстрактный. Из работы, выполненной J. Mycielski, следует, что каждая непротиворечивая теория r. e. первого порядка

T является доказательством-теоретически сводимым к локально конечной теории T. Я представляю другой метод
для получения того же результата. Следствием этих результатов является следующее: Если каждая локально конечная теория
является финитной, то ZF финитно сводима. Поскольку посылка “каждая локально конечная теория является
финитной " может быть принята некоторыми теоретиками доказательства, у нас есть проблема, что ZF окажется
финитно приводимой.

Введение

Я думаю, что ответом на вопрос, поставленный в названии этого текста, должно быть “нет”.
Поскольку выражение "финитно “повторяет слово” конечный" из обыденного языка,
это должно быть интуитивно очевидно. Даже не имея точных определений этого понятия. “

T is

конечностно приводимые” и “

S-это финитная теория”

1

под рукой—

S является конечным ⇐⇒ S не делает предположений о бесконечности

с этой точки зрения все выглядит вполне правдоподобно. Предположения о бесконечности сделаны
ZF, однако, до такой высокой степени, что это, кроме того, расширило бы наше понимание
“приводимого”, если бы ZF был объявлен финитно приводимым. Обнадеживает то, что
в исследованиях, относящихся к теории доказательств, можно найти то же самое суждение: “
например (чтобы снова быть крайним), система ZF, которая оправдывается бесчисленными
бесконечными рамками Канторианской теории множеств, не сводится ни к какой окончательно оправданной
системе.” ([6]: 7).

В то же время J. Mycielski (в [29] и [30]) утверждает, что ZF синтаксически
изоморфен локально конечной теории FIN(ZF), которая, по словам Mycielski, “устраняет
идеальные (бесконечные) объекты из доказательств свойств конкретных (конечных) объектов”.

2

И
S. Лавин, предлагая подход к основам математики (см. [24] и

1

Я использую “

S-это финитная теория” и” S-это финитная теория " как синонимы.

2

"Цель настоящей статьи состоит в том, чтобы построить единообразным образом для любой непротиворечивой теории

T A локально

конечная теория FIN(

Т) который синтаксически (в некотором смысле) изоморфен т.” ([30]: 59). И он добавляет “ " с
физикалистской точки зрения теоремы ZF и их FIN(ZF)-аналоги могут иметь одно и то же значение.
Поэтому FIN (ZF) [...] исключает идеальные (бесконечные) объекты из доказательств свойств конкретных (конечных)
объектов.” ([30]: 59).

154

К.-Г. Niebergall

[25]), который имеет некоторые сходства с Микельским, добавляет, что FIN(ZF) является аналогом
ZF, который принадлежит к тому, что он называет “конечной математикой” и даже не предполагает
потенциального бесконечного.

3

Конечно же, формулировка теоретика доказательства “

T конечностно приводимо” не является

так же, как и у Микельского " есть локально конечная теория, которая изоморфна

Т ”

или как у лавина “каждая теорема из

T имеет аналог в конечной математике". Таким образом
, утверждения последних прямо не противоречат оценке того, что ZF не может быть
финитно сводимым. Однако, finitistic и локально конечных теорий и тех, кто принадлежит к
конечной математики, с одной стороны, и отношения, доказательства теоретико-сводимость
и быть изоморфно С (или: будучи аналогом) с другой стороны, повернуть
вне для того чтобы быть настолько тесно связаны, что исследования Mycielski и лавин могут
быть задержаны в область теории доказательств, о результате, что ZF является
также финитно сводимый в смысле теоретика доказательства. Эта теоретико-доказательная
концепция финитной сводимости может дать неверный ответ на вопрос: “Является
ли ZF финитно сводимым?", является темой этого документа.

4

Определена Финитная Сводимость

Во введении я просто использовал фразу "ZF является финитно приводимым", как будто эта фраза
была понята достаточно хорошо, как она есть. “

Однако T является финитно сводимым " требует
экспликации. Для ответа на этот вопрос целесообразно обратиться к исследованиям
, относящимся к теории доказательств.

5

Доказательство-Теоретическая Сводимость

В [4, 6, 7] мы находим следующее определение, которое, по-видимому, широко принято
теоретиками доказательства:

Определение 1.

S является финитно приводимым: ⇐⇒ существует финитная теория T такая, что
S теоретически доказано сводится к T.

Но что насчет этого? “

S является финитной теорией” и "S является доказательством-теоретически сводимым к T"?
Для второй фразы были сформулированы точные определения; но есть несколько
из них, которые используются в теории доказательств. Прежде чем обсуждать четыре из них (концентрируясь

3

См. ([25]: 389): “каждая теорема обычной математики имеет естественный аналог в конечной математике.

[

...] Конечная математика даже не предполагает никакой формы потенциального бесконечного.”

4

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

вопрос в том, что это не так.

5

На самом деле, обычно приходится обращаться к трудам С. Фефермана. Кроме того, существует не так много
теоретико-доказательных текстов, которые имеют прямое отношение к философским темам. Большинство определений, рассмотренных
в этой статье, в частности, были сформулированы Феферманом.

Является ли ZF Финитно приводимым?

155

по версии из [4, 6, 7]), позвольте мне сначала ввести некоторую терминологию и формальный
фон.

Большинство теорий, рассмотренных в данной работе, будут сформулированы в первом порядке

языки L

ПА

и L

(QF-IA)

или в L

АФР

, свободный от квантора фрагмент L

(QF-IA)

. То

словарный запас L

ПА

содержит “

S”,"+", " · " и "0", в то время как словарь L

АФР

(и L

(QF-IA)

) содержит, для каждой примитивной рекурсивной функции

f, уникальный знак функции
f, т. е. “примитивный рекурсивный знак функции". В каждом из этих языков, есть, для
каждого натурального числа

n, ровно одна цифра n, обозначающая его в N (=

Н

, S,+,·, 0, то

стандартная модель арифметики). PRA-это теория в L

АФР

чьи аксиомы существуют, помимо

классическая логика в L

АФР

, уравнения рекурсии для всех примитивных рекурсивных функций,

“

Sx = 0”, "Sx = Sy - → x = y"; кроме того, предполагается, что пра замкнута относительно

правило индукции (сформулированное с помощью формулl

АФР

). (QF-IA) является теория, что

результаты от PRA через добавление логики первого порядка.

6

Теория - это набор предложений, которые дедуктивно замкнуты. Теория

T investi-

стробируемый здесь будет аксиоматизируемым; т. е. для каждого такого

T, там будет рекурсивное множество

из предложений таких, что

T =

. Для аксиоматизируемых теорий

S, T..., “σ ”, “τ ”... будет

используйте для

0

0

- формулы L

ПА

представляя множества (числа Геделя) аксиом для
T (за исключением PA и(QF-IA), где я буду принимать “pa(x)” и “(qf-ia) (x)”
для этих формул вместо этого).

7

Учитывая представленность

τ из (множества чисел Геделя

о) набор аксиом из:

T, общие арифметизации “доказательства в T", " доказуемые в

T " и "T является последовательным" являются:

Доказательство

τ

(x, y): ← → Seq (x) ∧ y = x

lh(x)

−1

∧ ∀V в < ЛГ(х) (LogAx(х

в

) τ τ (x

в

)∨

∃uw

в

= икс

u

˙

→икс

в

)),

Пиар

τ

(y): Proof → Proof X доказательство

τ

(x, y),

Зубрить

τ

:←→ Пиар

τ

(⊥).

8

Пусть L-язык с рекурсивным набором замкнутых термов и ClT(

u) быть a

0

0

-

формула L

ПА

представляющий “

u-замкнутый член L”; тогда " y-замкнутое уравнение в

L " представлен следующим образом:

0

0

- формула ClEq

(y) из L

ПА

определяется следующим образом:

ClEq

(y): ← → uv uv ≤ y (ClT (u) ∧ ClT (v) ∧ y =

=

, u, v).

6

Для таких теорий, как Q, I

0

+ Exp, I

0

+ Supexp, ACA

0

, ZF и NBG, которые упоминаются только в некоторых

пункты в этой статье и служат простыми примерами, см. [43], [9], [23], [41].

7

Каждое из выражений

t, которые принадлежат L

АФР

, Л

(QF-IA)

или L

ПА

имеет число Геделя

т с Геделем-

числительное

т. Если α-формула k-го места в L

ПА

и

A ⊆ ω

к

, затем “

α-это представление A " определяется как

∀северный

1

,... н

к

∈ ω (n

1

,..., северный

к

∈ A ⇒ ⇒ N / = α(n

1

,..., северный

к

)).

Арифметическую иерархию смотрите в работах [9], [20].

8

"Синтаксические" метаматематические выражения "x есть последовательность", "длина (последовательности) x", " x есть

отрицание y", "x есть условность y и z", " x есть формула L

АФР

"предполагается, что они будут представлены

Автор:

0

0

- формулы L

ПА

—для чего я пишу " Seq

(x)”, “lh(x)", " x =

y", " x = y

→z", "l[pra] (x)" - in

обычный способ (см., например, [9] и [20]; для “точечной нотации” см. Также [3]).

156

К.-Г. Niebergall

Позволь

g-примитивная рекурсивная функция с индексом e; затем

σρ

п

[e]τ

:←→ ∀xy (доказательство

σ

(y, x) Cle ClEq(x) → доказательство

τ

([e] (y), x)).

Определение 2 (см. [4, 6, 7]).

S ρ

Т

T: ⇐ ⇒ S является (неравномерно) доказательством-теоретически

сводится к

T: ⇒ ⇒ существует примитивная рекурсивная функция g с индексом e

9

такие что

(ля)

N |= σρ

п

[e] τ, и

(b)

Т

σρ

п

[e] τ.

Проблема с теоретико-доказательной сводимостью, как это объясняется в определении 2, заключается в ее
отсутствии транзитивности: см. [31] для примера теорий

S, T, U такие, что S ρ

Т

T и

T ρ

U

U, но не S ρ

U

U. Конечно, эта трудность исчезает, если вместо варьирования

теории

T, упомянутый в (b), существует только одна равномерно выбранная теория U, в которой

“

σρ

п

[e]τ ” доказано. Довольно часто PRA принимается за U; я следую этой практике

10

и
определите единый вариант теоретико-доказательной сводимости следующим образом:

Определение 3 (см. [7]).

S ρ

un

T: ⇐ ⇒ S (равномерно) доказательство-теоретически сводимо

Для

T: ⇒ ⇒ существует примитивная рекурсивная функция g с индексом e, такая что

(ля)

N |= σρ

п

[e] τ, и

b) (QF-IA)

σρ

п

[e] τ.

Теоретико-доказательная сводимость также определяется как доказуемая относительная согласованность.
Таким образом, давайте истолкуем следующее Как определения теоретико-доказательной сводимости:

Определение 4.

S равномерно доказуемо последователен относительно T: ⇐ ⇒ (QF-IA)

Зубрить

τ

→ Против

σ

.

Определение 5.

S неравномерно доказуемо последовательно относительно T: ⇒ ⇒

Т

Зубрить

τ

→ Против

σ

.

Когда эти определения сравниваются, каковы их сильные и слабые стороны?

Во-первых, просто доказывающ относительную последовательность

S to T достаточно для многих доказательств-

теоретическое исследование. Но вот отношение между

S и финитная теория T estab-

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

S конечностно приводимый в интуитивно понятном виде

убедительный смысл.

11

Во-вторых, доказуемая относительная последовательность имеет преимущество

будучи применимым к теориям

S, T которые сформулированы в различном, возможно даже dis-

сустав, языки. Если определения 2 и 3 должны иметь смысл, то языки

S и Т

9

Это и есть определение из [7]. Первоначально (в [4]),

g предполагалось, что она является лишь частично рекурсивной.

10

Чтобы быть точным, я использую (QF-IA). Для рассматриваемой цели, разница между PRA, (QF-IA) и I

1

пренебрежимо мал с теоретической точки зрения: для (QF-IA) и I

1

являются консервативными расширениями PRA, и

(QF-IA) и я

1

докажите то же самое

0
2

-предложения. Практически, выбор (QF-IA) предпочтителен потому что свое

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

11

Это суждение может быть слишком поспешным; ср. теорема.

Является ли ZF Финитно приводимым?

157

упомянутые в них должны хотя бы разделять замкнутые уравнения. В-третьих, существует
различие между однородными и неоднородными версиями: в случае последних
должна быть возможность формализовать (возможно, ограниченные версии) “x является доказательством для y в
A” на языке теории T, в которой выполняются доказательства. Таким образом, теория
групп, например, хотя и является подтеорией теории абелевых групп,
вряд ли является неравномерно доказанной-теоретически сводимой к последней.

В общем, единообразные версии, по-видимому, превосходят. Однако мы имеем интересную
и несколько удивительную ситуацию, которая для многих теорий, обычно рассматриваемых
как теоретико-доказательная сводимость, определяемая определениями 2, 3 и 4, составляет то же самое.
Более явно:

Теорема.

12

Пусть L-расширение L

ПА

и пусть...

S, T быть последовательными рекурсивно

перечисляемые теории, сформулированные в L с

0

0

-рецептурный

(in L

ПА

) σ, τ представив

аксиома-наборы из

S, T, такие что Q ⊆ S и I

1

⊆ Т. Затем

S ρ

Т

T, S ρ

un

T и " S равномерно доказуемо последовательны относительно T ”

эквивалентны друг другу.

13

Все еще остается вопрос о том, почему (QF-IA) следует принимать за

U, "Единая
доказательная теория". Конечно, этот выбор допустим: ибо он является целью доказательства того, что
“

σρ

п

[e]τ "в U, чтобы гарантировать, что" σρ

п

[e] τ " действительно имеет место; и для того, чтобы выполнить это

задача,

U должен быть звуковым (для

0
1

- предложения, по крайней мере). Однако последовательность и здравость
ПА, по-видимому, столь же бесспорны, как и (QF-IA). Теперь, (QF-IA)
можно рассматривать как отличающийся в силу того, что он является финитным или финитно сводимым;
но я думаю, что этот взгляд проблематичен (см. ниже). Наконец, почему бы не предпочесть, например,
мне

0

+ Exp к I

1

когда у кого-то есть финитные требования на

- А?

Даже если есть веские концептуальные основания для выбора (QF-IA) для

U трудно
найти, есть еще некоторые, которые говорят за его принятие, которое можно назвать “прагматичным”.
С одной стороны, если ПА принимается за

U вместо (QF-IA), слишком много теорий
стали бы неразличимыми в отношении теоретико-доказательной сводимости. Причина заключается
в том, что ПА доказывает прямую согласованность—откуда и относительная согласованность—“слабых”
теорий, таких как, например, все конечно аксиоматизируемые подпоследовательности ПА. Но полученное
доказательство-теоретическая сводимость, скажем, I

1000

к пропозициональной логике это, конечно, не
относится. С другой стороны, теории, которые (интуитивно) значительно слабее
,чем (QF-IA)—подобные Q или I

0

+ Exp-слишком слабы, чтобы делать свою работу. Таким образом, рассмотрим

пары ACA

0

, PA и NBG, ZF: это ACA

0

(соответственно. NBG) является доказательством-теоретически сводимым
к PA (ОТВ. ZF) обычно считается парадигматическим случаем для этого межтеоретического
отношения.

14

Если теоретико-доказательство сводимости были определены, как указано выше, но с I

0

+ Опыт

12

См. [7] и [31]. Аналогичная теорема справедлива, если L предполагается расширением L

АФР

и еще: "я...

1

” есть

заменено на “(QF-IA)".

13

В частности,

ρ

Т

является транзитивным для этих теорий. Это не так, однако, для неравномерно доказуемых

относительная согласованность, которая не может быть транзитивной для широкого круга теорий, см. [31].

14

Обратите внимание, что в обоих случаях мы не имеем относительной интерпретируемости результатов.

158

К.-Г. Niebergall

вместо (QF-IA), однако, эти пары теорий перестали бы быть примерами для
теоретико-доказательной сводимости; ибо П. Пудлак показал I

0

+ Опыт

Зубрить

ЗФ

→ Против

НБС

(см. [37]; аналогичный результат имеет место для ACA

0

и ПА). Теории между I

0

+ Опыт

и я

1

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

U: I

0

+ Supexp, например,

действительно доказывает " Кон

па

→ Против

технический заказчик

0

"; но так как это также доказывает " Кон

q

"(см. [9]), Q будет

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

15

На данном этапе я не буду принимать решения в пользу или против любого из определений
2-4. Скорее, я буду иметь дело с каждым из них до тех пор, пока это имеет смысл, давая понять
в каждом конкретном случае, который находится под следствием.