Inlogic andmathematics, aformal proof orderivation is a finitesequence ofsentences (known aswell-formed formulas when relating toformal language), each of which is anaxiom, an assumption, orfollows from the preceding sentences in the sequence, according to therule of inference. It differs from a natural language argument in that it is rigorous, unambiguous and mechanically verifiable.[1] If the set of assumptions is empty, then the last sentence in a formal proof is called atheorem of theformal system. The notion of theorem is generallyeffective, but there may be no method by which we can reliably find proof of a given sentence or determine that none exists. The concepts ofFitch-style proof,sequent calculus andnatural deduction aregeneralizations of the concept of proof.[2][3]
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 thedeductive 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 ininteractive theorem proving (e.g., through the use of proof checker andautomated theorem prover).[4] Significantly, these proofs can be checked automatically, also by computer. Checking formal proofs is usually simple, while the problem offinding proofs (automated theorem proving) is usuallycomputationally intractable and/or onlysemi-decidable, depending upon the formal system in use.
Aformal language is aset of finitesequences ofsymbols. Such a language can be defined withoutreference to anymeanings of any of its expressions; it can exist before anyinterpretation is assigned to it – that is, before it has any meaning. Formal proofs are expressed in some formal languages.
Aformal grammar (also calledformation rules) is a precise description of thewell-formed formulas of a formal language. It is synonymous with the set ofstrings over thealphabet of the formal language which constitute well formed formulas. However, it does not describe theirsemantics (i.e. what they mean).
Aformal system (also called alogical calculus, or alogical system) consists of a formal language together with a deductive apparatus (also called adeductive system). The deductive apparatus may consist of a set oftransformation rules (also calledinference rules) or a set ofaxioms, or have both. A formal system is used toderive one expression from one or more other expressions.
Aninterpretation 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 calledformal semantics.Giving an interpretation is synonymous withconstructing amodel.
| Functional: |  | |
|---|---|---|
| Formal: | ||
| Negation | ||
| General | |||||||||
|---|---|---|---|---|---|---|---|---|---|
| Theorems (list) and paradoxes | |||||||||
| Logics |
| ||||||||
| Set theory |
| ||||||||
| Formal systems (list), language and syntax |
| ||||||||
| Proof theory | |||||||||
| Model theory | |||||||||
| Computability theory | |||||||||
| Related | |||||||||
