О некоторых семантических дефектах в логике интеллектуальных систем

Размещено на http://www.allbest.ru/

О НЕКОТОРЫХ СЕМАНТИЧЕСКИХ ДЕФЕКТАХ В ЛОГИКЕ ИНТЕЛЛЕКТУАЛЬНЫХ СИСТЕМ

Александр Зенкин

Вычислительный Центр РАН им. А.А. Дородницына

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

В работе показано, что в некоторых случаях приведение формул к сколемовской предваренной форме приводит к фатальному искажению семантики их содержательных интерпретаций - математических моделей реальных объектов. В ряде важных случаев, в аксиоматической теории множеств имеются теоремы, в которых по тем или иным причинам отсутствует явная формулировка необходимых условий их доказательства. С формальной точки зрения такие теоремы неопровержимы, однако, при восстановлении необходимых условий такие теоремы становятся либо ложными, либо недоказуемыми. Как правило, средств самой формальной системы недостаточно, для идентификации подобных дефектов. На примере традиционного доказательства Теоремы Кантора о несчетности континуума показано, что существуют две, принципиально различные, версии метода Reductio ad Absurdum (RAA). В классическом исчислении предикатов реализуется специфическая RAA-версия, характерная для диагонального метода Кантора, что исключает корректное применение этого метода для формального доказательства большинства теорем математической физики. Неучет указанных дефектов исчисления предикатов в рамках ИИ-систем верификации математических моделей сложных систем может привести к непредсказуемым и нежелательным (катастрофическим) последствиям в процессе эксплуатации соответствующих реальных объектов.

1. Интеллектуальные системы верификации математических доказательств.

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

К числу таких «продвинутых» ИИ-систем относятся, например, проекты QED, Mizar и др.[1]. Вот как определяет цели и задача проекта QED один из его разработчиков, ведущий сотрудник фирмы Intel, John Harrison [2]: «Целью проекта является создание единой, распределенной базы знаний, в которой представлено все апробированное математическое знание. Создание такой системы требует совместной работы многих математиков, информатиков, ИИ-специалистов, целых исследовательских групп, агентств, университетов и корпораций. Эта система предназначена для обслуживания стратегических потребностей математики, науки, технологий, промышленности и образования».

Естественно, что теоретической базой разработки таких ИИ-систем является исчисление предикатов. Очевидно поэтому, что любые дефекты в исчислении предикатов могут приводить к непредсказуемым последствиям при практическом функционировании сложных финансовых, военных, космических, ядерных и т.п. объектов, математическое обеспечение которых сертифицировано с помощью дефективных «верификаторов».

2. «Сколемизация» формальных выражений и искажение семантики их неформальных прототипов.

Как известно, (простая) непротиворечивость исчисления предикатов была доказана Гильбертом и Аккерманом в 1938 г. [3] Однако, непротиворечивость и семантическая адекватность формальной системы своему неформальному прототипу - вещи существенно различные.

Приведу несколько примеров.

В работах [4,5] описан метод супер-индукции - новый (т.е. неизвестный в современной мета-математике) метод доказательства общих утверждений вида nP(n), являющийся естественным обобщением метода полной математической индукции. Этот метод был открыт с помощью когнитивной компьютерной графики (ККГ) и основан на доказательстве условных утверждений (так называемых ЕА-Теорем) следующего, довольно необычного вида.

ЕА-ТЕОРЕМА. Если существует натуральное n*, для которого выполняется предикат Q(n*), то для всех n>n* выполняется предикат P(n), или в символической форме:

n*Q(n*) n > n* P(n),(1)

где P(n) - произвольный арифметический предикат, а Q(n) - специальный арифметический предикат, определенным (заранее неизвестным) образом зависящий от P.

Ю.В. Матиясевич предложил следующую, более корректную с точки зрения исчисления предикатов, приведенную сколемовскую форму выражения (1):

n*n>n* [Q(n*) P(n)]].(1а)

