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

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

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

// .