Formal proof

A finite derivation in a formal language in which each step follows from stated assumptions or earlier steps by specified inference rules. Its validity depends on the rules and structure of the derivation, not on informal persuasion.

Inference rule: A rule specifying which conclusions may be derived from given premises. Each proof step is licensed by an inference rule.
Formal language: A set of strings formed from symbols according to specified grammatical rules. Proofs use a defined vocabulary and syntax rather than unrestricted prose.
Informal proof: A mathematical argument whose reasoning is expressed in natural language rather than fully specified formal steps. It can communicate a proof without spelling out every syntactic inference.
Proof theory: The mathematical study of formal proofs, derivability, and the structure of proof systems. It treats derivations themselves as objects of mathematical investigation.
Axiom: A statement accepted as a starting point within a formal system. Axioms supply premises from which a derivation can begin.
Formal system: A language equipped with axioms and rules for deriving statements. A formal proof is a derivation inside such a system.
Computer-assisted proof: A mathematical proof whose discovery or verification uses computational methods. Some computer-assisted proofs include formal derivations, while others rely on specialized computations.
Curry–Howard correspondence: A correspondence identifying propositions with types and proofs with programs. It links formal derivations to executable constructions in typed programming languages.
Modus ponens: An inference rule that derives Q from P and if P then Q. This basic rule illustrates how a proof step applies stated premises.
Syntax: The rules governing how symbols may be combined into well-formed expressions. A proof must consist of expressions permitted by the formal language.

Linked from 25 pages