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

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

16.2. ИНТЕРПРЕТАЦИЯ КОЛМОГОРОВА

431

3. Есть отображение

, такое, что

∀a (a

 A & f

 (A ⇒ B) ⊃ !ev(f, a) & ev(f, a)

 B) .

* Для квантора

∀

 ∀x A(x) ⊃ ∀a (a ∈ U ⊃ !ev(f, a) & ev(f, a)

 A(a)) .

4. Если нет таких

, что

 A

, то



Если главные импликации

⊃

повсюду заменить на

≡

, то интерпретация

называется

строго колмогоровской

или просто

колмогоровской

Через

 A

обозначается тот факт, что

 A

непусто. Если

 A

то

называется

реализуемой

в данной колмогоровской интерпретации.

Это определение отличается от оригинального в нескольких отно-

шениях. Во-первых, у Колмогорова не было явно указанных отображе-

ний и операторов, а прямо говорилось, что множество

 A & B —

прямое произведение

 A ×

 B, множество

 A ∨ B — пря-

мая сумма

 A ⊕

 B. Пункт, соответствующий

 A ⇒ B, был

определен только частично. Было сказано, что элементами

 A ⇒ B

являются эффективные преобразования

 A в

 B, но само понятие

эффективного преобразования оставалось неопределенным.

Таким образом,в сущности интерпретация Колмогорова была мета-

интерпретацией, общим методом построения целого множества интер-

претаций. Наше определение еще сильнее подчеркивает этот аспект и ее

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

и отображения, определявшиеся в пунктах 1 и 2. Они наводят на вос-

поминание об определяющих диаграммах для прямого произведения и

прямой суммы (ч. I, диаграммы 5.9, 5.10).

Посмотрим, что гарантирует наше слабое определение.

Предложение 16.2.1. Выполнены следующие соотношения:

1. Если

 A и !

 B, то !

 A & B.

2. Если !

 A & B, то !

 A и !

 B.

3. Если !

 A и !

 A ⇒ B, то !

 B.

4. Если !

 A или !

 B, то !

 A ∨ B.

432

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

5. Не могут быть одновременно !

 A и !



6. Если

 ∀x A(x), то !

 A(u) для любого u ∈ U.

7. Если

 ∃x A(x), то !

 A(u) для некоторого u ∈ U.

8. Если

 A(u) для некоторого u ∈ U, то !

 ∃x A(x).

