Разработка больших международных проектов по созданию ИИ-систем автоматизации всего процесса математического познания на основе доказательства теорем. Значение "сколемизации" формальных выражений и искажение семантики их неформальных прототипов.
Аннотация к работе
В последнее десятилетие началась разработка больших международных проектов по созданию ИИ-систем автоматизации всего процесса математического познания на основе автоматического доказательства теорем, формальной верификации математических моделей сложных систем, математической поддержки процессов принятия решений, прежде всего, в военной области, в космических исследованиях, в ядерной физике и т.п. В ряде важных случаев, в аксиоматической теории множеств имеются теоремы, в которых по тем или иным причинам отсутствует явная формулировка необходимых условий их доказательства. Но возможна и обратная ситуация, когда отсутствие явной формулировки необходимых условий некоторого доказательства делает такое доказательство формально «безупречным», а соответствующую «теорему» - убедительной и неопровержимой. Однако, после этих признаний, W.Hodges делает довольно странный с точки зрения математики вывод: это «принятие» актуальной бесконечности «является фактом общеизвестным и общепринятым», а потому «нет никакой необходимости каждый раз явно выписывать этот необходимое условие в начале каждого доказательства». Как известно, в математике явная формулировка необходимых условий любого доказательства, во-первых, является первейшим требованием корректности доказательства, а, во-вторых, не способна лишить такое доказательство его легитимности.Таким образом, в основаниях современной метаматематики (так называемой «теории доказательства»), а именно, в классическом исчислении предикатов и аксиоматической теории множеств имеется целый ряд формальных дефектов, которые приводят к ложным, как формальным, так и эпистемологическим, выводам.