Математическая энциклопедия - доказательств теория

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

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

Истоки Д. т. можно проследить со времен античности (дедуктивный метод рассуждения в элементарной геометрии, силлогистика Аристотеля и др.), но современный этап ее развития начинается в конце 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) по конструктивной семантике, использующие общие индуктивные определения. Кроме того, ряд важных проблем, относящихся к исчислениям, можно рассматривать и вне связи с основаниями математики. Сюда относятся вопросы о полноте и разрешимости формальных теорий, вопрос о независимости нек-рых утверждений от данной формальной теории и др. В такой ситуации нет необходимости ограничиваться в рассуждениях определенными средствами и можно развивать Д. т. как обычную математич. теорию, пользуясь любыми математич. средствами доказательства, убедительными для исследователя.