Однако, в процессе (приватной) дискуссии мы пришли к выводу, что выражения (1) и (1а) имеют существенно различную семантику и операциональное содержание: в выражении (1) акцент делается на условии «если существует такое n*, что Q(n*) …», причем существование такого n* не гарантируется; в выражении (1а) вопрос о существовании «критического» числа n* вообще игнорируется. Это означает, что стандартная «сколемизация» формальных выражений в рамках ИИ-систем формализации математики (типа QED-системы) может, в общем случае, привести к существенному (и неконтролируемому) искажению семантики содержательных математических моделей управления сложными динамическими системами и повлечь за собой непредсказуемые последствия.

3. От сокрытия необходимых условий формальных доказательств к мифологизации истины.

Как известно, в математике отсутствие явной формулировки необходимых условий доказательства является грубой ошибкой, которая может привести к ложным выводам. Например, Теорема Пифагора a² = b² + c² является, в общем случае, просто неверной, если в ее доказательстве опущено условие о том, что соответствующий треугольник ABC является прямоугольным. Но возможна и обратная ситуация, когда отсутствие явной формулировки необходимых условий некоторого доказательства делает такое доказательство формально «безупречным», а соответствующую «теорему» - убедительной и неопровержимой. Однако, при явном учете «опущенных» необходимых условий такая «теорема» становится либо ложной, либо просто недоказуемой.

С этой точки зрения, в рамках современной теории множеств (из которой, по утверждению Бурбаки, «можно вывести почти всю математику» [5]) сложилась довольно странная ситуация вокруг такого фундаментального понятия философии, логики и математики, как понятие актуальной бесконечности (АБ). Так, например, один из выдающихся современных мета-математиков, С. Феферман [6] пишет: «понятие актуальной бесконечности не используется в современной аксиоматической теории множеств, хотя некоторые аксиомы обосновываются принятием концепции актуальной бесконечности». В частности, его собственная новейшая OST-система («Операциональная Теория Множеств») «определенно включает в себя некоторую форму существования актуальной бесконечности». Другой известный мета-математик W.Hodges (бывший главный редактор журнала The Bulletin of Symbolic Logic) выражается более определенно [8]: «Аксиомы Цермело-Френкеля неявно включают в себя актуальную бесконечность. Доказательство Теоремы Кантора зависит от принятия актуальной бесконечности». Что значит неявное включение «философской» концепции АБ в аксиоматику формальной системы и зависимость формального доказательства от принятия неформальной концепции АБ, нигде не раскрывается. Однако, после этих признаний, W.Hodges делает довольно странный с точки зрения математики вывод: это «принятие» актуальной бесконечности «является фактом общеизвестным и общепринятым», а потому «нет никакой необходимости каждый раз явно выписывать этот необходимое условие в начале каждого доказательства».

На языке математики, этот очевидный «бурбакизм» (термин В.И. Арнольда [9,10]) означает: сегодня каждый школьник знает, что «прямоугольность» треугольника ABC является необходимым условием доказательства Теоремы Пифагора, поэтому «нет никакой необходимости каждый раз явно выписывать (да и вообще упоминать) это условие».

Последствия подобной разновидности «бурбакизации математики» анализируются в работах [11,12,13], где детально рассматривается вопрос о связи понятия актуальной бесконечности с вопросом о необходимых условиях доказательства Теоремы Кантора о несчетности континуума. Показано, что традиционное доказательство этой Теоремы со времен Кантора и до наших дней никогда не содержало в явном виде, по крайней мере, двух необходимых условий. Первое условие связано с актуальностью всех бесконечных множеств, фигурирующих в канторовском доказательстве. А именно, традиционная формулировка Теоремы Кантора в форме «Континуум - несчетен» не содержит условия, что континуум - актуально бесконечен. Это условие является необходимым условием традиционного канторовского («диагонального») доказательства, поскольку в противном случае, т.е. если континуум потенциально-бесконечен, то диагональный метод Кантора становится «недееспособным», а Теорема Кантора - недоказуемой. Поэтому, с точки зрения математики, традиционная формулировка Теоремы Кантора в форме «Континуум - несчетен» является просто неверной и должна быть переписана в следующей условной форме: «Если континуум актуально-бесконечен, то он - несчетен». Как известно, в математике явная формулировка необходимых условий любого доказательства, во-первых, является первейшим требованием корректности доказательства, а, во-вторых, не способна лишить такое доказательство его легитимности. Однако, как доказано в [11,12], в случае явной формулировки указанного необходимого условия диагональный метод Кантора хотя и «работает» безупречно, но само «диагональное» доказательство, с точки зрения классической логики, не доказывает целевого утверждения о несчетности континуума.

