ПРИЛОЖЕНИЕ

Цель этого приложения — коротко объяснить смысл, который мы придаем термину конструктивный.

Все рассматриваемые нами объекты должны быть конструктивными объектами, т. е. конечными конфигурациями знаков. Эти знаки, которые могут быть непосредственно распознаны как равные или различные, рассматриваются как далее неразложимые атомы. Конструктивные объекты должны рассматриваться как конкретные объекты, т. е. в конечном счете как существующие во времени и пространстве. Например, формулы и доказательства в формальной системе являются конструктивными объектами в этом смысле, а произвольные осмысленные утверждения и неформальные доказательства не являются. Также и множества в обычном интуитивном смысле, безусловно, не являются конструктивными объектами.

Мы принимаем анализ оперирования над конструктивными объектами по механическим правилам, данный Постом [1] и Тьюрингом [1]. В соответствии с этим анализом правила вычислений, так же как и сами вычисления, снова являются конструктивными объектами и оказывается разрешимым вопрос о корректности вычисления по данным правилам. Точнее, имеется разрешимый предикат выражающий, что корректное вычисление по правилу с начальными данными этом случае мы можем считывать результат вычисления Так как конструктивные объекты — это просто конфигурации знаков, их можно закодировать натуральными числами.

Мы скажем, что применимо к если существует такое, что

Отсюда немедленно получается, что не может быть правила, которое позволило бы нам решать для бого правила применимо ли оно к самому себе, Действительно, тогда имелось бы правило приме нимое к тогда и только тогда, когда не применимо к самому себе:

В частности, применимо к себе тогда и только тогда, когда не применимо к себе:

что противоречиво.

Любая теорема конструктивной математики, после того как она до конца проанализирована, имеет утвердительную форму: найден конструктивный объект с определенным свойством. Критический вопрос состоит в том, какие свойства мы собираемся считать конструктивно осмысленными.

Простейший случай представляет разрешимое свойство Это просто правило, позволяющее нам вычислять истинностное значение для любого натурального . В применении к таким свойствам классические пропозициональные связки имеют четкий вычислительный смысл, который задается обычными таблицами истинности, и применима классическая логика высказываний. Например, - разрешимое свойство, которое имеет место для всех натуральных

Классически произвольные логические формулы, построенные из разрешимых предикатов с помощью пропозициональных связок и кванторов (для всякого) и V (существует) по числовым переменным, считаются осмысленными в терминах классического понятия истинности, и законы классической логики предикатов истинны при такой интерпретации. Например, формула

истинна в классическом смысле.

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

Начнем с того, что будем считать конструктивно осмысленными свойствами вида

где разрешимо. Частными случаями являются т. е. т. е. Самый типичный пример -свойства — это применимость правила ко всем числам

Утверждая. мы имеем в виду, что мы нашли метод, позволяющий нам каждый раз, когда нам дано натуральное число найти такое натуральное что верно Заметим, что подразумеваемый смысл утверждения — тот же самый и при классической интерпретации. Действительно, если истинно классически, то мы действительно имеем метод нахождения для каждого натурального числа такого, что истинно Мы просто вычисляем одно за другим истинностные значения

пока не обнаружим для которого верно Таким образом, между классической и конструктивной интерпретациями Пгутверждений нет разницы в отношении подразумеваемого смысла. Разница заключается в допускаемых методах доказательстваг Например, пусть -утверждение, что есть гёделевский номер некоторого доказательства в аксиоматической теории множеств (или даже в арифметике второго порядка) с последней формулой Тогда разрешимый предикат, а утверждение

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

Рассмотрим теперь произвольную предваренную формулу

с разрешимым Мы скажем, что эта формула конструктивно истинна, если мы нашли правила такие, что применима ко всем -членным системам натуральных чисел, и

В полной записи это значит, что мы нашли правила такие, что

Это свойство считается конструктивно осмысленным, так как оно имеет вид

Формула

не является конструктивно истинной, хотя она истинна классически. Действительно, предположим, что правило, применимое ко всем натуральным числам и удовлетворяющее

Тогда

так что мы имели бы разрешающую процедуру для предиката что невозможно. Этот пример показывает, что законы классической логики, в частности закон исключенного третьего, могут вести к заключениям, не являющимся конструктивно истинными.

Первые две главы основаны на некритическом принятии утверждений как конструктивно

осмысленных, а нужные рудименты логики можно понижать в терминах конструктивной истинности.

Мы уже видели, что классическое понятие истины отличается от понятия конструктивной истинности. Тем не менее оказывается, что понятие арифметической истины может быть конструктивно понято совершенно иным способом, с помощью интерпретации отсутствием контрпримера (которая была намечена Эрбраном [1] для случая логики предикатов и распространена на теорию чисел Крайзелем [1]; последнему принадлежит и терминология). Рассмотрим снова предваренную формулу

которую мы обозначим через А. Тогда

где область значений все теоретико-числовые функции от аргумента, Следовательно,

причем последняя формула называется интерпретацией отсутствием контрпримера для А. Кодируя в виде единой бесконечной последовательности натуральных чисел и виде одного натурального числа, мы видим, что интерпретация отсутствием контрпримера имеет вид

где разрешимое свойство конечных последовательностей натуральных чисел. Наиболее типичным примером свойства является свойство быть ординалом конструктивного второго числового класса.

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

Как легко видеть, эквивалентность

заперта для

имеет место классически. Таким образом, подразумеваемый смысл утверждения один и тот же как для принятой нами конструктивной интерпретации, так и для классической интерпретации. Разница только в принимаемых методах доказательства. Это полностью аналогично рассмотренной ранее ситуации для -утверждений.

В интуиционистской математике обе части приведенной выше эквивалентности считаются осмысленными. При этом считается, что область изменения переменной, связанной левым квантором всеобщности, — это все свободно становящиеся последовательности натуральных чисел. Тот факт, что эта эквивалентность справедлива интуиционистски, является содержанием бар теоремы Брауэра. Мы рассматриваем рассуждение Брауэра [11] в доказательстве бар теоремы скорее как интуитивный анализ, оправдывающий наше определение истинности -утверждения.

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

последовательностей — истолкование кванторов по теоретикочисловым функциям как кванторов по правилам, определяющим такие функции, т. е. по числам таким, что Это путь, избранный конструктивистской школой Маркова, а также Бишопом [1] в его недавней книге (которая не была доступна автору в процессе работы над рукописью). В случае Бишопа при помощи подходящих предположений о непрерывности удается избежать патологий, порожденных этой концепцией.

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

В действительности, как только мы соглашаемся признавать -утверждения конструктивно осмысленными, мы можем понимать конструктивно гораздо больше, чем понятие арифметической истинности. Большая часть анализа, включая теорию ординалов второго числового класса, борелевских множеств и меры Лебега, может быть рассмотрена с использованием этих абстракций. Это показано в последних двух главах. Однако для конструктивного анализа теоремы Кантора — Бендиксона (Крайзель [2]) нужны более сильные методы, и то же верно для аналитических и, в еще большей мере, проективных множеств.

Более мощные средства, достаточные по крайней мере для рассмотрения теоремы Кантора — Бендиксона, получаются введением более высоких конструктивных числовых классов.