В логике и математике формальное доказательство или вывод — это конечная последовательность предложений (известных как правильно сформированные формулы , когда речь идет о формальном языке ), каждое из которых является аксиомой , предположением или следует из предыдущих предложений в последовательности в соответствии с правилом вывода . Оно отличается от аргумента на естественном языке тем, что является строгим, недвусмысленным и механически проверяемым. [1] Если набор предположений пуст, то последнее предложение в формальном доказательстве называется теоремой формальной системы . Понятие теоремы, как правило, эффективно , но может не быть метода, с помощью которого мы можем надежно найти доказательство данного предложения или определить, что его не существует. Понятия доказательства в стиле Фитча , секвенциального исчисления и естественной дедукции являются обобщениями понятия доказательства. [2] [3]
Теорема является синтаксическим следствием всех правильно построенных формул, предшествующих ей в доказательстве. Чтобы правильно построенная формула могла считаться частью доказательства, она должна быть результатом применения правила дедуктивного аппарата (некоторой формальной системы) к предыдущим правильно построенным формулам в последовательности доказательства.
Формальные доказательства часто строятся с помощью компьютеров в интерактивном доказательстве теорем (например, с помощью проверки доказательств и автоматического доказательства теорем ). [4] Примечательно, что эти доказательства могут быть проверены автоматически, также с помощью компьютера. Проверка формальных доказательств обычно проста, в то время как проблема поиска доказательств (автоматическое доказательство теорем) обычно вычислительно неразрешима и/или только полуразрешима , в зависимости от используемой формальной системы.
Формальный язык — это набор конечных последовательностей символов . Такой язык может быть определен без ссылки на какие-либо значения любого из его выражений; он может существовать до того, как ему будет приписана какая-либо интерпретация — то есть до того, как он обретет какое-либо значение. Формальные доказательства выражаются на некоторых формальных языках.
Формальная грамматика (также называемая правилами формирования ) — это точное описание правильно построенных формул формального языка. Она синонимична набору строк в алфавите формального языка, которые составляют правильно построенные формулы. Однако она не описывает их семантику (т. е. то, что они означают).
Формальная система (также называемая логическим исчислением или логической системой ) состоит из формального языка вместе с дедуктивным аппаратом (также называемым дедуктивной системой ). Дедуктивный аппарат может состоять из набора правил преобразования (также называемых правилами вывода ) или набора аксиом , или иметь и то, и другое. Формальная система используется для вывода одного выражения из одного или нескольких других выражений.
Интерпретация формальной системы — это присвоение значений символам и истинностных значений предложениям формальной системы. Изучение интерпретаций называется формальной семантикой . Предоставление интерпретации синонимично построению модели .