Второе необходимое условие канторовского доказательства (так называемый Постулат Кантора-Ходжеса, суть которого состоит в том, что для индексации счетного (согласно допущению доказательства «от противного», см. ниже) списка элементов континуума необходимо использовать все элементы счетного множества N={1,2,3, …} и категорически запрещается использовать не все натуральные числа, например, элементы счетного множества {2,4,6, …}, т.к. в последнем случае доказательство Кантора теряет силу) вообще имеет телеологический характер, т.е., согласно Кронекеру, не имеет к математике никакого отношения.

Как известно, и Теорема Кантора и ее «диагональное» доказательство фигурируют во всех современных теориях множеств (кроме, естественно, интуиционистских), однако без явной формулировки (даже без упоминания) указанных необходимых условий этого доказательства. Последнее и обеспечивает кажущуюся неопровержимость Теоремы Кантора о несчетности континуума. Явная формулировка и (алгоритмическое) использование указанных необходимых условий приводит к тому, что Теорема Кантора либо становится ложной, либо недоказуемой.

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

4. О двух версиях метода reductio ad absurdum («от противного»)

Рассмотрим теорему Кантора о мощности множества-степени [14] и ее традиционное `диагональное' доказательство в его современной ZF-форме [15].

Здесь и далее P(X) - множество-степень, и |X| - мощность произвольного множества X, и, для краткости, RAA = Reductio ad Absurdum, ДМК = Диагональный Метод Кантора, АД-элемент = Анти-Диагональный элемент, порождаемый применение ДМК.

ТЕОРЕМА-1 КАНТОРА (1890). |X| < |P(X)|.

ДОКАЗАТЕЛЬСТВО (с помощью RAA-метода). Очевидно, что |X| |P(X)|.

Допустим, что отображает X на P(X). Определим новое подмножество X* множества X следующим образом: X*={x X | x (x)}. Тогда X* X, и если X* = (y) для некоторого y X, то y X* y (y) y X* и y X* y (y) y X*. Последнее невозможно. Ч.Т.Д.

Как справедливо отмечает Есенин-Вольпин, (см. его комментарий в [15], стр.172), основным этапом доказательства Кантора является доказательство следующего утверждения: “для любого X не существует взаимно однозначного отображения X на P(X)”. К сожалению, это очень важное замечание Есенина-Вольпина не было оценено по достоинству и не имело продолжения. Мы попытаемся проанализировать некоторые следствия этого комментария.

Однако, прежде, чем приступить к анализу канторовского доказательства, напомню некоторые фундаментальные утверждения современной теории множеств [14-16], которые будут использованы ниже.

ОПРЕДЕЛЕНИЕ 1. Множество, Z, является бесконечным, если и только если оно эквивалентно своему собственному подмножеству.

ЛЕММА 1. Если разность между количествами элементов двух бесконечных множеств, скажем, Z₁ и Z₂ является конечной, то множества Z₁ и Z₂ эквивалентны, т.е. |Z₁| = |Z₂|.

ОПРЕДЕЛЕНИЕ 2. Два бесконечных множества, скажем, Z₁ и Z₂ эквивалентны, т.е. |Z₁| = |Z₂|, если и только если существует 1-1-соответствие между Z₁ и Z₂.

ЛЕММА 2. Если не существует 1-1- соответствия между элементами множеств Z₁ и Z₂, то множества Z₁ и Z₂ не эквивалентны, т.е. |Z₁| |Z₂|.

Теперь, принимая во внимание комментарий Есенина-Вольпина, перепишем Теорему-1 Кантора и ее традиционное доказательство в следующей семантически эквивалентной форме.

ТЕОРЕМА-2 КАНТОРА (1873, 1890). Не существует 1-1-соответствия между X и P(X) для любого X.

ДОКАЗАТЕЛЬСТВО (с помощью RAA-метода). Допустим, что существует 1-1-соответствие , которое отображает X на P(X), т.е. YP(X)[Y]. Определим новое подмножество: X*={x X | x (x)}. Тогда X*P(X), но Y[X*Y], т.е. X*. Противоречие. Ч.Т.Д.

ТЕОРЕМА-3 КАНТОРА (1890). |X| < |P(X)|.

ДОКАЗАТЕЛЬСТВО. Из Теоремы 2 и Леммы 2 следует |X| |P(X)|, откуда, в силу очевидного неравенства |X| |P(X)|, следует строгое неравенство |X| < |P(X)|. Ч.Т.Д.

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

1. Имеется некоторое общее гипотетическое утверждение x P(x).

2. Устанавливается факт (если это удается), что x* P(x*).

3. Из этого единственного факта следует, что [x P(x)].

СЛЕДСТВИЕ-1. Для того, чтобы опровергнуть общее утверждение, xP(x), достаточно единственного контр-пример x *, для которого имеет место P(x*).

СЛЕДСТВИЕ-2. Мощность множества всех возможных контр-примеров, x, для которых P(x), не принимается во внимание и не используется в рамках доказательства методом контр-примера.

Рассмотрим два примера реального применения метода контр-примера в математике.

ПРИМЕР 1. В XVIII веке Эйлер сформулировал следующее общее утверждение.

ГИПОТЕЗА ЭЙЛЕРА. Для любого показателя r 3 диофантово уравнение, n^r = n₁^r + n₂^r + n₃^r + … + n_s^r, не имеет решений в натуральных числах, если s < r.

В течение более 200 лет никому не удавалось ни доказать, ни опровергнуть эту Гипотезу. Только в 1967 группа американских математиков с помощью мощного компьютера открыла... всего только один контр-пример [17], 144⁵ = 27⁵ + 84⁵ + 110⁵ + 133⁵, где r = 5, s = 4, т.е. s < r. Этот единственный контр-пример доказал, что Гипотеза Эйлера - ложна. Таким образом, для того, чтобы опровергать общее утверждение, действительно оказалось достаточно единственного контр-примера (Следствие 1). И тот факт, что множество таких контр-примеров может быть бесконечным не играет в таком опровержении никакой роли (Следствие 2). Другими словами, опровержение общего утверждения с помощью данного контр-примера и вопрос о фактическом количестве таких контр-примеров, т.е. вопрос о мощности множества всех возможных контр-примеров, являются абсолютно различными, независимыми проблемами.

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

ПРИМЕР 2. Согласно допущению доказательства Теоремы-2 Кантора, имеется 1-1-соответствие , которое отображает X на P(X), т.е. {B:} все элементы множества P(X) принадлежат данному отображению . Затем Кантор определяет новое подмножество X*={x X | x (x)} такое, что X*P(X), но X*. Это означает что X*P(X)[X*], т.е. {B:} не все элементы множества P(X) принадлежат данному .

Таким образом, с точки зрения классической логики, канторовский АД-элемент X* является контр-примером, опровергающим общее утверждение B.

Эти два примера показывают, что есть две, существенно различные версии метода контр-примера: в первой версии (назовем ее классической версией), контр-пример отыскивается в множестве всех возможных реализаций данной гипотезы; во второй версии (назовем ее ДМК-версией), контр-пример алгоритмически дедуцируется из той гипотезы, которую этот контр-пример должен опровергнуть.

Заметим, что ДМК-версия является отличительной особенностью именно диагонального метода Кантора. Этот факт может быть сформулирован в следующей общей форме.

УТВЕРЖДЕНИЕ-1. Знаменитый Диагональный Метод Кантора (в любой мета-математической реализации этого метода) является специальным случаем метода контр-примера, где сам контр-пример не отыскивается в множестве всех возможных реализаций данного общего утверждения, а алгоритмически дедуцируется из того общего утверждения, которое этот контр-пример и призван опровергнуть.

Докажем теперь две теоремы, выявляющие некоторые "скрытые" логические особенности диагонального метода Кантора.

ТЕОРЕМА 1. Вывод Кантора |X| < |P(X)| противоречит Лемме 1 [12,13,18-21].

ДОКАЗАТЕЛЬСТВО. Следуя Кантору, допустим, что отображает X на P(X), т.е. |X| = |P(X)|. Представим множество P(X) в виде суммы, P(X) = P₁+P₂ где P₁ есть множество всех элементов из P(X), которые действительно принадлежат , и P₂ - дополнение к P₁ в P(X), т.е. P₂ = P(X) - P₁. В силу RAA-допущения, |P₁|=|X|, и P₂ - пустое множество.

Для данного отображения Кантор определяет X*={x X | x (x)} так, что X*P(X), но X*, т.е. X* P₁. Следовательно, X* P₂.

С точки зрения классической логики и классической математики, канторовский АД-элемент X* является контр-примером, опровергающим общее утверждение B = «данное отображение включает все элементы из P(X)». Из доказанной ложности утверждения B (доказанной именно с помощью ДМК-версии метода контр-примера) следует (по правилу modus tollens), что RAA-допущение, |X| = |P(X)|, ложно. На основании Леммы 2, вместе с очевидным неравенством |X| |P(X)|, это ведет к заключительному утверждению Кантора |X| < |P(X)|.

Таким образом, с точки зрения формальной логики, RAA-доказательство Кантора - безупречно и неопровержимо. Однако, очевидно, что для данного (фиксированного) отображения , диагональный метод Кантора способен «породить» единственный, уникальный элемент X* множества P(X), не принадлежащий данному . Это означает, что заключение Кантора |X|<|P(X)| основано на том факте, что бесконечное множество P(X) имеет на один элемент больше, чем бесконечное множество X, т.е. |P₂| = 1. Очевидно, что такое теоретико-множественное "основание" для канторовского вывода |X|<|P(X)| фатально противоречит теоретико-множественной Лемме 1, согласно которой из равенства |P(X)| - |X| =1 следует |X| = |P(X)|. Ч.Т.Д.

ТЕОРЕМА 2. Неравенство Кантора |X|<|P(X)| недоказуемо [12,13,18-21]

ДОКАЗАТЕЛЬСТВО. Единственным поводом для утверждения |X|<|P(X)|, является Теоремоа-1 Кантора. Поэтому для доказательства Теоремы 2 достаточно доказать, что традиционное доказательство Кантора не доказывает утверждения |X|<|P(X)|.

С этой целью, рассмотрим снова традиционное доказательство Кантора.

ТЕОРЕМА КАНТОРА. |X| < |P(X)|.

ДОКАЗАТЕЛЬСТВО 1. Допустим, что отображает X на P(X), т.е. |X| = |P(X)|.

Представим множество P(X) в виде суммы: P(X) = P₁₁+P₁₂, где P₁₁ - множество всех элементов из P(X), которые действительно принадлежат , и P₁₂ - дополнение к P₁₁ в P(X), т.е. P₁₂ = P(X) - P₁₁. В силу RAA-допущения, |P₁₁|=|X|, и P₁₂ = .

Для данного Кантор определяет новый элемент X*={xX | x(x)}, который не принадлежит . Но теперь, мы допускаем, что изменяя исходное отображение (без изменения, однако, количества элементов из P(X) в исходном отображении ), диагональная процедура Кантора способна произвести бесконечное множество новых АД-элементов из P(X), не принадлежащих исходному отображению , т.е. принадлежащих дополнению P₁₂. Последнее означает, что теперь истинная мощность множества P(X) определяется количеством элементов дополнения P₁₂, то есть |P(X)| = |P₁₂|.

При этом возможны следующие два случая.

(i) |P₁₂| = |X|. Тогда |P(X)| = |P₁₁ + P₁₂| =|X|, и поэтому опровергнуть RAA-допущение |X| = |P(X)| невозможно, с точки зрения аксиоматической теории множеств.

(ii) |P₁₂| > |X|. Однако, поскольку доказательство Кантора пока еще не закончено, само существование мощности большей, чем |X|, пока не доказано, а поэтому гипотетическое утверждение |P₁₂| > |X| должно быть доказано. Это может быть сделано единственным способом - посредством ДМК, т.е. нужно теперь доказать исходную Теорему Кантора с новым символом P₁₂ вместо старого символа P(X).

ТЕОРЕМА КАНТОРА. |X| < |P₁₂|.

ДОКАЗАТЕЛЬСТВО 2. Допустим, что ₁ отображает X на P₁₂, т.е. |X| = |P₁₂|. Применение ДМК к ₁ порождает бесконечное множество элементов из P₁₂, которые не принадлежат ₁. Представим множество P₁₂ в виде суммы: P₁₂ = P₂₁+P₂₂, где P₂₁ - множество всех элементов из P₁₂, которые действительно принадлежат ₁, и P₂₂ - дополнение к P₂₁ в P₁₂. В силу RAA-допущения, |P₂₁|=|X|, и P₂₂ содержит все АД-элементы, порождаемые применением ДМК к ₁. Последнее означает, что теперь истинная мощность P₁₂ определяется количеством элементов дополнения P₂₂, то есть |P₁₂| = |P₂₂|.

Рассмотрим следующие два случая.

(i) |P₂₂| = |X|. Тогда |P₁₂| = |P₂₁ + P₂₂| =|X|, и поэтому невозможно опровергнуть RAA-допущение, |X| = |P₁₂|, с точки зрения аксиоматической теории множеств.

(ii) |P₂₂| > |X|. Однако, поскольку доказательство Кантора пока еще не закончено, само существование мощности, которая больше, чем |X|, пока не доказано, а поэтому гипотетическое утверждение |P₂₂| > |X| должно быть доказано. Это может быть сделано единственным способом - посредством ДМК, т.е. нужно теперь доказать исходную Теорему Кантора с новым символом P₂₂ вместо старого символа P₁₂.

И так далее до бесконечности.

Таким образом, традиционное канторовское доказательство Теоремы о мощности множества-степени, с теоретико-множественной точки зрения (!), или не способно опровергнуть RAA-допущение, |X| = |P(X)|, или сводится к бесконечной системе "вложенных" доказательств исходной Теоремы Кантора с последовательной заменой исходного символа P(X) символами P₁₂, P₂₂, P₃₂, …, т.е. сводится к следующему нефинитному, тавтологическому, и довольно бессмысленному "рассуждению" (здесь D_i = «требуется доказать, что |X| < |P_i2|»): D₁ D₂ D₃ … (*)

Очевидно, что до тех пор, пока потенциально бесконечное "рассуждение" (*) не закончено, исходное RAA-допущение |X| = |P(X)| канторовского RAA-доказательства неопровержимо с теоретико-множественной точки зрения, и, следовательно, утверждение Кантора |X| < |P(X)| - недоказуемо. Ч.Т.Д.

Итак, существуют две, принципиально различные версии метода контр-примера. Традиционное доказательство Теорем 1 и 2 Кантора проводится методом RAA и основано на явном использовании ДМК-версии метода контр-примера. Ключевым моментом канторовского RAA-доказательства является (алгоритмическое) доказательство истинности некоторого следствия (В= “X*P(X)[X*]”) данного RAA-допущения (А = “|P(X)|=|X|”), которое (это следствие) дедуцируется из данного RAA-допущения. Ключевым моментом классического RAA-метода является доказательство ложности некоторого формального следствия RAA-допущения, причем это доказательство ложности основано не на методе контр-примера, а на законе противоречия и проводится независимо от дедуктивного вывода данного формального следствия из данного RAA-допущения (иначе - круг в доказательстве). Это означает, что существуют две различные версии метода RAA: ДМК-версия, на которой основано традиционное доказательство Кантора, и классическая версия, которая используется в подавляющем большинстве реальных математических доказательств.

В современной мета-математике RAA-метод (так называемое правило «введения отрицания») формулируется следующим образом [16]: если Г, А |- В и Г, А |- В, то Г |- А.(П-1)

Нетрудно показать, что данная формулировка RAA-метода является формализацией именно канторовской ДМК-версии. С другой стороны, адекватная формулировка классической версии RAA-метода имеет вид: если Г, А |- В и Г |- В, то Г |- А.(П-2)

Это означает, что ИИ-системы, использующие мета-математическую версию (П-1) RAA-метода, могут приводит к результатам, существенно искажающим семантику исходных математических моделей функционирования реальных сложных систем.

5. Основной вывод.

Таким образом, в основаниях современной мета-математики (так называемой «теории доказательства»), а именно, в классическом исчислении предикатов и аксиоматической теории множеств имеется целый ряд формальных дефектов, которые приводят к ложным, как формальным, так и эпистемологическим, выводам. Неучет указанных дефектов исчисления предикатов в рамках ИИ-систем верификации математических моделей сложных систем может привести к непредсказуемым, неконтролируемым и нежелательным (катастрофическим) последствиям в процессе эксплуатации соответствующих реальных объектов и сложных систем.

автоматизация математический теорема сколемизация

Литература

1. J.Wright, J.Grundy, and J.Harrison, editors. Theorem Proving in Higher Order Logics. - 9th International Conference, TPHOLs'96, vol. 1125 of Lecture Notes in Computer Science, Turku, Finland, August 1996. Springer.

2. John Harrison, High-Level Verification using Theorem Proving and Formalized Mathematics. - CADE 17, Springer LNCS 1831, pp. 1-6, 2000.

3. Д.Гильберт, В.Аккерман, Основы теоретической логики. - Москва: ИЛ, 1947.

4. А.А.Зенкин, Супериндукция: новый метод доказательства общих математических утверждений с помощью компьютера. - Доклады РАН, том 354, No. 5, 587 - 589 (1997).

5. A.A.Zenkin, Super-Induction Method: Logical Acupuncture of Mathematical Infinity. - Proceedings of the XX World Congress of Philosophy, Boston, Massachusetts, 1998. Section "Logic and Philosophy of Logic".

6. Н.Бурбаки, Теория множеств. - Москва: МИР, 1965

7. S.Feferman, In the light of logic. - Oxford University Press, 1998.

8. W.Hodges, An editor recalls some hopeless papers. - The Bulletin of Symbolic Logic, 1998, v. 4, p. 1-16.

9. В.И.Арнольд, Антинаучная революция и математика. - Вестник РАН, 1999, No. 6, 553-558

10. А.А.Зенкин, "Научная контр-революция в математике". - Независимая газета, 19-09-02.

11. А.А.Зенкин, "Infinitum Actu Non Datur". - Вопросы философии, 2001, no.9, 157-169.

12. A.A. Zenkin, Scientific Intuition Of Genii Against Mytho-"Logic" Of Transfinite Cantor's Paradise. - International Symposium «Philosophical Insights into Logic and Mathematics (PILM 2002)», 2002, Nancy, France. Proceedings, pp. 141-148.

13. А.А.Зенкин, Принцип разделения времени и анализ одного класса квазифинитных правдоподобных рассуждений (на примере теоремы Г.Кантора о несчетности). - Доклады РАН, том 356, no 6,733-735(1997).

14. Георг Кантор, Труды по Теории Множеств, Москва, «Наука», 1985.

15. Пол Дж. Коэн. Теория множеств и континуум-гипотеза. - М.: МИР, 1969.

16. С.Клини, Введение в метаматематику. - М.: ИЛ, 1957.

17. L.J. Lander, T.R. Parkin, A counter example to Euler's sum of power conjecture. - Math. Comp., 21, 101-103 (1967).

18. А.А.Зенкин, Ошибка Георга Кантора. - Вопросы философии, 2000, № 2, 165-168.

19. А.А.Зенкин, О Логике "правдоподобных" мета-математических заблуждений. - Труды Всероссийской Конференции “Научная Сессия МИФИ-2004 ”, Москва, МИФИ, 2004, стр. 182-183.

20. А.А.Зенкин, Априорные логические утверждения с нулевой онтологией. - В Сб. “Математика и Опыт”, (ред. А.Г. Барабашев), Издательство МГУ, 2004, стр. 423-434.

21. A.A. Zenkin, A Linear Goedel's Numbering Of Multi-Modal Texts. - The Bulletin of Symbolic Logic, 2002, Vol. 8, No. 1, p. 180.

Размещено на Allbest.ru