Формальное доказательство - Formal proof

В логике и математике , А формальное доказательство или вывод является конечной последовательностью из предложений ( так называемая хорошо сформированные формулы в случае формального языка ), каждый из которых является аксиома , предположение, или следует из предыдущих предложений в последовательности по правилу вывода . Он отличается от аргументации на естественном языке тем, что является строгим, недвусмысленным и механически проверяемым. Если множество предположений пусто, то последнее предложение формального доказательства называется теоремой о формальной системе . Понятие теоремы в целом неэффективно , поэтому не может быть метода, с помощью которого мы всегда можем найти доказательство данного предложения или определить, что его не существует. Концепции доказательства в стиле Фитча , исчисления последовательностей и естественной дедукции являются обобщениями концепции доказательства.

Теорема является синтаксическим следствием всех правильно построенных формул, предшествующих ей в доказательстве. Чтобы правильно сформированная формула квалифицировалась как часть доказательства, она должна быть результатом применения правила дедуктивного аппарата (некоторой формальной системы) к предыдущим правильно сформированным формулам в последовательности доказательств.

Формальные доказательства часто строятся с помощью компьютеров при интерактивном доказательстве теорем (например, с использованием средства проверки доказательства и автоматического средства доказательства теорем ). Примечательно, что эти доказательства могут быть проверены автоматически , в том числе с помощью компьютера. Проверка формальных доказательств обычно проста, в то время как проблема поиска доказательств ( автоматическое доказательство теорем ) обычно трудноразрешима с вычислительной точки зрения и / или является лишь частично разрешимой , в зависимости от используемой формальной системы.

Задний план

Формальный язык

Формальный язык представляет собой набор конечных последовательностей из символов . Такой язык может быть определен без ссылки на какое-либо значение любого из его выражений; он может существовать до того, как ему будет приписана какая-либо интерпретация, то есть до того, как он будет иметь какое-либо значение. Формальные доказательства выражаются на некоторых формальных языках.

Формальная грамматика

Формальная грамматика (также называемые правилами образования ) представляет собой точное описание хорошо образованных формулы формального языка. Это синоним набора строк в алфавите формального языка, которые составляют правильно построенные формулы. Однако он не описывает их семантику (то есть то, что они означают).

Формальные системы

Формальная система (также называется логическое исчисление , или логическая система ) состоит из формального языка вместе с дедуктивным аппаратом (также называется дедуктивной системой ). Дедуктивный аппарат может состоять из набора правил преобразования (также называемых правилами вывода ) или набора аксиом , либо иметь и то, и другое. Формальная система используется для получения одного выражения из одного или нескольких других выражений.

Интерпретации

Интерпретация формальной системы является присвоение значений к символам, а также значений истинности для предложений формальной системы. Изучение интерпретаций называется формальной семантикой . Интерпретация является синонимом построения модели .

Смотрите также

использованная литература

внешние ссылки