|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-proposition, mere proposition|
|cut rule||composition of classifying morphisms / pullback of display maps||substitution|
|cut elimination for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|logical conjunction||product||product type|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator, (idemponent) monad||modal type theory, monad (in computer science)|
|linear logic||(symmetric, closed) monoidal category||linear type theory/quantum computation|
|proof net||string diagram||quantum circuit|
|(absence of) contraction rule||(absence of) diagonal||no-cloning theorem|
|synthetic mathematics||domain specific embedded programming language|
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.
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.
… we might list famous important theorems/lemmas/etc in the Lab here …
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