Таким образом, прямые правила вывода классической логики (за ис-

ключением правила снятия двойного отрицания, отвергнутого Брауэ-

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

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

Интерпретация Колмогорова служит и сильным косвенным, полу-

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

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

ного отрицания, критиковавшиеся Брауэром в его диссертации.

Пример 16.2.1.

Реализуемость

A ∨

означает возможность либо по-

строения реализации

, либо установления, что такой реализации не

существует. А именно, для каждого

имеется элемент, из которого с

помощью операции

case

можно получить либо реализацию

, либо ре-

ализацию

. Если этот закон принят как общий, то такая проверка

должна делаться допустимыми у нас средствами. Значит, если мы инте-

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

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

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

Пример 16.2.2.

Доказано, что

элементарная теория действительных

чисел

элементарная геометрия

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

формулировку аксиом элементарной теории действительных чисел.

Сигнатура состоит из отношений

, операций сложения, умно-

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

Div(x, y, z)

, истинного, когда

x/y = z

Аксиомы делятся на три группы. Первая — стандартные аксиомы

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

как

x−x

как

x/x

для произвольного

x 6= 0

Вторая — аксиомы линейно упорядоченного поля.

∀x, y, z(x > y & y > z ⇒ x > z) ∀x, y, z(y < z ⇒ x + y < x + z)

∀x, y, z(y < z & x > 0 ⇒ x ∙ y < x ∙ z) ∀x

(x > x)

0 < 1 ∀x, y(x = y ∨ x < y ∨ x > y)

(16.6)

16.2. ИНТЕРПРЕТАЦИЯ КОЛМОГОРОВА

433

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

существование корня для любого многочлена нечетной степени.

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

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

вать на их языке (логику мы рассматриваем пока что классическую).

Например,в элементарной теории действительных чисел можно форму-

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

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

полны, они разрешимы. Таким образом, в геометрии закон исключен-

ного третьего полностью корректен, поскольку любое утверждение

принципе

можно проверить на истинность либо ложность (вопрос о том,

сколько реально ресурсов для этого потребуется, нас сейчас не интере-

сует). Поэтому эллины совершенно правильно пользовались классиче-

ской логикой при построении своей математики.

Что означает реализуемость A ∨

A без ограничений на язык? Зна-

чит, мы можем решить любую задачу! Значит, теорема Гёделя о непол-

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

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

цип всезнания и выглядит совершенно нереалистичным

Анекдотично, но показательно для стиля мышления большинства математиков сле-

дующее. Теоремы Гёделя во времена Брауэра сначала не было, а затем он принципи-

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

поскольку не считал, что теорема имеет отношение к сущности классической матема-

тики (в этом отношении он был прав, поскольку теорема Гёделя имеет отношение к

сущности любой достаточно богатой формализации любой математики). Поэтому

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

следующим образом.

Мы не знаем, есть ли в десятичном разложении числа

π последова-

тельность цифр

0123456789. Поэтому, если через A обозначить утвер-

ждение

В десятичном разложении

π есть последовательность цифр

0123456789,

(16.7)

то мы не можем утверждать ни

A, ни

, и поэтому A ∨

A нельзя

считать истинным.

Брауэр не мог вообразить себе ни мощности и общедоступности современных ком-

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

что эта последовательность встречается в числе π и объявил о решении проблемы, дав-

но поставленной интуиционистами!

434

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

А чем же провинился принцип двойного отрицания? Тут вопрос не-

сколько тоньше. Рассмотрим формулу

¬¬

. Когда она реализуема и

каковы ее реализации?

Реализацией ее является стандартный элемент

0, а реализуема она,

когда нет реализаций у

. Расшифровываем последнее условие и по-

лучаем интересное соотношение:

¬¬

реализуема тогда и только тогда, когда ре-

ализуема A, но реализацией ее является заранее

известный элемент 0.

(16.8)

Что теперь означало бы принятие закона

¬¬

A ⇒ A

? Тогда был бы об-

щий метод преобразовывать любую решаемую проблему в ее решение,

т. е. общий решатель задач

. Итак, закон снятия двойного отрицания с

конструктивной точки зрения означает существование общего решателя

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

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

Пример 16.2.3.

Рассмотрим вопрос, может ли интуиционистская тео-

рия противоречить классической? Пусть

A(x)

— неразрешимое свой-

ство, а наши эффективные методы — алгоритмические. Тогда нет та-

кого функционала

, который реализует

∀x(A(x) ∨

A(x))

, и, зна-

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

∀x(A(x) ∨

A(x))

Пример 16.2.4.

Рассмотрим совершенно неформальный пример, тем не

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

получать

∃x

A(x)

из

∀x A(x)

Пусть реализовать

A(x)

означает соблазнить девушку

. Тогда реа-

лизовать

∀x A(x)

— это найти общий метод соблазнения любой девуш-

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

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

творчески.

Неформальные ответы на многие вопросы требуют исследования

более тонкой структуры колмогоровской интерпретации.

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

традиционно являлся одной из целей классического искусственного интеллекта. Неко-

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

16.2. ИНТЕРПРЕТАЦИЯ КОЛМОГОРОВА

435

Пример 16.2.5.

Рассмотрим следующий вопрос:

Каков конструктивный смысл формулы A ⇒ A и

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

неверна?

(16.9)

Ее реализацией является тождественная функция, и, соответственно,

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

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

образом, чтобы не было

A ⇒ A

, необходимо не иметь и тождественных

функционалов. В частности, для этого достаточно учесть, что есть вре-

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

Пример 16.2.6.

Чуть-чуть видоизменим предыдущую импликацию.

A ⇒ A & A

уже требует удвоения реализации

. А если на реализа-

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

такой реализации. Конечно, примером такого ресурса опять-таки может

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

ваться при бездействии, но расходоваться при действиях.

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

Пусть реализации конъюнкции, дизъюнкции и существования —

прямые суммы и прямые произведения.

16.2.1. Что получится, если в качестве реализаций

A ⇒ B будут рас-

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

ции f :

 A →

 B? А если еще обобщим и будем рассматри-

вать все отношения?

16.2.2. А если теперь будем рассматривать лишь постоянные функции?

16.2.3. Рассмотрим формулу

(

A ⇒ B ∨ C) ⇒ (

A ⇒ B) ∨ (

A ⇒ C).

Студент Классиков следующим образом обосновал ее конструк-

тивную приемлемость.

Пусть некоторый функционал

ϕ решает задачу

A ⇒ B ∨ C

Тогда ϕ по решению

вычисляет, какой из членов дизъюнкции

решается, и дает его решение. Но реализация отрицания извест-

на заранее — 0. Так подставим 0 в ϕ и получим, какой из членов

436

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

дизъюнкции в заключении решается, а уж его решение нетрудно

получить опять-таки из ϕ!

Можете ли Вы что-либо возразить, и если да, то что? Если возра-

жаете, то что разумного в рассуждениях Классикова?

16.2.4. Почему мы не включили в число аксиом действительных чисел

плотность порядка

∀x, y(x < y ⇒ ∃z(x < z & z < y))? (16.10)

16.2.5. Напишите одну аксиому, выражающую наличие корня у любого

многочлена третьей степени.

16.2.6. Мы позаботились о существовании корней у многочленов не-

четной степени. А как доказать существование

√

§ 16.3. ФОРМАЛИЗАЦИЯ ГЕЙТИНГА

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

дал ученик Брауэра А. Гейтинг. Первоначально сам Брауэр не рассма-

тривал эту формализацию как нечто устойчивое, настаивая на нефор-

мализуемости не только интуиционистской математики (в чем он был

прав), но и самой логики (в чем он тоже был прав, если рассматривать

целый класс конструктивных логик). Но попытки видоизменить кон-

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

его формализация постепенно обрастала точными интерпретациями и

красивыми теоремами. В результате сейчас интуиционистскую логику

отождествляют с формализаций Гейтинга.

Формализацию Гейтинга проще всего описать как результат замены

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

двойного отрицания на правило из лжи следует все что угодно (ex falso

quodlibet).

(16.11)

Поскольку ex falso quodlibet допустимо в классической логике, любое

логическое доказательство в системе Гейтинга одновременно является

16.3. ФОРМАЛИЗАЦИЯ ГЕЙТИНГА

437

классическим доказательством

. Так что имеется возможность, не бу-

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

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

Доказательство закона исключенного третьего A ∨

A (11.2)

использовало закон двойного отрицания. В интуиционистской логи-

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

¬¬

(A ∨

Доказательство формулы A & ∃x B(x) ⇒ ∃x(A & B(x)) может

быть проведено интуиционистскими средствами, а ∀x(A ∨ B(x)) ⇒

A ∨ ∀x B(x) — нет.

В самом деле, рассмотрим два этих доказательства.

∗ A & ∃x B(x)



A ∃x B(x)

B(c

)

A & B(c

)

∃x(A & B(x))

A & ∃x B(x) ⇒ ∃x(A & B(x))

(16.12)

Второе доказательство:

∗ ∀x(A ∨ B(x))



∗ A ∗

| A ∨ ∀x B(x)



∗ z

произвольное



A ∨ B(z)

B(z)

∀x B(x)

A ∨ ∀x B(x)

∀x(A ∨ B(x)) ⇒ A ∨ ∀x B(x)

(16.13)

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

и правило ex falso quodlibet (когда из

и A ∨ B(z) следует B(z)).

Конечно, рассмотрение конкретного доказательства еще не обосно-

вывает неприемлемости данной формулы в интуиционистской логике.

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

Тем не менее в конкретных теориях, основанных на гейтинговской формализации

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

ской логике. См. далее.

438

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

Отметим,что свойство замены эквивалентных сохраняется и для ин-

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

казываются интуиционистски).

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

Попытайтесь доказать интуиционистски:

16.3.1.

A & (B ∨ C) ⇒ (A & B) ∨ (A & C).

16.3.2.

A ∨ (B & C) ⇒ (A ∨ B) & (A ∨ C).

16.3.3.

(A & B) ∨ (A & C) ⇒ A & (B ∨ C).

16.3.4.

(A ∨ B) & (A ∨ C) ⇒ A ∨ (B & C).

16.3.5.

A ⇒

¬¬

16.3.6.

A ∨ B ⇒ (A ⇒ B)

16.3.7.

(A ⇒ B) ⇒

A ∨ B.

§ 16.4. ПЕРВЫЕ МАТЕМАТИЧЕСКИЕ МОДЕЛИ

ИНТУИЦИОНИСТСКОЙ ЛОГИКИ

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

ревод на алгебраический язык. Поскольку свойство замены эквивалент-

ных сохраняется, остается без изменения и определение алгебры Лин-

денбаума-Тарского на стр. 206. Она теперь уже не обязательно будет

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

свойства.

Прежде всего,поскольку отношение ` A ⇒ B транзитивно, рефлек-

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

го порядка на элементах алгебры Линденбаума-Тарского. Далее, & и ∨

являются нижней и верхней гранями двух элементов согласно данному

отношению. Для обоснования этого достаточно доказать (для &; для ∨

аналогично):

A & B ⇒ A, A & B ⇒ B,

(C ⇒ A) & (C ⇒ B) ⇒ (C ⇒ A & B).

(16.14)

Таким образом, алгебра Линденбаума-Тарского интуиционистской те-

ории является решеткой. Более того, данная решетка дистрибутивна,

16.4. ПЕРВЫЕ МОДЕЛИ

439

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

есть и операция импликации, которую теперь необходимо охарактери-

зовать в терминах частично-упорядоченных множеств.

Рассмотрим характеристическое свойство импликации. Если

A и

A ⇒ B, то B. Для корректности вывода при оценках формул элемен-

тами частично-упорядоченного множества необходимо, чтобы ни один

шаг вывода не понижал оценки формул. Поэтому приходим к характе-

ристическому свойству импликации:

a ∩ (a ⊃ b) 4 b. (16.15)

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

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

элементом, для которого выполнено такое свойство. И тогда

a 4 b ⇔

(a ⊃ b) = 1.

Теперь рассмотрим частный случай, когда

b = 0. В этом случае

импликация a ⊃ 0 несовместима с a: a ∩ (a ⊃ 0) = 0, и, более то-

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

a ⊃ 0 естественно называть псевдодополнением a, и по аналогии в ал-

гебре (a ⊃ b) называют относительным псевдодополнением a относи-

тельно b.

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

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

додополнениями называется

гейтинговой

или

псевдобулевой

алгеброй.

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

имеем

Предложение 16.4.1. Каждая интуиционистская теория имеет точ-

ную гейтинговозначную модель.

Доказательство. Такой моделью является алгебра Линденбаума-Тар-

ского рассматриваемой теории

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

циально придуманным для интуиционистской логики и поэтому не очень

интересным. Но уже в 30-х гг. Тарский и Куратовский показали, что

решетки открытых множеств топологического пространства являются

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

формул интуиционистской логики можно брать открытые множества

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

[0, 1]).

440

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

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

ство, ложной — если ее значение есть ∅.

Значением

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

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

когда не является открытым. Но можно взять внутренность дополнения

A: Int

A. Одна из эквивалентных формулировок определения внутрен-

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

жащееся, что в точности соответствует псевдодополнению.

Соотвественно, значение импликации определяется «почти» как в

булевой алгебре:

(A ⊃ B) = Int(B∩

A).Еще одно место,где приходится

брать внутренность, — значение всеобщности, поскольку пересечение

бесконечного семейства открытых множеств не всегда открыто.

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

16.4.1. Покажите, что в определении псевдобулевой алгебры дистрибу-

тивность выводится из существования и единственности относи-

тельного псевдодополнения.

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

следующие формулы:

A ∨

¬¬

A ⇒ A

;

¬¬

A ∨

;

¬¬

A ∨ (

¬¬

A ⇒ A)

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

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

§ 16.5. МОДЕЛИ КРИПКЕ

Следующий класс моделей интуиционистской логики связан с давней

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

роэса. Если даже Бог может подчиняться законам логики, значит, она

описывает не только наш мир, но и другие возможные миры. Поэтому

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