basic constructions:
strong axioms
further
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
There are good reasons why the theorems should all be easy and the definitions hard. (Michael Spivak, preface to “Calculus on Manifolds” )
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.
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.
… we might list famous important theorems/lemmas/etc in the $n$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
Thomas Hales, Formal proof (pdf)
John Harrison, Formal proof – theory and practice (pdf)
Last revised on May 31, 2022 at 03:24:00. See the history of this page for a list of all contributions to it.