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

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

12.4. ТЕОРЕМА БЕТА

341

12.3.3. В индуктивном утверждении мы позаботились о кванторах все-

общности для сигнатур. В каком пункте нашего доказательства

сигнатуры изменяются?

12.3.4. Студент Гениалькис сформулировал новую аксиоматику ариф-

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

ся в одной и той же аксиоме, а других операций нет (естественно,

в данной аксиоматике есть принцип математической индукции).

Он, исходя из этого, установил следующий результат:

Если в арифметике доказано утверждение вида

A ⇒ B, где A не

содержит умножения,а B не содержит сложения,то найдется фор-

мула C, содержащая лишь предикат равенства и константы, кото-

рая является интерполянтом.

Что Вы ему ответите?

§ 12.4. ТЕОРЕМА БЕТА ОБ ОПРЕДЕЛИМОСТИ

Докажем теперь, что семантическое несущественное расширение — то

же самое,что и несущественное расширение.Для этого достаточно уста-

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

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

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

Пусть даны сигнатура

и ее подсигнатура

.Пре-

дикат

P /∈ σ

называется

определимым

через

в теории

, если в сиг-

натуре

есть такая формула

A(x

, . . . , x

)

, свободные переменные ко-

торой

, . . . , x

, что в теории

доказуемо

∀x

. . . ∀x

(A(x

, . . . , x

) ⇔ P (x

, . . . , x

)).

Теорема 12.2. (Теорема Бета (Beth, 1952) об определимости) P опре-

делим через σ тогда и только тогда, когда в любых двух моделях M

теории Th с одинаковыми универсами и одинаковыми значениями

понятий из σ значения P совпадают.

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

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

щей его сигнатуры.

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

образование теории

Th. Отдублируем все предикаты и константы, не

342

ГЛАВА 12. ОСНОВЫ ТЕОРИИ ОПРЕДЕЛЕНИЙ

входящие в σ, двойник каждого предиката обозначим

, двойник кон-

станты — ˉc. Двойником формулы назовем результат замены всех по-

нятий, не входящих в σ, на их двойники. Теперь заменим все аксиомы

теории Th, содержащие понятия, не входящие в σ, на их двойники. По-

лучившуюся теорию обозначим

. Очевидно, что всякую модель

можно изоморфно преобразовать в модель Th и что двойник формулы

выводим в Th ттт формула выводима в Th. Последнее легче усмотреть

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

строив преобразование вывода.

Далее, если теория Th непротиворечива, то непротиворечива и те-

ория Th ∪ Th. Ее модель получается просто удвоением интерпретаций

понятий, не входящих в σ, в модели исходной теории. Теперь выведем

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

