theorem in nLab

Theorems

There are good reasons why the theorems should all be easy and the definitions hard. (Michael Spivak, preface to “Calculus on Manifolds” )

Theorems

Idea

In the traditional language of mathematics, a theorem is a statement which is of interest in its own right and which has been proven to be true, though the proof may not be immediately obvious. This contrasts with a lemma (which is usually of interest primarily because of its implications for other statements), a conjecture (which has not yet been proved), an axiom (which is obviously true or assumed to be true), a definition (which becomes true by virtue of its assigning meaning to a word or phrase), a proposition (which usually follows more easily from known facts than a theorem does), or a corollary (which follows immediately from facts recently proven).

The discipline of logic formalizes the notion of proof, but not the notions of “interest” or “immediacy”. Thus, to a logician, any proved statement is often called a theorem. (Mathematicians know this meaning too, but still usually reserve the term ‘theorem’ for important theorems in their published work.) The term ‘proposition’, to a logician, means any statement and does not imply the existence of a proof. The term ‘axiom’ is used in a way that somewhat matches its ordinary usage, but as a logician counts trivial proofs as proofs, an axiom is also a special case of a theorem. Logic rarely studies definitions explicitly, but in some theories they do play a role, similar to their informal usage. The other terms appear not to be used in logic.

Definition

In a given logic, in a given context, we have various propositions and various proofs of propositions. In that context, a theorem is a proposition with a proof.

Classically, a theorem is a proposition for which there exists a proof, but in some contexts (such as, perhaps, fully formalized constructive type theory), one may use “theorem” to mean a proposition together with a proof.

A theorem should be contrasted with a tautology: a proposition that is true in all models. If every theorem in a given logic is a tautology in a given class of models for that logic, then we say that the class of models is sound for that logic; if conversely every tautology is a theorem, then we say that the class of models is complete.

Examples

… we might list famous important theorems/lemmas/etc in the nnLab here …

Quotations

• A mathematician is a device for turning coffee into theorems. —Alfréd Rényi

• Lemmas do the work in mathematics: Theorems, like management, just take the credit. —Paul Taylor

References

• Thomas Hales, Formal proof (pdf)

• John Harrison, Formal proof – theory and practice (pdf)