ГЕДЕЛЬ, ЭШЕР, БАХ: эта бесконечная гирлянда.

Представление знания с помощью логического формализма.

Существует несколько философских школ, по-разному трактующих лучшие способы представления знания и работы с ним. Одна из наиболее влиятельных школ пропагандирует представление знаний с помощью формальной нотации, подобной нотации ТТЧ, — с использованием препозиционных связок и кванторов. Не удивительно, что основные операции в подобной системе выглядят как формализация дедуктивных рассуждений. Логические заключения могут быть сделаны при помощи правил вывода, аналогичных соответствующим правилам ТТЧ. Спрашивая такую систему о какой-либо идее, мы ставим перед ней цель в виде строчки, которую необходимо вывести. Например: «Является ли МУМОН теоремой?» Тут вступают в действие автоматические рассуждающие механизмы, которые пытаются приблизиться к цели, используя различные методы упрощения задач.

Предположим, например, что дано высказывание «все формальные арифметические системы неполны»; вы спрашиваете программу: «Полны ли „Principia Mathematical“». Сканируя имеющуюся в ее распоряжении информацию (часто называемую базой данных), программа может заметить, что если бы ей удалось установить, что «Principia Mathematica» — это формальная арифметика, то она могла бы ответить на вопрос. Таким образом, высказывание «„Principia Mathematica“ — это формальная арифметика» становится подзадачей, после чего в действие вступает метод упрощения задач. Если программа сможет найти что-либо еще, что могло бы способствовать подтверждению (или опровержению) задачи или подзадачи, она начнет работать над этой информацией — и так далее, рекурсивным образом. Этот процесс называется обратным сцеплением данных, поскольку он начинается с цели и затем отступает назад — предположительно к уже известным вещам. Если представить графически основную задачу, подзадачи, подподзадачи и так далее, у нас получится структура дерева, поскольку основная задача может включать несколько подзадач, каждая из которых, в свою очередь, может подразделяться на несколько подподзадач… и т. д.

Обратите внимание, что этот метод не гарантирует решения, так как внутри системы может не существовать способа установить, что «Principia Mathematica» — формальная арифметика. Это, однако, означает не то, что задача или подзадача являются ложными утверждениями, а лишь то, что они не могут быть получены на основании сведений, имеющихся в распоряжении системы в данный момент. Когда такое случается, система может напечатать что-нибудь вроде: «Я не знаю». Тот факт, что некоторые вопросы остаются открытыми, разумеется, подобен неполноте, от которой страдают некоторые хорошо известные формальные системы.