Cтраница 4
В логическом языке Пролог, в основе которого лежит принцип резолюции на базе хорновских дизъюнктов, вывод состоит в доказательстве непротиворечивости цели базе данных, состоящей из правил и фактов. [46]
И все же возникает некоторая другая проблематика, если принять во внимание то вытекающее из теоремы Геделя соображение, что финитное доказательство непротиворечивости формализма анализа и теории множеств позволило бы нам получить финитное доказательство некоторого арифметического предложения, невыводимого в указанном формализме. Выглядит несколько парадоксальным, что при доказательстве арифметических предложений методы финитной теории доказательств в определенном отношении превосходят методы анализа и теории множеств. [47]
Содержательной базой, необходимой для построения и исследования этого исчисления, служит интуиционистская математика, с помощью которой П. С. Новиков и дает доказательство непротиворечивости своего неинтуиционистского исчисления. Вышеупомянутый конкретный математический результат, полученный им при этом, состоит в следующем: Пусть F ( п) есть предложение, зависящее от натурального числа п, проверяемое для любого h конечным числом операций. Тогда, если дано доказательство существования натурального числа N, для которого предложение F ( N) верно, из этого доказательства можно извлечь эффективное указание числа N. Иными словами, П. С. Новиков предложил прием, позволяющий извлечь из некоторых чистых доказательств существования эффективный способ вычисления числа, существование которого утверждается. Для этого вводится неинтуиционистски определяемое понятие содержательно верной формулы и устанавливается, что всякая содержательно верная формула, записываемая в терминах формализма П. С. Новик о в а, доказуема в этом формализме. [48]