Непейвода Н.Н. Прикладная логика

Подождите немного. Документ загружается.

16.9. РЕАЛИЗУЕМОСТИ

451

ется просто как строка символов. Соответственно, преобразова-

ния высших порядков не обязаны давать одинаковые значения для

кодов одних и тех же функций.

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

точному определению.

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

Каждой формуле

сопоставляется множество на-

туральных чисел

 A

(множество ее

рекурсивных реализаций

n ∈

 A

читается «

рекурсивно реализует

» (или просто «реа-

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

определяется контекстом) и обозначается сокращенно

 A

 (t = u) =

(

{0}

Значения равны;

∅

Значения различны.

 A & B ⇔ ∃n

, n

(n = [n

, n

] & n

 A & n

 B)

 A ∨ B ⇔ ∃n

, n

(n = [n

, n

] & (n

= 0 ⇒ n

 A) &

6= 0 ⇒ n

 B))

 (A ⇒ B) ⇔ ∀m(m

 A ⇒ !U(n, m) & U(n, m)

 B)



A =

(

{0},

 A = ∅;

∅,

 A 6= ∅.

 ∀x A(x) ⇔ ∀m(!U(n, m) & U(n, m)

 A(m))

 ∃x A(x) ⇔ ∃n

, m(n = [n

, m] & n

 A(m))

В этих пунктах считаются фиксированными некоторое кодирование кор-

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

сальная рекурсивная функция

U(x, y)

Предложение 16.9.1. Любая теорема интуиционистской арифметики

рекурсивно реализуема.

Доказательство. Единственный нетривиальный пункт — реализу-

емость индукции. Но здесь реализация заключения строится примитив-

ной рекурсией по реализациям посылок

Замечание

Не обольщайтесь, что построение, извлеченное из арифме-

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

тивно-рекурсивно строится программа функции.

452

ГЛАВА 16. ИНТУИЦИОНИСТСКАЯ ЛОГИКА

Сразу же после того, как появилась первая точная интерпретация реа-

лизуемости, стали появляться результаты, показывающие, что реализу-

емость отличается от логической выводимости.

Пример 16.9.1. Абсолютная формула

—такая, которая понимается оди-

наково в классической и конструктивной математике. Например, тако-

вы формулы

∀x f(x) = 0

, где

— примитивно-рекурсивания функция.

Среди таких формул есть как выражающие разрешимые свойства, так и

выражающие неразрешимые свойства.

Рассмотрим абсолютную неразрешимую формулу

A(x)

. Тогда, если

бы формула

∀x(A(x) ∨

A(x))

была реализуема, то имелась бы ре-

курсивная функция, которая по числу

выдавала бы пару, первый эле-

мент которой является дискриминатором случая, а второй — реализа-

цией соответствующей формулы. Взяв первую компоненту результата,

мы смогли бы построить рекурсивную характеристическую функцию

неразрешимого множества

. Значит, у рассматриваемой формулы нет

реализации, и, по определению, тогда реализуема

∀x(A(x) ∨

A(x)).

(16.28)

Этот пример подтвердил в частном, но точном случае ранее содер-

жательно проведенный нами анализ колмогоровской интерпретации. В

свое время он произвел шокирующее действие. Хотя при более глубо-

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

матика может расходиться с классической, почти никто из математиков

и философов этого не ожидал.

Следующий принцип впервые явно сформулировал А. А. Марков.

Мы уже формулировали его содержательно на стр. 345.

Формальный принцип Маркова:

∀x(A(x) ∨

A(x)) &

¬¬

∃x A(x) ⇒ ∃x A(x)

(16.29)

Еще один формальный принцип был сформулирован независимо

С. К. Клини и Н. А. Шаниным, но по заслугам носит другое имя.

Формальный тезис Черча:

∀x(

A(x) ⇒ ∃y B(x, y))

⇒ ∃e ∀x(

A(x) ⇒!f

(x) & B(x, f

(x)))

(16.30)

Данная конструкция переносится практически на любое точное понятие реализуе-

мости, изменяется лишь понятие абсолютной и неразрешимой формулы.

16.10. ИНТУИЦИОНИСТСКАЯ ЛОГИКА И КАТЕГОРИИ

453

Итак, если мы можем найти y, исходя из предположения, не дающего

нам никакой дополнительной информации, но, возможно, отбрасываю-

щего нежелательные случаи, то это построение может быть выполнено

алгоритмом.

Заметим,что принцип Маркова является классически истинной фор-

мулой, а тезис Черча противоречит классической логике.Исходя из него,

доказывается формула (16.28).

Сам же Клини некоторое время спустя предложил вариацию поня-

тия реализуемости. Он стал рассматривать лишь всюду определенные

рекурсивные функции и определяемые ими всюду определенные функ-

ционалы конечных типов. Теперь уже пришлось, как и в исходном кол-

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

требовать, чтобы реализация было соответствующего типа, но схема

осталась прежней (только осмысленность была всегда выполнена). В

общерекурсивной реализуемости принцип Маркова уже не выполнен,

зато выполнен другой принцип, также классически истинный, но кон-

структивно несовместимый с приципом Маркова. Он обычно называет-

ся принципом независимости от посылки (

Принцип IP:

∀x(

A(x) ⇒ ∃y B(x, y)) ⇒ ∀x ∃y(

A(x) ⇒ B(x, y))

(16.31)

Этот принцип еще сильнее унижает отрицание: оно не может хоть чем-

то помочь при нахождении объектов. Он имеет и свое пропозициональ-

ное выражение, називаемое принципом Медведева:

(

A ⇒ B ∨ C) ⇒ (

A ⇒ B) ∨ (

A ⇒ C) (16.32)

Рассмотренные два одинаково красивых, но несовместимых между со-

бой случая были лишь началом в построении целой совокупности раз-

личных понятий реализуемости.

§ 16.10. ИНТУИЦИОНИСТСКАЯ ЛОГИКА И КАТЕГОРИИ

Последний вид семантик неклассических логик — категорные интер-

претации. В принципе колмогоровская интерпретация подсказывает ка-

тегорную, но функционалы, конечно же, приносят немало хлопот.

Из интерпретации Колмогорова сразу же видно, что конъюнкции со-

ответствует прямое произведение реализаций, а дизъюнкции — их пря-

мая сумма. Простейшая категорная конструкция, превращающая мор-

физмы в объекты, так называемая категория морфизмов. Ее объектами

454

ГЛАВА 16. ИНТУИЦИОНИСТСКАЯ ЛОГИКА

являются морфизмы, а морфизмом между f и g считается коммутатив-

ная диаграмма

(16.33)

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

богатства операций над морфизмами и, с другой стороны, выводит нас

за пределы исходой категории

. Поэтому в определении семантики ин-

туиционистской логики используется гораздо более сильная категорная

конструкция — экспоненциал.

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

Объект

называется

экспоненциалом

объектов

, если есть морфизм

означивания ev : b

× a → b

, такой, что для

любого объекта

и любого

g : c × a → b

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

диаграмма

× a

c × a

ˆg×e

Таким образом, морфизм ev играет роль функционала означивания,

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

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

функции на данном аргументе

g можно рассматривать как функцию

от двух аргументов g(c

, a

) ∈ b. По преобразованию Карри, функцию

от двух аргументов можно заменть на функционал (g → (a → b)), ко-

торый и обозначается на диаграмме ˆg. Поскольку стрелка пунктирная,

такой ˆg находится единственным образом.

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

Карри или, что эквивалентно, функционал частичной параметризации.

Что гораздо важнее, поскольку пойти на сознательное ограничение класса операций

в некоторых случаях даже целесообразно.

Естественно, все это верно лишь если морфизмы есть функции либо программы, но

аналогия работает и в других случаях.

16.11. О ФОРМАЛИЗАЦИИ НЕЗНАНИЯ

455

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

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

которая готова принять оставшиеся неизвестными аргументы.

Понятие частичной параметризации — понятие, важность которого

давно выяснена в теории, реализация которого исключительно легка и

которое по какой-то тупости и инерции все время забывается в опреде-

лениях языков программирования, претендующих на работу со значени-

яи высших типов. Из-за этого подобные языки безнадежно ущербны с

самого начала, становясь либо фантастически неэфективными (ЛИСП),

либо провоцирующими неестественный стиль программирования.

В категории можно проинтерпретировать пропозициональную ин-

туиционистскую логику, если в ней есть конечные прямые произведе-

ния и прямые суммы, а также экспоненциалы. В этом случае, следуя

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

ется объект.

Подробнее можно посмотреть данную конструкцию и ее примене-

ния в книге [12].

Упражнения к § 16.10

16.10.1. Вглядимся в диаграмму для экспоненты, конкретизированную

для категории частичного порядка. Чем окажется в данном случае

экспонента? Нет ли аналогий с псевдобулевыми алгебрами?

§ 16.11. О ФОРМАЛИЗАЦИИ НЕЗНАНИЯ

Для тех, кто к совершенству путь прошел,

Неведение знанием бывает.

А знанье, что невежда приобрел,

В невежестве его изобличает.

(Руми. [23, стр. 212])

Рассмотрим принципиально новые возможности, предоставляемые

интуиционизмом в области формализации.

Творческая последовательность.

α(n) =

(

если в году n не доказана формула A,

1, если она доказана.

456

ГЛАВА 16. ИНТУИЦИОНИСТСКАЯ ЛОГИКА

Видно, что творческая последовательность идейно совпадает с мо-

делью Крипке интуиционистской логики. В моделях Крипке формула

может некоторое время оставаться неразрешенной, а затем при движе-

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

никогда не станет истинной, она по определению считается ложной.

Принцип, формально выражающий наличие творческих последователь-

ностей, носит называние схемы Крипке, хотя Крипке лишь вторым на-

писал его формальное выражение. В доказательствах его использовал

уже Брауэр, а под другим названием — конструкций — изоморфный

принцип использовал и формально выразил Крайзел:

∀x ∃α(A(x) ⇔ ∃n α(n) = 1). (16.34)

Беззаконные последовательности. Вводится новый тип последова-

тельностей, обладающий следующим свойством:

∀α(A(α) ⇒ ∃n ∀f(∀m(m < n ⇒ α(m) = f(m)) ⇒ A(f ))),

т. е. все, что мы о них знаем, мы знаем из уже полученной информации.

Здесь f — произвольная последовательность. Брауэр приводил в каче-

стве примера последовательности, естественно формализуемой как без-

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

из физического источника, природа которого неизвестна.

Из определения беззаконности следует, что никакая беззаконная по-

следовательность не равна тождественно нулю, то есть

∀α

∀n α(n) = 0. (16.35)

В самом деле, возьмем произвольную беззаконную последовательность

α. Если бы она была тождественно равна нулю, то это мы узнали бы из

конечного числа ее членов, но тогда было бы такое конечное число n

членов, что любая последовательность, первые n членов которой были

бы равны нулю, была бы тождественно равна нулю, что абсурдно.

Нельзя ввести вместо переменной по беззаконным последователь-

ностям предикат “быть беззаконной”, поскольку его отрицание устана-

вливалось бы, исходя из конечного числа значений последовательности.

Так что не всегда тип данных можно заменить новым предикатом.

Трулстра (Голландия, 1968) доказал, что композиции алгоритмов и

беззаконных последовательностей образуют модель интуиционизма, в

которой можно промоделировать творческие последовательности.

16.11. О ФОРМАЛИЗАЦИИ НЕЗНАНИЯ

457

Беззаконные последовательности явились первым примером пози-

тивного использования незнания в точных науках. Возможность сфор-

мулировать незнание в виде логической формулы — еще одно достиже-

ние интуиционизма.

Глава 17. Семантики Крипке

и базирующиеся на них логики

Семантики Крипке стали ныне одним из наиболее распространенных

орудий в современной неклассической логике, в философии и в когни-

тивной науке. Общая их идея соответствует тому, что мы видели в ин-

туиционистской логике.Модели представляется как множество возмож-

ных миров. Эти миры связаны некоторыми отношениями и некоторые

логические связки заставляют переходить от данного мира к другим свя-

занным с ним мирам. Рассмотрим эту конструкцию на примерах.

§ 17.1. ОБЩАЯ ИДЕЯ

Еще Аристотель, создавая логику, рассматривал тот ее фрагмент, кото-

рый позже лег в основу классической логики как частный случай. Он

осознавал, что понятие истинности слишком часто привязано к случай-

ным обстоятельствам, в которых мы оказались. Поэтому статус истин-

ных предложений

2 × 2 = 4 (17.1)

Аристотель родился в Стагире (17.2)

совершенно разный. Первое из них необходимо, оно не зависит от на-

шего конкретного мира, а второе просто (или даже случайно) истинно

именно в нашем конкретном мире. А вот предложение

Аристотель родился в Афинах (17.3)

в нашем конкретном мире ложно, но оно является возможным: вполне

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

там.

Значительная часть логики Аристотеля была посвящена модальным

утверждениям, содержащим модальности (прежде всего, возможность

17.1. ОБЩАЯ ИДЕЯ

459

и необходимость). Но в средние века эта часть его теории практиче-

ски игнорировалась. В большинстве университетов Аристотеля разре-

шалось изучать лишь до модальностей. Обоснованием этого являлось

опасение, что, узнав про модальности, студенты засомневаются, что Бог

сотворил лучший из возможных миров, и даже могут перейти к гности-

ческо-буддийской ереси, что миров очень много

Истолкование модальностей ‘возможно’ и ‘необходимо’ требует пе-

Гностики — секты времен раннего христианства. Некоторые из них признавали Хри-

ста, а некоторые были скорее просвещенными язычниками. Общим был у них взгляд на

мир, который они рассматривали как изначально злой, порожденный слабым послан-

цем Бога — Демиургом (творцом, ремесленником с оттенком “халтурщик”). Души то-

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

перевоплощаются.

Буддизм сходен с гностицизмом в изначально пессимистическом взгляде на мир и в

общей задаче — освобождения душ от зла мира. Но он даже несколько более атеисти-

чен по исходной природе, поскольку для него мир — не творение, а самоорганизующа-

яся система духовных атомов — дхарм. Зато роль человека в мире для буддистов ис-

ключительно велика даже по сравнению с христианством, а не то что с гностицизмом.

Лишь люди могут достичь высших степеней духовного совершенства, чтобы освобо-

диться самим и, возможно, помочь освободиться и другим (в разных толках буддизма

это трактуется по-разному). Поэтому христиане упрекают гностиков в богохульстве, а

буддистов — в гордыне.

И то, и другое учение склонно к признанию существования множества миров. Джай-

ны вообще включили множественность миров в свою догматику.

Стоит различать множественность обитаемых миров в нашем Мире, во Вселенной,

и множественность Миров с разными законами. Первое даже в средние века не счи-

талось противоречащим совершенству Божию. В частности, кардинал Николай Кузан-

ский интенсивно развивал идею множественности обитаемых миров, отвергая геоцен-

трический взгляд. И самого Джордано Бруно сожгли вовсе не за его натурфилософские

взгляды, в частности, за проповедь множества обитаемых миров (что даже в те времена

могло квалифицироваться инквизицией в худшем случае как подозрительное в ереси

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

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

Современный католицизм считает, что миров может быть много, поскольку, хотя Бог

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

неоднозначно (порядок является лишь частичным). А что касается нашей Вселенной,

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

жизнь может существовать лишь на Земле. Повсюду, где есть условия для появления

разумных существ, они должны появляться, дабы славить Творца.

Православные богословы здесь занимают менее определенную позицию, предпочи-

тая не отвечать на такие провокационные и вводящие в соблазн вопросы.

460

ГЛАВА 17. СЕМАНТИКИ КРИПКЕ

рехода от одного мира к целому множеству возможных миров.

Возможное — то, что истинно в одном из миров.

(17.4)

Необходимое —то,что истинно не только в нашем

случайном мире, но и во всех возможных мирах.

(17.5)

На самом деле это же истолкование нужно и для других модально-

стей. Например, рассмотрим предложение

Завтра будет морское сражение.

(17.6)

Это предложение сам Аристотель приводил в качестве примера выска-

зывания, к которому не применим сильный закон исключенного третье-

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

состоянию. Поэтому и в логиках, изучающих временные соотношения,

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

модели — фиксированное состояние одного и того же Мира

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

торый начал изучать также Аристотель, — ассерторические модально-

сти. Пусть некто говорит:

Я знаю, что

(17.7)

Чтобы проанализировать и проинтерпретировать данное квазивысказы-

вание, нам необходимо перейти из нашего мира в мир внутренних пред-

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

мантика возможных миров.

И, наконец, даже в описании логик программ естественна та же кон-

струкция, поскольку каждый оператор программы изменяет ее область

памяти и, так сказать, переносит нас из одной модели в другую с той

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

кретных высказываний и поэтому уже не подходит для изменяющегося мира. Но дан-

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

и поэтому теория, основанная на классической логике, вполне может описывать изме-

няющийся мир. В частности, таковы многие модели, основанные на дифференциаль-

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

изменения, процессы, протекающие в мире.