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

Теория доказательств (англ. proof theory) — раздел математической логики, в котором феномен математического доказательства сам становится объектом, например алгебры или арифметики. Доказательство обычно представляют как индуктивно возникающие структуры данных, начиная с простейших, таких как плоские списки, деревья, вплоть до гипотетических предельно сложных структур/машин которые строятся в соответствии с аксиомами и правилами вывода логических систем, имеющих соответствующие сложности/холистичности семантик.

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

Компьютеры являются срезом синтаксиса/семантики логики. В логике компьютеры воспринимаются платонически, как некий абсолют, в котором машина Тьюринга — одна из точек основания пирамиды, наряду с живой клеткой, а вершина — как некий Абсолютный Дух в стиле Гегеля. То есть принципиально различных типов машин и организмов бесконечно много.

Одной из моделей, целью которых был математических универсум были работы Готлоба Фреге или параллельная концепция так называемых «оснований математики» Гильберта. В неё наряду с теорией доказательств входили также теория моделей, аксиоматическая теория множеств, теорией рекурсии.

Теория доказательства может рассматриваться как ветвь философской логики, в которой основной интерес проективный потенциал или семантика теории доказательств (proof-theoretic semantics), и обратная задача нахождения/конструирования машин и пути в логическом универсуме межу исходными данными и доказательством.

История доказательств

(как профиль общего развития логики)

• Досократики — мысль воспринимает глубины существования (см., например, анализ Парменида у Хайдеггера).
• Сократ — мысль входит в жизнь человека.
• Платон — мысль образует мироздание.
• Аристотель — мысль структурируется в знание.
• Фома Аквинский — мысль помогает в познании Бога.
• Философия Нового Времени Локк — Кант — мысль становится универсальной индоктринацией.
• Джон Буль — алгебра логических выражений.
• С начала ХХ века логика становится одной из ведущих парадигм научных исследований Фреге, Гильберт, Гёдель.
• 60-е годы ХХ века — мощность машин и развитие программного обеспечение позволяет осознавать компьютер как область логического универсума.
• 80-е годы ХХ века — проект компьютеров пятого поколения, попытка создать компьютер способный понимать окружающий мир, передвигаться в логическом универсуме (то есть самосовершенствоваться). Вследствие основания на порочной технологии языка Пролог — полный провал и потеря интереса к логике.

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

Однако этот слой теории доказательств не был задействован. Сработал принцип теории доказательств: «Если теорема Пифагора заденет чьи-то интересы она будет опровергаться.» Академическая математика ушла в области недоступные контролю общества.

В компьютерах широко разрабатывались методы доказательств, вывода в символьных математических системах на основе Лисп-технологии — Maxima, Mathematica. В экспертных системах широко развилась системы доказательств на основе правил и онтологии. (В этой области произошёл выход в область стратегического планирования, но эти работы были закрыты для общества — военная тайна.)

В настоящее время, наряду с общим развитием логики, делаются попытки радикально разрешить отношение треугольника логика — биология — интеллект. Осуществляются проектные подходы:

• создание живой клетки/организма, синтетическая биология Крейга Вентера
• создание принципиально новой математики, создание математики мозга DARPA, запрос «brain», DARPA-Русский словарь, DARPA '2007
• синтез MEMS-система и насекомых DARPA Hybrid Insect MEMS (HI-MEMS), Animal Machine

Литература

• Б. В. Бирюков, В. Н. Тростников Жар холодных числ и пафос бесстрастной логики. — 1988.
• Фреге, Готлоб. Мысль: логическое исследование.
• Фреге, Готлоб. Основоположения арифметики. Логико-математическое исследование о понятии числа. — Томск: «Водолей», 2000.
• Фреге, Готлоб. Смысл и значение.
• Фреге Г. О существовании. Диалог с Пеньером.

См. также

• Дедукция

Ссылки