Колмогоров А.Н. Уравнения турбулентного движения несжимаемой жидкости (1124030), страница 81
Текст из файла (страница 81)
Результаты главы 1У в несколько обобщенной форме сформулированы в [24) 4упражкенме 38.12) так. Для каждой формулы А исчисления предикатов следую«цим образом определим формулу А* («перевод» формулы А): если А есть элементарная формула, то А* есть ) ) А; (А Д В)» есть [ ) (А» е«, В»); (А ~/ ~/ В)* есть ) ) (А* ~/ В*); (А ~ В)* есть ~ ) (А* ~ В"); ( ) А)» есть ) А*; если А есть»е хВ, то А*есть ) )»хВ»; если А есть 3 хВ,тоА" есть ) ) 3 хВ». Формула А является теоремой классического исчисления предикатов тогда и только тогда, когда А * есть теорема минимального исчисления предикатов.
В действительности в работе ПТНД «перевод»классических теорем ва язык интуиционистской системы осуществляется не только для логических формул. По существу та»«намечена схема получения для широкого класса матеыатических теорий следующего метаматематического результата: если в некоторой классической теории с использованием закона исключенного третьего нли эквивалентных ему принципов доказано некоторое утверждение, то некоторое равносильное ему (с классической точки зрения) утверждение может быть доказано и без вакона исключенного третьего, а именно в рамках минимальной логики. В частности, если в некоторой теории с помощью закона исключенного третьего получено противоречие, то противоречивое суждение может быть доказано и без использования этого закона. Таким образом, использование закона исключенного Интуиционистскол логика (В.
А. Успенский, В. Е. Плиско) 399 третьего нельзя считать подлинной причиной противоречий в классической математике, в частности причиной теоретико-лгножественных антиномий. Результаты работы ПТНД моншо резюмировать и таким образом. Пусть аксиомы математической теории таковы, что описанные выше их «переводы» признаны истинными с интуиционистской точки зрения. Тогда перевод всякой теоремы етой теории также должен быть признан истинным с интуицноннстской точки зрения. Этот вывод имеет принципиальное значение.
Он показывает, что та часть классической математики, которая имеет дело только с интуиционистски допустимыми объектами(например, арифметика), может быть истолкована интуиционистски с полным сохранением ее классического содержания. Таким образоы, ограничение интуиционистской логикой не является существенным и различие интуиционистской и классической математики проявляется главным образом в способах образования абстрактных математических понятий. Погружение классических логических и логико-математических теорий в соответствующие теории, основанные на интуиционистской логике, стало в дальнейшем важным инструментом исследования интуиционистских теорий, ибо оно часто позволяет без лишних усилий перенести результаты, полученные при исследовании классических теорий, на интуиционистские. Шаниным [25[ проведено детальное исследование различных погружений классической арифметики в интуиционистскую. Им введен термин «погружающая операция» для обозначения такого алгоритма, который по каждому арифметическому предложению А строит другое арифметическое предложение А», обладающее тем свойствоы, что А доказуемо в классической арифметике тогда и только тогда, когда А" доказуемо в интуиционистской арифметике.
Таким образом, в работе ПТНД построен исторически первый пример погружающей операции. Несколько позднее сходное погружение классической логики в интуициопистскую было предлол«ено Геделем [29[. В [251 доказано, что погружающие операции Колмогорова и Геделя эквивалентны в том смысле, что реаультаты их применения к любой формуле ивтуицвоипстски эквивалентны. Если з работе ПТНД построена погружающая операция, которая позволяет дать ннтуиционистское истолкование для значительной части классической математики, то работа ТИЛ посвящена решению в известном смысле обратной аадачи: дать толкование интуиционистской логики в рамках обычных математических понятий, независимое от философских и методологических установок ннтувциопиама.
Это удается сделать, трактуя логические формулы не как схемы суждений, а как схемы типов задач. При этом общеаначимость или еистинность» логической формулы понимается как существование общего метода решения всех задач данного типа. Такиы образом, например, «опровергается»,' закон исключенного третьего: общезначимость формулы а ~/ [ а означала бы существование общего метода, позволяющего для любой конкретной задачи либо найти ее решение, либо привести к противоречию предположение о существовании ее решения.
Поскольку такой метод вряд ли возможен, формулу а 'у' [ а нельзя признать общезначимой. В то же время все формулы, выводимые в иптуиционист- Комментарии оком исчислении высказываний, оказываются общезначимыми. Тем самым получена интерпретация атого исчисления как логика задач. Найденная интерпретация интуиционистской логики имела важное методологическое значение. В рамках хотя и не вполне точных, но все же понятных любому математику понятий «задачи» и «решения задачи» была обоснована необходимость рассмотрения логических систем, ие содержащих закона исключенного третьего.
П. С. Новиков указывает в [14, с. 54 — 55[: «В 1932 г. Колмогоровым (10[ была предложена интересная интерпретация этого [иитуиционистского.— В. У., В. П.[ исчисления, не связанная с какими-то новыми специфическими принципами в основаниях математики. Согласно Колмогорову, наряду с традиционной логикой, систематизирующей схемы доказательств теоретических истин, возможна также логика, снстематизирующая схемы решения задач (например, геометрических задач на построение).
При этом понятия «задачи» и «решения задачи» считаются первоначальными». Свободное от философских установок интуициониама, новое истолкование интуиционистской логики, сделало осмысленным исследование ее как исчисления задач. Характерно, что в 50-е годы сам термин «исчисление задаче употреблялся в советской логика-математической литературе для обозначения интуиционистского исчисления высказываний (см., например, [15, 16[). Таким образом, в работе ТИП изложена в достаточно раавернутом виде идея истолкования логических формул с помощью задач.
Эта идея впоследствии получила различные конкретные воплощения, характеризующиеся выбором того или иного точно очерченного класса задач. Первое математическое развитие идеи А. Н. Колыогорова об истолковании иитуиционистской логики как исчисления задач было дано его учеником Медведевым [12[ (см. также [21, $13.7[). Каждая из задач, рассматриваемых Медведевым, является задачей нахождекия всюду определенной функции с заданными свойствами.
Такие задачи названы в [12[ «массовыми проблемами». Массовая проблема нааывается алгоритмически раарешимой (или просто <разрешимой»), если среди ее решений имеется общерекурсивная функция. Центральное место в развиваемой теории аанимает понятие сводимости одной массовой проблемы к другой, которое носит алгоритмический характер. Удается определить логические операции над массовыми проблемами, отражающие идеи, высказанные А. Н. Колмогоровым.
Оказалось, что все формулы, выводимые в интуиционистском исчислении высказываний, являются схемами алгоритмически разрешимых массовых проблем. Несколько позднее Медведевыи [13[ была предложена другая интерпретация логических формул посредствои аадач. При атом в качестве ограничения и уточнения понятия задачи использовались так называемые финитные задачи.
Финитная задача определяется непустым конечным множеством воаможных решений, в котором выделено некоторое, '(возможно, пустое) подмножество фактических решений. Задаются логические операции над финитными задачами. При этом, например, А ~ В есть финитная задача, возможными решениями которой служат проиавольные отобрав<ения множества всех возможных решений задачи А в множество возможных решений задачи В, а фактические решения — ато те отображения, которые переводят фактические решения аадачи А в фактические решения а«дачи В.
Пусть теперь А (р,,..., рн) — какая-либо пропозициональная формула с переменными р,,..., р„. Зафиксируем непустые конечные мно- Интуиционистская логика (В. А. Успенский, В. Е. Плиско) 401 пества Х,,..., Хя и будем подставлять в формулу А вместо переменных р„... ..., р„всевозможные финитные задачи р,,..., р„, множества возможных решений которых суть множества Х»,..., Х„, варьируя множества фактических решений.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