Th ∪Th ` ∀~x(P (~x) ⇔

P (~x)).

В самом деле, возьмем произвольную модель теории Th ∪ Th. Из нее

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

универсы и интерпретации понятий из σ. Значит, согласно допущению,

в них совпадают и интерпретации предикатов P и

. А совпадение ин-

терпретаций и означает истинность эквивалентности.

Теперь применяем теорему полноты и получим, что имеется вывод

формулы ∀~x(P (~x) ⇔

P (~x)) в теории Th ∪ Th. Возьмем все аксио-

мы, участвующие в этом выводе. Тогда в классической логике выводима

формула

& ∙∙∙ & A

& ∙∙∙ &

⇒ ∀~x(P (~x) ⇔

P (~x)), (12.1)

где

— все задействованные аксиомы теории Th, а

— все аксиомы

теории Th, не являющиеся аксиомами исходной теории и участвующие

в выводе эквивалентности. Значит, выводима импликация

& ∙∙∙ & A

⇒



& ∙∙∙ &

⇒ ∀~x(P (~x) ⇔

P (~x))



, (12.2)

являющаяся эквивалентным преобразованием формулы 12.1. Тогда вы-

водимы следующие две формулы, которые являются переформулиров-

ками обеих импликаций данной условной эквивалентности:

∀~x



& ∙∙∙ & A

& P (~x) ⇒



& ∙∙∙ &

⇒

P (~x)



, (12.3)

∀~x



& ∙∙∙ & A

& ¬P (~x) ⇒



& ∙∙∙ &

⇒ ¬

P (~x)



. (12.4)

12.4. ТЕОРЕМА БЕТА

343

Для первой из этих формул применим теорему Крейга и построим ин-

терполянт C, такой, что

∀~x (A

& ∙∙∙ & A

& P (~x) ⇒ C) , (12.5)

∀~x



C ⇒



& ∙∙∙ &

⇒

P (~x)



. (12.6)

Этот

C и является искомым выражением P через понятия σ. В самом де-

ле, C записано в сигнатуре σ, поскольку оно находится в общем словаре

посылки и заключения импликации 12.3. Далее, в теории Th доказуемо

∀~x (P (~x) ⇒ C) , (12.7)

а в

теории Th —

∀~x



C ⇒

P (~x)



. (12.8)

Но по изоморфизму

между Th и исходной теорией тогда

∀~x (C ⇒ P (~x)) (12.9)

в теории

Th. Искомая эквивалентность доказана.

Применением этой теоремы является, например, следующее рассу-

ждение. Операция извлечения квадратного корня неопределима через

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

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

рень из

−1 можно определить двояко: как i и как −i. Эти два определе-

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

x + iy 7→ x − iy

является изоморфизмом поля комплексных чисел.

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

12.4.1. Покажите, что операция умножения неопределима через сложе-

ние.

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

жение.

Глава 13. Неполнота

и неформализуемость

§ 13.1. ТЕОРЕМА ТАРСКОГО О НЕВЫРАЗИМОСТИ ИСТИНЫ

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

на языке классической логики. Соответственно, никакая теория не мо-

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

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

этом множестве, чего было бы часто достаточно. В частности, в таком

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

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

ния сводился бы лишь к оптимизации данного алгоритма

В самом деле, опишем следующий процесс. Будем порождать все-

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

мкнутой формулы

A, либо ее отрицания

. Поскольку одна из этих двух

формул доказуема, процесс поиска когда-нибудь закончится и наша про-

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

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

Лейбница: вместо того чтобы спорить, вычислять. Но обратите внимание на количество

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

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

предложен испанским схоластом Луллием, затем ехидно прокомментирован Свифтом

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

звание алгоритма британского музея.

Заметьте, что в данном рассуждении нет никакой оценки числа шагов, необходимых

для выдачи результата. Более того, оно опирается на один принцип, безусловно, при-

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

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

чающихся конструкций. Этот принцип был явно сформулирован русским математиком

13.1. ТЕОРЕМА ТАРСКОГО О НЕВЫРАЗИМОСТИ ИСТИНЫ

345

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

рий доказал в 1931 г. австрийский математик Курт Гёдель, тот самый,

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

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

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

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

рый может считаться идейной основой результата Гёделя

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

дается индуктивно. Пусть у нас зафиксировано некоторое кодирование

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

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

скольку слова в данном конечном алфавите естественно кодируются как

натуральные числа в соответствующей системе счисления: см.стр. 137.)

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

подстановку, т. е. построить формулу Subst(x, y, z), такую, что

∀x ∀y ∃1z Subst(x, y, z)

для любого кода a формулы A(x) с одной свободной переменной x и для

любого объекта b объект ιzA(a, b, z) является кодом A(b). Тогда, соглас-

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

цию sub(A, b), вычисляющую по коду формулы A,имеющей свободную

переменную, и по объекту b код формулы, являющейся подстановкой b

вместо

в данную формулу. Код формулы

обозначим

dAe

Определением истинности по Тарскому называется такая формула

Tr, что для любого кода замкнутой формулы A

Tr(dAe) ⇔ A.

(13.1)

А. А. Марковым и носит название принцип Маркова.

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

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

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

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

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

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

Конечно, во втором случае их поменьше, но это — разница типа разницы

ω и ω! в не-

стандартном анализе: одно бесконечно, а другое — невообразимо бесконечно.

Взаимосвязь между этими результатами не была очевидна ни самим Гёделю и Тар-

скому, ни остальным логикам до середины 40-х гг.

346

ГЛАВА 13. НЕПОЛНОТА И НЕФОРМАЛИЗУЕМОСТЬ

Теорема 13.1. (Тарский, 1928) Если в языке теории имеется отрица-

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

тинность неопределима по Тарскому.

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

Tr(x). Рассмотрим формулу B

Tr(sub(x, x)). Содержательно она

утверждает, что формула ложна на своем коде. Тогда по определению и

по свойству (13.1) имеем:

B(dBe) ⇔

Tr(sub(dBe, dBe)) ⇔

B(dBe).

Таким образом, пришли к противоречию.

Конец доказательства.

Далее возникает соблазн заявить, что (хотя бы в случае полной те-

ории) доказуемость является определением истинности по Тарскому и

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

она не может быть полна. Но Гёдель уловил важную ловушку, которая

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

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

∃x Proof(x, dAe) ⇔ A. (13.2)

Здесь

Proof(x, dAe) — формула, выражающая доказуемость. Сам Тар-

ский в эту ловушку не попался, а Гёдель показал, что такое свойство

на самом деле намного сильнее непротиворечивости и не может быть

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

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

тики, если только вся наша традиционная математика имеет смысл

Принцип рефлексии:

∃x Proof(x, d∃x Proof(x, dAe)e)ттт ∃x Proof(x, dAe).

(13.3)

То, что мы делаем такую оговорку о смысле математики, — также следствие резуль-

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

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

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

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

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

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

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

13.2. АКСИОМАТИЧЕСКОЕ ОПИСАНИЕ ВЫЧИСЛИМОСТИ

347

Содержательно это означает, что доказать доказуемость A то же самое,

что доказать само A.

Заметим,кстати,что определения истинности для подмножеств фор-

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

метике можно определить истинность для формул, имеющих менее

перемен кванторов формулой, имеющей n перемен кванторов.

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

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

ну аксиому, а как схему аксиом, утверждающих свойство индукции для

всех формул нашего языка.

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

13.1.1. Можно ли внутри теории множеств построить определение ис-

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

торым множеством?

13.1.2. А произвольным конечным множеством (возможно, своим для

каждого квантора)?

§ 13.2. АКСИОМАТИЧЕСКОЕ ОПИСАНИЕ ВЫЧИСЛИМОСТИ

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

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

посвященных данной науке (теории алгоритмов и вычислений.) Недо-

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

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

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

логическую суть от конкретной реализации. Это позволяет работать с

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

и типов данных

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

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

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

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

обхода.

Именно такая ситуация является практически наиболее распространенной и требует

теоретического осмысления.

348

ГЛАВА 13. НЕПОЛНОТА И НЕФОРМАЛИЗУЕМОСТЬ

Известно, что одним из основных свойств алгоритмов является их

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

ность исполнения машиной заложенной в нее программы.Но еще до по-

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

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

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

шина (универсальная), которая может смоделировать поведение и ре-

зультаты любой другой. А именно:

(Аксиома универсального алгоритма)

Имеется такой

алгоритм

, что для любого другого алгоритма

найдет-

ся его код

dϕe

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

ϕ(x)

Υ ([dϕe, x])

совпадают для любого

Возникает вопрос: а почему мы сразу не записали данное утвержде-

ние формулой? В частности, потому, что эта аксиома сама по себе огра-

ничивает набор возможных формализаций понятия алгоритма, которые

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

торые из принимаемых обычно по умолчанию вариантов.

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

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

сколько неудобно брать в качестве таких данных сами объекты. Лучше

пользоваться их структурами. Таким образом, лучше брать не универс

U, а множество кортежей над ним U

∗

. Из технических соображений к U

целесообразно добавить два логических значения ИСТИНА и ЛОЖЬ

(если их там не было).

Раз у нас есть множество кортежей, то нужно иметь элементарные

операции над кортежами. Практика и теория совместно показали, что

достаточно иметь одну двуместную операцию

APPEND

(см. (5.3)), при-

соединяющую свой второй аргумент к первому. Кроме того, нужны не-

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

извольные кортежи либо объекты, —

TAIL(x), выделяющая последний элемент кортежа x,

BODY(x), удаляющая из кортежа его хвост, т. е. последний элемент;

и четыре предиката:

ATOM

Проверяет, является ли x элементом исходного множества U.

SIMPLE

Проверяет, что x — кортеж из одного элемента.

13.2. АКСИОМАТИЧЕСКОЕ ОПИСАНИЕ ВЫЧИСЛИМОСТИ

349

TRUE

Проверяет, что x — атом, равный

ИСТИНА

NIL

Проверяет, что x — пустой кортеж [ ].

Пустой кортеж будем обозначать

NULL

. Через эти операции выражение,

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

щим образом:

Υ (APPEND(APPEND(NULL, dϕe), x)) (13.4)

Конечно, мы не будем писать в стиле (13.4); это выражение просто по-

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

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

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

ем:

Выражение

APPEND(∙∙∙(APPEND(NULL, t

), ∙∙∙), t

)

обо-

значается

, . . . , t

]

Термы, построенные из заданных известных алгоритмов и предикатов

при помощи перечисленных выше операций и имеющие лишь одну сво-

бодную переменную x, называются простейшими композициями алго-

ритмов. В компьютерах, как Вы знаете, исполняется только тот алго-

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

алгоритмов на язык самой машины. Программа-транслятор — универ-

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

кодирование алгоритмов. Из рассмотрения данного частного случая ко-

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

тоже должны быть алгоритмичны, а именно:

(Аксиома композиций)

Если имеется простейшая ком-

позиция

T (ϕ

, . . . , ϕ

)

переменных алгоритмов

, . . . , ϕ

то имеется алгоритм, выдающий для кортежа кодов

[dϕ

e, . . . , dϕ

код

dT (ϕ

, . . . , ϕ

Докажем

Предложение 13.2.1. Из двух принятых выше аксиом следует невоз-

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

Примечание для математиков. Такие кодирования алгоритмов являются главными

вычислимыми нумерациями (см. [16]), но мы не прикладывали никаких усилий к тому,

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

350

ГЛАВА 13. НЕПОЛНОТА И НЕФОРМАЛИЗУЕМОСТЬ

Доказательство. Рассмотрим выражение

ψ(x)

= [Υ ([x, x]) , NULL] .

Это — простейшая композиция, и она является алгоритмом. Пусть π —

ее код. Тогда Υ([π, π]) есть по определению универсального алгорит-

ма ψ(π). По определению ψ, последнее выражение записывается как

[Υ([π, π]), NULL]. Таким образом, мы получили, что кортеж Υ([π, π]) не

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

Значит, значение Υ([π, π]) не определено.

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

мализации понятий. Приняв две естественных аксиомы вычислимости,

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

ставлением понятия алгоритма. Мы должны рассматривать, как мини-

мум, частично определенные функции. Таким образом, слишком рано

заменив слова естественного языка на “точные” математические терми-

ны, мы можем зайти в тупик. Сначала уясняйте задачу и ситуацию, ми-

нимально пользуясь символами, а затем уже подставляйте действитель-

но точные, но подходящие к случаю, понятия.

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

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

начальных данных могут давать разные результаты. Поэтому мы везде

старались не использовать знак равенства, а говорить осторожнее: да-

ет тот же результат. Утверждение, что алгоритм

μ на входных данных a

может давать результат b, обозначается

μ(a) → b.

Равенство будем использовать лишь в том случае, если результат име-

ется, и только один.

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

функции может выглядеть как в следующей формуле:

Υ (APPEND(APPEND(NULL, dϕe), x)) → y ⇔ ϕ(x) → y. (13.5)

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

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

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

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

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