Колмогоров А.Н. Уравнения турбулентного движения несжимаемой жидкости (1124030), страница 82
Текст из файла (страница 82)
Формула А называется финитно общеаначимой, если прн любом выборе множеств Х„..., Х„всегда найдется общее фактическое решение у всех задач А (р,,..., рн), полученных на формулы А подстановкой указанного вида. Иными словами, пропозипиональная формула А (р„..., р„) является фивитно общезначнмой, если можно указать фактическое решение задачи А (Р„... , . „рн), зная лишь множества воз»южных решений задач р„..., р„.
Логика финитвых аадач оказалась устроенной довольно сложно. Она не совпадает с интуиционистским псчислениеы высказываний. Например, формула ( [ а ) -> Ь '/ с) ~ (' ) а ~ Ь) ~»З ( ~ а ~ с) финитно общезначима, но иевыводима в этом исчислении. Неиавество, является ли эта логика разрешимой. Докааано лишь, что она не' может быть задана конечным множеством аксиом (см. [11[). В последнее время Скворцовым рассматривались некоторые естественные обобщения нонятня финитвой задачи и соответствующие интерпретации логических формул (см. [22, 23)). Одно обобщение состоит в рассыотрении ве только финитных задач, но задач с проиавольным множеством возможных и фактических решений.
Доказано, что получающаяся при этом логика не совпадает с ннтуиционистскнм исчнслениеы высказываний, но может быть задана посредством рекурсивной системы аксиом. Другое обобщение понятия финитнов задачи, введенное Скворцовым [22[, свяаано с рассмотрением аадач, возможными и фактическими решениями которых являются натуральные числа, а логические операции носят алгоритмический характер. Так, фактическим решением задачи А ~ В является всякое натуральное число, которое служит геделевым номером частично рекурсивной функции, отображающей возможные решения задачи А в возможные решения задачи В, причем фактические решения задачи А отображаются в фактические решения задачи В. Эта интерпретация, называемая рекурсивной общезначимостью, распространяется и ва предикатные формулы. Рассмотренные выше интерпретации логических формул возникли как прямое развитие идей А.
Н. Колмогорова, вмскааавных в работе ТИЛ. Заметим, что интерпретацию формул с помощью задач не следует рассматриватьнепосредствевно как разъяснение интуициовистского смысла формул. Речь идет как раа о независимом от интуиционистскил иредставлений истолковании логиче ских формул, которое приводит к логике без закона исключеняого третьего. Однако в $2 работы ТИЛ А. Н. Колмогоров показывает, что ивтуиционистский смысл экзистенциального утверждения естественным образом может быть свяаан с некоторой аадачей.
С другой стороны, согласно Гейтивгу,«математическое высказывание утверждает тот факт, что было выяолнево некоторое математическое построение» [4, с. 11[, и вопрос об истинности высказывания заключается в существовании такого построения, т. е. имеет экзистенциальный характер. Поэтому идеи исчисления аадач оказываются применимыми к истолкованию интуиционистского смысла проиавольных математических суждений.
В математически точной форме восходящая к Гейтингу идея трактовки математического предложения как требования некоторого построения была осуществлена Кливи по отношению к арифметическим суждениям [34) (см. также [8, 14)). 402 Л'еммевтар из С каждым арифметическим предложением связывается некоторое (возможно, пустое) множество натуральных чисел, вавываемых реаливациями этого предложения. Грубо говоря, реализация кодирует информацию об интуиционистской истинности предложения. Так, элементарное предложение вида з = г имеет реализацию только в случае, когда оно истинно в обычном смысле. Число е является реалиаацией предложения вида А ~ В, если частично рекурсивная функция с геделевым номером е применима к любой реализации формулы А и перв- водит ее в некоторую реализацию формулы В.
Формула называется реализуемой, если существует число, реализующее ее. Рекурсивная реализуемость обычно рассматривается как аналог интуиционистской (точнее, конструктивной) истинности. Можно, например, построить предложение вида тх (А (з) ~/ [ А (з)) которое не будет истинным в этом смысле. Свяаь рекурсивной реализуемости с исчислением задач состоит в том, что установление реалиауемости арифметического суждения можно рассматривать как задачу в колмогоровском смысле.
(Более явно идея сопоставления каждому арифметическому предложению некоторой задачи осуществлена в предложенном Шаниным [26) алгоритме конструктивной расшифровки математических суждений.) Можно развивать соответствующую логику решения таких вадач, рассматривая в качестве общезначимых или реализуемых так логические формулы, которые являются схемами реализуемых арифметических предложений. Возникавяцая при этом логика высказываний впервые исследовалась Роузом [39).
Им было установлено, что не все реализуемые пропозицнональные формулы доказуемы в интуиционистском исчислении высказываний. В дальнейшем логика рекурсив» ной реализуемости исследовалась в работах [1, В, 7] и др. Однако до сих пор не получено какой-либо характеризацни класса реализуемых пропозицнональных формул. В частности,невавестно, является ли этот класс разрешимым или хотя бы перечислимым. Наибольший прогресс достигнут в исследовании логики предикатов, оснс ванной на понятии реализуемости. Установлено [19), что зта логика не может быть задана в виде исчисления и даже не является арифметической, т. е.
класс всех реализуемых предикатных формул не может быть определен арифметической формулой. Попутно удалось показать [17), что если вместо яаыка формальной арифметики ваять некоторый болеее богатый язык и овределить для него понятие реализуемости, то соответствующий ему класс реализуемых предикат ных формул окажется существенно более узким, чем в случае клиниевской реализуемости. Таким образом, семантика предвкатных формул окаамвается зависящей от исходного логико-математического языка.
В работе [18) Плиско, основываясь ва идеях рекурсивной реалиауемости, предложил понятие абсолютно реалиауемой предикатной формулы, не зависящее от какого-либо конкретного языка. Понятие абсолютной реализуемости близко упоминавшемуся выше понятию рекурсивной реализуемости. В заключение обратимся к поставленному в конце 3 2 главы 11 работы ПТНД вопросу о полноте системы аксиом 1 — 4 для формул без отрицания: всякая ли формула, выводимая в классическом исчислении выскааываний и содер- Ннтуицивниетекаа логика (В.
А. Уекенекий, В. Е. Плиекв) 403 жащая лишь символы импликации, выводима на основе аксиом 1 — 4 системы Гильберта? Отрицательный ответ дает Ван Хао (42, с. 416Ь А именно формула ((аз Ь) ~ а) ~ а выводима в классическом исчислении высказываний, так как является тавтологией. В то же время она иевыводшга из аксиом 1 — 4, так как она невыводима в ивтуиционистском исчислении высказываний. Действительно, подставка в указанную формулу )а вместо переменной 6, мы получим форму.
лу, эквивалентную закону двойного отрицания. ЛИТЕРАТУРА 1. Варкахвеекий Ф. 7. О нереализуемости диаъюнкции нереализуемых формул.— ДАН СССР, 1965, т. 161, № 6, с. 1257 — 1258. 2. Воробьев Б. Н. Новый алгорифм выводпмости в конструктивном исчислении высказываний.— Тр. МИАН СССР, 1958, т.
52, с. 193 — 225. 3. Гейтине А. Обаор исследований по основаниям математики ) Пер. с нем. М.„ Лл ОНТИ, 1936. 4. Гейтинг А. Интуиционизм)Пер. с англ. Мл Мнр, 1965. 5. Драгалин А. Г. Математический интуиционизм. Введение в теорию докааательств. Мл Наука, 1979.) 6. Бинниг М. М. Об одном свойстве пропозициональных формул.— ДАН СССР, 1967, т. 174, № 2, с.
277 — 278. 7. Кикние М. М. О реалиаациях предикатвых формул.— Зап. науч. семинаров ЛОМИ, 1971, т. 20, с. 40 — 48. 8. Клини С. К. Введение в метаматематику(Пер. с англ. Мл Иад-во иностр. лиг., 1957. 9. Колмогоров А. Н. О принципе 1ег11иш поп йагиг.— Мат. сб., 1925, т. 32, с. 646 — 667. Англ. перл Кв!твувгви А. Н. Ов 1Ье рппс1р!е о! ехс!пйей ш!йй1е.— !в: НеНекввгс в. эак. Ргош Ргейе со бойе!. А еокгсе Ьоой ш шаьЬеша11са! !ой!с, 1879 — 1931.
СашЬНйбе, 1967, р. 416 — 437. 10. Кв!твувгв)( А. Епг Веигипй йег 1птьй11ошз11зсЬеп ! о8!Ь.— Ма1Ь. 21всЬг.> 1932, Вй. 35, 8. 58 — 65. 11. Максимова )Л. Л., Скворцов Д. П., Н(ехтман В. Б. Невозможность конечной аксиоматизации логики фкнитвых задач Медведева,— ДАН СССР, 1979, т. 245, № 5, с. 1051 — 1054.
12. Медведев Ю. Т. Степени трудности массовых проблем.— ДАН СССР, 1955, т. 104, № 4, с. 501 — 504. 13. Медведев Ю. Т. Финитные задачи.— ДАН СССР, 1962, т. 142, № 5, с. 1015— 1018. 14. Нвеиквв П. С. Конструктивная математическая лапша с точки зрения классической. Мл Наука, 1977. 15. Пильчак Б. Ю. О проблеме раарешимости для исчисления задач.— ДАН СССР, 1950, т. 75, № 6, с. ?73 — 776. 16. Пильзен Б. Ю. Об исчислении задач.— Укр.
мат. журн., 1952> т. 4, № 2> с. 174 — 194. 17. Плиекв В. Е. Рекурсивная реализуемость и конструктивная логика предикатов.— ДАН СССР, 1974, т. 214, № 3, с. 520 — 523. 18. П*иекв В. Е. Некоторые варианты понятия реализуемости для предикатных формул.— ДАН СССР, 1976, т. 226, № 1, с. 61 — 64. 19. Плиекв В. Е. Неарифметичность класса реализуемых предикатиых формул.— Изв. АН СССР. Сер. мат., 197?, т. 41, № 3, с. 483 — 502. 20. Раеева Е., Сикорский Р. Математика метаматематики.
Мл Наука, 1972. 21. Роджерс Х. Теория рекурсивных функций в эффективная вычислимость) Пер. с англ. Мл Мир, 1972. 22. Скворцов Д. П, Два обобщения понятия фннитиой задачи.— В кнл Исследования по неклассическим логикам и теории множеств.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
