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