Понятие формального вывода.
Когда говорят о формальном доказательстве, прежде всего описывают формальную модель — множество аксиом, записанных с помощью формального языка, и правил вывода. Формальным выводом называется конечное упорядоченное множество строк, написанных на формальном языке, таких, что каждая из них либо является аксиомой, либо получена из предыдущих строк применением одного из правил вывода. Формальным доказательством утверждения называется формальный вывод, последней строкой которого является данное утверждение. Утверждение, имеющее формальное доказательство, называется теоремой, а множество всех теорем в данной формальной модели (рассматриваемое вместе с алфавитом формального языка, множествами аксиом и правил вывода) называется формальной теорией.
Последовательность формул исчисления высказывания, называется формальным выводом, если каждая формула этой последовательности имеет следующий вид:
Полнота базы знаний. Представление неполных знаний.
ПОЛНОТА́- свойство формальных систем (исчислений), характеризующее достаточность для к.-л. определ. целей, их выразительных и (или) дедуктивных средств. П. в первом смысле наз. обычно ф у н к ц и о н а л ь н о й (см. Полнота функциональная), во втором – д е д у к т и в н о й. Впрочем, вместо "дедуктивная П." (в ее различных модификациях, см. Полнота дедуктивная) часто говорят просто "П.". Понятие (дедуктивной) П. по своему происхождению носит с е м а н т и ч е с к и й (см. Семантика в логике) характер: дедуктивная теория (формальная система) наз. (семантически) полной (относительно к.-л. фиксированной интерпретации), если каждое выразимое ее средствами истинное (при данной интерпретации) предложение доказуемо в ней; в противном случае система наз. неполной. Более общо: система наз. полной по отношению к нек-рому св-ву, если все ее формулы, обладающие этим св-вом, доказуемы (это понятие сводится к предыдущему, если в качестве рассматриваемого св-ва формул иметь в виду истинность выражаемых ими при нек-рой интерпретации предложений). Для широкого класса формальных систем (в частности, для прикладных исчислений предикатов первого порядка с равенством – см. Предикатов исчисление) указанные (и родственные им) семантич. понятия допускают и чисто с и н т а к с и ч е с к у ю (см. Синтаксис в логике) переформулировку. Напр., формальная система наз. (формально) полной, если присоединение к ней любой недоказуемой в ней формулы (выразимой на языке нерасширенной теории) приводит к ее противоречивости (см. Непротиворечивость).
Для широкого класса исчислений из их П. в указ. смысле следует их разрешимость (см. Разрешения проблемы). Т.о., проблема П. формальной системы, означающей по существу П. (в самом буквальном смысле слова) отображения формально-аксиоматич. средствами соответств. содержат. область (научного) знания (см. Формализация, Метод аксиоматический), становится в ряде случаев предметом точного (пользующегося матем. методами) рассмотрения в рамках спец. матем. дисциплины, названной Д. Гильбертом метаматематикой, или теорией доказательства (см. Метатеория). (Следует, впрочем, отметить, что не всякое понятие П. может быть выражено – не говоря уже о решении – метаматем. средствами; это относится, напр., к такому "неэффективному" по своему заданию понятию, как "П. относительно п р о и з -в о л ь н о й интерпретации".) В ходе метаматем. исследований был получен ряд важнейших результатов о П. различных логич. исчислений (Э. Пост, К. Гёдель). С др. стороны, ряд результатов, важнейшим из к-рых безусловно является теорема Гёделя о неполноте (и непополнимости) формальной арифметики (в этой связи весьма важны также результаты Чёрча и Тарского), послужили одним из стимулов к поискам более широких средств формализации науч. теорий и более сильных дедуктивных средств. Следует также отметить, что П. отнюдь не является необходимым условием плодотворности конкретной формализации науч. теории; более того, именно неполные теории, в силу возможности неизоморфных их расширений (см. Изоморфизм, Категоричность системы аксиом), имеют разнообразные приложения, чем и определяется их науч. ценность.
пределах.