Formal proof

A formal proof or derivation is a finite sequence of sentences (called wellformed formulas in the case of a formal language) each of which is an axiom or follows from the preceding sentences in the sequence by a rule of inference. The last sentence in the sequence is a theorem of a 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 concept of natural deduction is a generalization of the concept of proof.^{[1]}
The theorem is a syntactic consequence of all the wellformed formulas preceding it in the proof. For a wellformed 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 wellformed formulae 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 (automated theorem proving) is usually computationally intractable and/or only semidecidable, depending upon the formal system in use.
Contents
Background
Formal language
Main article: Formal languageA 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 language.
Formal grammar
Main articles: Formal grammar and Formation ruleA formal grammar (also called formation rules) is a precise description of the wellformed 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 (i.e. what they mean).
Formal systems
Main article: Formal systemA formal system (also called a logical calculus, or a logical system) consists of a formal language together with a deductive apparatus (also called a deductive system). The deductive apparatus may consist of a set of transformation rules (also called inference 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
Main articles: Formal semantics (logic) and Interpretation (logic)An interpretation of a formal system is the assignment of meanings to the symbols, and truthvalues to the sentences of a formal system. The study of interpretations is called formal semantics. Giving an interpretation is synonymous with constructing a model.
See also
 Proof (truth)
References
 ^ The Cambridge Dictionary of Philosophy, deduction
External links
 "A Special Issue on Formal Proof". Notices of the American Mathematical Society. December 2008. http://www.ams.org/notices/200811/.
 2πix.com: Logic Part of a series of articles covering mathematics and logic.
Categories: Formal languages
 Proof theory
 Formal systems
 Logical syntax
 Logical truth
Wikimedia Foundation. 2010.
Look at other dictionaries:
proof spirit — proof′ spir it n. vin an alcoholic liquor containing one half of its volume of alcohol of a specific gravity of.7939 at 60° F • Etymology: 1735–45 … From formal English to slang
Proof theory — is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively defined data structures such as plain lists, boxed… … Wikipedia
Proof — may refer to: * A rigorous, compelling argument ** Formal proof ** Mathematical proof ** Proof theory, a branch of mathematical logic that represents proofs as formal mathematical objects ** Logical argument ** Evidence (law), tested evidence or… … Wikipedia
proof — [[t]pruf[/t]] n. 1) evidence sufficient to establish a thing as true or believable 2) anything serving as such evidence 3) the act of testing or trying anything; test; trial: to put a thing to the proof[/ex] 4) the establishment of the truth of… … From formal English to slang
formal — for•mal [[t]ˈfɔr məl[/t]] adj. 1) being in accordance with the usual requirements, customs, etc.; conventional: to pay one s formal respects[/ex] 2) marked by form or ceremony: a formal occasion[/ex] 3) clo designed for wear or use at elaborate… … From formal English to slang
ProofCarrying Code — (PCC) is a software mechanism that allows a host system to verify properties about an application via a formal proof that accompanies the application s executable code. The host system can compare the conclusions of the proof to its own security… … Wikipedia
proof — aff. a combining form of proof, with the meaning “resistant, impervious to” that specified by the initial element: childproof; waterproof[/ex] … From formal English to slang
Formal methods — In computer science and software engineering, formal methods are particular kind of mathematically based techniques for the specification, development and verification of software and hardware systems.cite webauthor=R. W. Butlertitle=What is… … Wikipedia
Proof of impossibility — A proof of impossibility, sometimes called a negative proof or negative result , is a proof demonstrating that a particular problem cannot be solved, or cannot be solved in general. Often proofs of impossibility have put to rest decades or… … Wikipedia
Formal — The term formal has a number of uses, including:General*relating to formality *opposite of informalocial* Formal occasion ** Formal attire worn on such occasions ** Formals are particular meals at some British universities ** In Australian or… … Wikipedia