A mathematical statement whose truth has been established by means of a proof.
The concept of a theorem developed and became more precise together with the concept of a mathematical proof. With the use of the axiomatic method, the theorems in a theory under consideration are defined as statements deduced in a purely logical way from previously chosen and fixed statements called axioms. Since axioms are assumed to be true, theorems ought to be true as well. A further refinement of the concepts of a proof and a theorem was connected with the investigation, undertaken in mathematical logic, of the concept of a logical consequence, as a result of which for a wide class of mathematical theories it became possible to reduce the process of logical deduction to transformations of formulas, that is, of mathematical statements written in a suitably formalized language, using exactly formulated rules (deduction rules, cf. Derivation rule) about merely the form (and not the content) of the propositions. In formal theories arising in this manner the name proof is given to a finite sequence of formulas each of which either is an axiom or is obtained from certain preceding formulas of this sequence according to the deduction rules. A formula is called a theorem if it is the last formula in a proof.
Such a refinement of the notion of a theorem made it possible to obtain, using rigorous mathematical methods, a series of important results on mathematical theories. In particular, it has been established that axiomatic theories representing substantial chapters of mathematics (for instance, arithmetic) are incomplete, that is, there exist propositions whose truth or falsity cannot be established in a purely logical way on the basis of axioms. As a rule, these theories are undecidable, that is, there is no unique method (algorithm) making it possible to decide whether an arbitrarily given statement is a theorem.
[a1] | S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951) pp. 288 |
[a2] | J.R. Shoenfield, "Mathematical logic" , Addison-Wesley (1967) |