Введение
Установление теоремы посредством вывода из аксиом
В логике и математике формальное доказательство или вывод представляет собой конечную последовательность предложений (называемых хорошо сформированными формулами в случае формального языка), каждое из которых является аксиомой, предположением или следует из предшествующих предложений в последовательности по правилу вывода. Оно отличается от аргумента на естественном языке тем, что является строгим, однозначным и механически верифицируемым. Если множество предположений пусто, то последнее предложение в формальном доказательстве называется теоремой формальной системы. Понятие теоремы в общем случае не является эффективным, поэтому может не существовать метода, позволяющего всегда найти доказательство данного предложения или установить, что его не существует. Доказательства в стиле Фича, исчисление секвенций и натуральная дедукция являются обобщениями понятия доказательства. Теорема является синтаксическим следствием всех хорошо сформированных формул, предшествующих ей в доказательстве. Для того чтобы хорошо сформированная формула считалась частью доказательства, она должна быть результатом применения правила дедуктивного аппарата (некоторой формальной системы) к предыдущим хорошо сформированным формулам в последовательности доказательств. Формальные доказательства часто строятся с помощью компьютеров в интерактивном доказательстве теорем (например, посредством использования проверочных средств для доказательств и автоматических решателей теорем). Важно отметить, что эти доказательства могут быть проверены автоматически, также с помощью компьютера. Проверка формальных доказательств обычно проста, в то время как задача поиска доказательств (автоматическое доказательство теорем) обычно является вычислительно неразрешимой и/или лишь полуразрешимой, в зависимости от используемой формальной системы.
In logic and mathematics, a formal proof or derivation is a finite sequence of sentences (called well formed formulas in the case of a formal language), each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence by a rule of inference. It differs from a natural language argument in that it is rigorous, unambiguous and mechanically verifiable. If the set of assumptions is empty, then the last sentence in a formal proof is called a theorem of the formal system. The notion of theorem is not in general effective, therefore there may be no method by which we can always find a proof of a given sentence or determine that none exists. The concepts of Fitch style proof, sequent calculus and natural deduction are generalizations of the concept of proof. The theorem is a syntactic consequence of all the well formed formulas preceding it in the proof. For a well formed formula to qualify as part of a proof, it must be the result of applying a rule of the deductive apparatus (of some formal system) to the previous well formed formulas in the proof sequence. Formal proofs often are constructed with the help of computers in interactive theorem proving (e. g., through the use of proof checker and automated theorem prover). Significantly, these proofs can be checked automatically, also by computer. Checking formal proofs is usually simple, while the problem of finding proofs (automated theorem proving) is usually computationally intractable and/or only semi decidable, depending upon the formal system in use.
Формальный язык
Формальный язык — это множество конечных последовательностей символов. Такой язык может быть определён без обращения к какому-либо значению его выражений; он может существовать до того, как ему будет дана какая-либо интерпретация, то есть до того, как он приобретёт какой-либо смысл. Формальные доказательства выражаются на некоторых формальных языках.
Формальная грамматика
Формальная грамматика (также называемая правилами порождения) — это точное описание правильно построенных формул формального языка. Она эквивалентна множеству строк над алфавитом формального языка, составляющих правильно построенные формулы. Однако она не описывает их семантику (то есть их значение).
Формальные системы
Формальная система (также называемая логическим исчислением или логической системой) состоит из формального языка и дедуктивного аппарата (также называемого дедуктивной системой). Дедуктивный аппарат может состоять из набора правил преобразования (также называемых правилами вывода), набора аксиом или включать и то, и другое. Формальная система используется для вывода одного выражения из одного или нескольких других выражений.
Интерпретации
Интерпретация формальной системы — это назначение значений символам и значений истинности предложениям этой формальной системы. Изучение интерпретаций называется формальной семантикой. Предоставление интерпретации равносильно построению модели.