Доказательств Теория

Раздел математич. логики, посвященный исследованию понятия доказательства в математике, приложениям этого понятия в различных разделах науки и техники. Доказательство в широком смысле этого слова есть способ обоснования истинности того или иного суждения. Степень убедительности доказательства решающим образом зависит от средств, используемых для обоснования истинности. Напр., в точных науках выработаны определенные условия, при выполнении к-рых сообщаемый экспериментальный факт может считаться доказанным (необходима устойчивая воспроизводимость эксперимента, отчетливое описание методики эксперимента, его точности, применяемого оборудования и т. п..). В математике, для к-рой характерен аксиоматический метод исследования, средства доказательства достаточно четко определились уже на раннем этапе ее развития. Доказательство фигурирует в математике как последовательное выведение одних суждений из других, причем способы этого выведения допускают точный анализ. Истоки Д. т. можно проследить со времен античности (дедуктивный метод рассуждения в элементарной геометрии, силлогистика Аристотеля и др.), но современный этап ее развития начинается в конце 19 в.- начале 20 в. под влиянием работ Г. Фреге (G. Frege), Б. Рассела (В. Russell) и А. Уайтхеда (A. Whitehead), Э. Цермело (Е. Zermelo) и, в особенности, Д. Гильберта (D. Hilbert). В это время в теории множеств Г. Кантора (G. Cantor) были обнаружены антиномии, поставившие под сомнение достоверность даже простейших рассуждений с произвольными множествами. Л. Брауэр (L. Brouwer) подверг весьма серьезной критике нек-рые классич. способы доказательства существования объектов в математике и предложил радикальную перестройку математики в духе интуиционизма. Вопросы оснований математики приобрели особую актуальность. Д. Гильберт предложил выделить часть практич. математики, так наз. финитную математику, не вызывающую возражений как с точки зрения появления антиномий, так и с точки зрения интуиционистской критики. В рамках финитной математики к рассмотрению допускаются лишь конструктивные объекты, напр, натуральные числа, и лишь такие способы рассуждений, к-рые согласуются с абстракцией потенциальной осуществимости и не привлекают абстракции актуальной бесконечности. В частности, ограничивается использование закона исключенного третьего. В финитной математике никаких антиномий не обнаружено и нет оснований их ожидать. С философской точки зрения способы рассуждения в финитной математике значительно более удовлетворительным образом отражают конструктивные процессы реальной действительности, чем в общей теоретико-множественной математике. Идея Д. Гильберта состояла в том, чтобы обосновать все основные разделы классич. математики, оставаясь на твердой почве финитной математики. С этой целью Д. Гильберт предложил метод формализации, являющийся одним из основных методов Д. т. В общих чертах метод формализации состоит в следующем: формулируется логико-математич. язык (предметный язык) L, в терминах к-рого суждения данной математич. теории Тзаписываются в виде формул. Далее описывается нек-рый класс Аформул L, называемых аксиомами теории, и описываются вывода правила, с помощью к-рых можно переходить от одних формул к другим. Для аксиом и правил вывода употребляется общий термин — постулаты. Заданием постулатов определяется формальная теория (в другой терминологии — исчисление) Т*. Формулы, получаемые из аксиом формальной теории по ее правилам вывода, наз. выводимыми, или доказуемыми, в данной теории. Сам процесс вывода может быть при этом оформлен в виде дерева вывода (см. Вывода дерево). Исчисление Т* представляет особенный интерес по отношению к содержательной математич. теории Т, если аксиомы Т* являются записями истинных суждений Т, а правила вывода ведут от истинных суждений к истинным. В этом случае Т* можно рассматривать как уточненный фрагмент теории Т, а понятие вывода в Т* можно рассматривать как уточнение неформальной идеи доказательства в теории Т, по крайней мере в рамках, формализованных исчислением Т*. Таким образом, при построении исчисления Т* нужно предварительно уметь определять, какие постулаты считать пригодными с точки зрения теории Т. Это, однако, не означает, что необходимо уже иметь развитую семантику теории Т:здесь можно использовать практич. навыки, включать в число постулатов наиболее часто употребляющиеся или наиболее интересные в теоретич. отношении факты и т. п. Точный характер описания выводов исчисления Т* позволяет применять для их исследования математич. методы и таким образом судить о содержании и свойствах теории Т. В Д. т. выработаны стандартные приемы формализации содержательных математич, теорий. Аксиомы и правила вывода исчислений обычно делятся на логические и прикладные. Логич. постулаты служат для получения высказываний, истинных независимо от формализуемой теории уже в силу своей формы. Такие, постулаты определяют логику формальной теории и оформляются в виде высказываний исчисления или предикатов исчисления (см. также Логические исчисления, Математическая логика, Интуиционизм, Конструктивная логика, Строгой импликации исчисление). Прикладные постулаты служат для описания истин, относящихся к особенностям данной математич. теории. Напр., в аксиоматич. теории множеств — это выбора аксиома, в элементарной арифметике — схема аксиом индукции (см. Математическая индукция), в интуиционистском анализе — бар-индукция. Гильбертову программу обоснования математики можно описать следующим образом. Можно надеяться, что всякую, даже весьма сложную и абстрактную математич. теорию Т(такую, напр., как теория множеств), можно в ее существенных частях формализовать в виде исчисления Т*, причем формулировка самого исчисления требует лишь финитной математики. Далее, анализируя выводы Т* чисто финитными средствами, можно пытаться установить непротиворечивость Т* и, следовательно, установить отсутствие антиномий в Т, по крайней мере в той ее части, к-рая отражена в постулатах Т*. Для обычных методов формализации отсюда непосредственно следует, что нек-рые простейшие суждения (в терминологии Гильберта — реальные суждения) выводимы в Т*, только если они истинны в финитном смысле. Первоначально надежда состояла в том, что в виде исчисления, формулируемого финитным образом, удастся описать практически всю классич. математику, а затем финитно же доказать ее непротиворечивость. Невыполнимость этой программы в целом была установлена в 1931 К. Гёделем (К. Godel), к-рый показал, что при нек-рых естественных предположениях непротиворечивость исчисления Т* невозможно доказать даже мощными средствами, формализуемыми в T*. Тем не менее исследование различных формальных исчислений остается важнейшим методом в основаниях математики. Во-первых, представляет интерес построение исчислений, отражающих существенные разделы современной математики и построенных в расчете на непротиворечивость, даже если непротиворечивость таких исчислений и нельзя доказать в настоящее время убедительным для всех математиков способом. Примером такого рода исчисления является система теории множеств Цермело — Френкеля, в к-рой могут быть выведены практически все результаты, полученные в современной теоретико-множественной математике. Доказательства невыводимости в этой теории ряда фундаментальных гипотез, полученные в предположении; непротиворечивости теории (см. Аксиоматическая теория множеств, Вынуждения метод), свидетельствуют о независимости этих гипотез от применяемых в математике теоретико-множественных принципов. Это, в свою очередь, можно рассматривать как подтверждение той точки зрения, что существующих представлений- недостаточно для доказательства или опровержения рассматриваемых гипотез. Именно в этом смысле П. Коэн (P. Cohen) установил независимость континуум-гипотезы Г. Кантора. Во-вторых, широко изучается класс исчислений, непротиворечивость к-рых можно установить финитными средствами. Так, К. Гёдель в 1932 предложил погружающую операцию, перерабатывающую формулы, доказуемые в классическом арифметич. исчислении, в формулы, доказуемые в интуиционистском арифметич. исчислении. Если последнее считать непротиворечивым (напр., в силу его естественной финитной интерпретации), то отсюда следует непротиворечивость и классического арифметич. исчисления. Наконец, перспективным является исследование средств более широких, чем традиционный финитизм Д. Гильберта, но в то же время достаточно удовлетворительных с нек-рой точки зрения. Так, оставаясь в рамках потенциальной осуществимости, можно использовать так наз. общие индуктивные определения. Это позволяет применять полуформальные теории, в к-рых некоторые из правил вывода имеют бесконечное (но конструктивно порожденное) множество посылок, и перенести в финитную математику многие семантические результаты. К этому направлению относятся результаты П. С. Новикова (1943), установившего непротиворечивость классич. арифметики с использованием эффективных функционалов конечного типа, К. Спектора (С. Spector, 1961), доказавшего непротиворечивость классич. анализа с помощью расширения естественных интуиционистских средств доказательства на интуиционистские эффективные функционалы конечного типа, А. А. Маркова (1971) по конструктивной семантике, использующие общие индуктивные определения. Кроме того, ряд важных проблем, относящихся к исчислениям, можно рассматривать и вне связи с основаниями математики. Сюда относятся вопросы о полноте и разрешимости формальных теорий, вопрос о независимости нек-рых утверждений от данной формальной теории и др. В такой ситуации нет необходимости ограничиваться в рассуждениях определенными средствами и можно развивать Д. т. как обычную математич. теорию, пользуясь любыми математич. средствами доказательства, убедительными для исследователя. Инструментом для исследования исчислений, а также часто и мотивировкой для самого введения ряда исчислений служит точно определенная семантика для формул рассматриваемого языка, т. е. точное определение смысла суждений, выразимых в данном языке. Напр., для классич. исчисления высказываний такая семантика хорошо известна: в этом исчислении выводимы тавтологии и только они. В общем случае, чтобы показать, что нек-рая формула Ане выводится в рассматриваемом исчислении Т*, достаточно построить семантику для формул языка этой теории таким образом, чтобы все формулы, выводимые в Т*, были истинны в этой семантике, в то время как Ане истинна. Семантика может быть классической, интуиционистской или иного типа в зависимости от того, с какими логич. постулатами она согласована. В исследовании классич. исчислений с успехом применяются неклассич. семантики, напр, отношение вынуждения П. Коэна при естественном уточнении задает интуиционистскую семантику. В другом известном варианте теории П. Коэна используются многозначные семантики — модели с истинностными Значениями в полной булевой алгебре. С другой стороны, семантики типа Крипке моделей, определенные классическим теоретико-множественным способом, позволяют выяснить многие свойства модальных и нестандартных логик (включая интуиционистскую логику). Алгебраич. методы получили широкое развитие в Д. т. в виде моделей теории. Алгебраич. система, сопоставляющая каждому начальному символу языка нек-рый алгебраич. объект, естественно определяет нек-рую классич. семантику языка. Алгебраич. система наз. моделью формальной теории Т*, если все формулы, выводимые в Т*, истинны в семантике, порожденной алгебраич. системой. К. Гёдель в 1931 показал, что всякое непротиворечивое исчисление (с классич. логикой) имеет модель. Несколько позже А. И. Мальцев независимо от результата К. Гёделя установил, что если каждый конечный фрагмент исчисления имеет модель, то и все исчисление в целом имеет модель (так наз. теорема о компактности логики первого порядка). Эти две теоремы легли в основу целого направления в математич. логике. Рассмотрение нестандартных моделей арифметики позволило установить неаксиоматизируемость понятия натурального ряда в рамках теорий 1-го порядка, доказать независимость принципа математич. индукции от других аксиом арифметич. исчисления. Относительность понятия мощности множества в классич. математике выявилась при изучении счетных моделей для формальных теорий, стандартная интерпретация к-рых предполагает лишь заведомо несчетные модели (так наз. парадокс Сколема). Многие синтаксич. результаты были получены вначале из теоретико-модельных соображений. В терминах конструкций теории моделей можно дать простые критерии для многих понятий, интересных с точки зрения Д. т. Так, критерий Скотта гласит, что класс Калгебраич. систем данного языка тогда и только тогда является аксиоматизируемым, когда он замкнут относительно ультрапроизведений, изоморфизмов и взятия элементарных подсистем. Формальная теория наз. разрешимой, если существует алгоритм, позволяющий по произвольной формуле Авыяснять, выводима ли Ав этой теории или нет. Известно, что всякая формальная теория, содержащая нек-рый фрагмент теории рекурсивных функций, необходимо неразрешима. Отсюда следует неразрешимость элементарной арифметики, системы Цермело — Френкеля и многих других теорий. В Д. т. разработаны тонкие методы интерпретации одних теорий в других; с помощью таких интерпретаций можно установить неразрешимость и ряда очень простых исчислений, в к-рых не интерпретируются непосредственно рекурсивные вычисления. Примерами могут служить элементарная теория групп, теория двух отношений эквивалентности, элементарная теория частичного порядка. С другой стороны, имеются примеры интересных разрешимых теорий, таких, как элементарная геометрия, элементарная теория действительных чисел, теория множеств натуральных чисел с единственной операцией следования. Разрешимость теорий доказывается теоретико-модельными и синтаксич. методами. Синтаксические методы часто дают более простые разрешающие алгоритмы. Так, например, для элементарной теории р-адических чисел разрешимость была установлена сначала теоретико-модельными методами. Позднее был найден примитивно-рекурсивный алгоритм распознавания выводимости для этой теории с помощью нек-рой модификации синтаксич. метода элиминации кванторов. Существенной является оценка сложности алгоритмов разрешения теорий. Как правило, для разрешимых теорий имеется примитивно-рекурсивный разрешающий алгоритм, и проблема состоит в том, чтобы указать более точные границы сложности. Перспективным направлением исследований является изучение разрешимости естественных фрагментов известных формальных теорий. В этом отношении особенно подробно, изучено классич. исчисление предикатов, где эффективно описаны все разрешимые и неразрешимые классы формул, заданные в терминах расположения кванторов в формуле и вида предикатных символов, встречающихся в формуле. Описан ряд разрешимых фрагментов арифметич. исчисления, элементарной теории множеств. Внимание исследователей привлекают и методы оценки сложности выводов. Сюда относятся такие проблемы, как отыскание сравнительно коротких формул, необходимо имеющих сложные доказательства, или формул, из к-рых уже сравнительно несложно можно получить большое количество результатов. Такие формулы можно рассматривать как выражающие в нек-ром смысле "глубокие" факты теории. Рассматриваются естественные меры сложности вывода: длина доказательства; время, требуемое для поиска вывода; сложность формул, фигурирующих в выводе, и др. В этой области методы Д. т. смыкаются с методами теоретич. кибернетики. Лит.:[1] Клини С. К., Математическая логика, пер. с англ., М., 1973; [2] Френкель А., Бар — Xиллел И., Основания теории множеств, пер. с англ., М., 1966; [3] Ершов Ю. Л. и др., "Успехи матем. наук", 1965, т. 20, в. 4, с. 37-108. А. Г. Драгалин.