The Theorems · what logic discovered
The results
Concepts are the vocabulary; theorems are the discoveries. The landmark results of logic, each stated in real notation and wired to the mind who proved it and the field it reshaped.
- The Syllogism (Barbara) القياس (الشكلُ الأول) c. 350 BCE
Valid deduction reduced to form: two universal premises sharing a middle term force a universal conclusion.
- Cantor’s Theorem مبرهنةُ كانتور 1891
No set can be mapped onto its own power set, so there are infinitely many distinct sizes of infinity.
- Löwenheim–Skolem مبرهنةُ لوفنهايم–سكولم 1920
A countable first-order theory with an infinite model has models of every infinite cardinality, including unintended ones.
- Completeness Theorem مبرهنةُ الاكتمال 1929
In first-order logic, semantic truth and formal provability coincide exactly: what is valid can be proved.
- Compactness Theorem مبرهنةُ التراصّ 1930
A set of first-order sentences has a model iff every finite subset does: the engine of model theory.
- First Incompleteness عدمُ الاكتمال الأول 1931
Any consistent system strong enough for arithmetic contains a true sentence it cannot prove.
- Second Incompleteness عدمُ الاكتمال الثاني 1931
No such system can prove its own consistency. Certainty about a system must come from outside it.
- Tarski’s Undefinability لاتعريفيةُ تارسكي 1933
Arithmetical truth cannot be defined inside arithmetic itself. Truth always outruns its own language.
- Cut-Elimination (Hauptsatz) حذفُ القطع 1935
Every sequent proof can be rewritten without the cut rule: a proof never needs a detour through a lemma.
- Undecidability of the Halting Problem عدمُ قابلية مسألةِ التوقّف للبَتّ 1936
No algorithm can decide, for every program, whether it halts, nor whether a first-order sentence is valid.
- Consistency of Arithmetic اتساقُ الحساب 1936
Peano arithmetic’s consistency is provable using transfinite induction up to ε₀, exactly measuring its strength.
- Independence of the Continuum Hypothesis استقلالُ فرضية المتّصل 1963
The continuum hypothesis can be neither proved nor refuted from ZFC: settled by Gödel and Cohen together.
- Lindström’s Theorem مبرهنةُ ليندستروم 1969
First-order logic is the strongest logic that has both compactness and the Löwenheim–Skolem property: a portrait of its limits.
- Curry–Howard Correspondence تناظرُ كَري–هاوَرد 1969
Proofs and programs are literally the same objects: to prove is to compute, and logic and computation are one.