Formal proof


In logic and mathematics, a formal proof or derivation is a finite sequence of sentences, 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 checkable. 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 to the previous well-formed formulas in the proof sequence.
Formal proofs often are constructed with the help of computers in interactive theorem proving. Significantly, these proofs can be checked automatically, also by computer. Checking formal proofs is usually simple, while the problem of finding proofs is usually computationally intractable and/or only semi-decidable, depending upon the formal system in use.

Background

Formal language

A formal language is a set of finite sequences of symbols. Such a language can be defined without reference to any meanings of any of its expressions; it can exist before any interpretation is assigned to it - that is, before it has any meaning. Formal proofs are expressed in some formal languages.

Formal grammar

A formal grammar is a precise description of the well-formed formulas of a formal language. It is synonymous with the set of strings over the alphabet of the formal language which constitute well formed formulas. However, it does not describe their semantics.

Formal systems

A formal system consists of a formal language together with a deductive apparatus. The deductive apparatus may consist of a set of transformation rules or a set of axioms, or have both. A formal system is used to derive one expression from one or more other expressions.

Interpretations

An interpretation of a formal system is the assignment of meanings to the symbols, and truth values to the sentences of a formal system. The study of interpretations is called formal semantics. Giving an interpretation is synonymous with ''constructing a model.