{ "id": "epb4m87tq3", "slug": "martin-lob", "title": "Martin Löb", "updated": "2026-10-15", "topic_path": [ { "id": "physical", "label": "Physical world and mathematics", "api_url": "https://www.edgepedia.org/api/v1/topics/physical" }, { "id": "physical.scientists", "label": "Physical and mathematical scientists", "api_url": "https://www.edgepedia.org/api/v1/topics/physical.scientists" }, { "id": "physical.scientists.mathematics-statistics", "label": "Mathematicians and statisticians", "api_url": "https://www.edgepedia.org/api/v1/topics/physical.scientists.mathematics-statistics" }, { "id": "physical.scientists.mathematics-statistics.logicians-set-theorists-and-combinatoria", "label": "Logicians, set theorists, and combinatorialists", "api_url": "https://www.edgepedia.org/api/v1/topics/physical.scientists.mathematics-statistics.logicians-set-theorists-and-combinatoria" }, { "id": "physical.scientists.mathematics-statistics.logicians-set-theorists-and-combinatoria.proof-theorists-and-foundational-logicians", "label": "Proof theorists and foundational logicians", "api_url": "https://www.edgepedia.org/api/v1/topics/physical.scientists.mathematics-statistics.logicians-set-theorists-and-combinatoria.proof-theorists-and-foundational-logicians" } ], "geo": [ { "id": "geo.weu.t1946.physical.scientists.mathematics-statistics.logicians-set-theorists-and-combinatoria", "label": "Western Europe · 1946 to 2000: Logicians, set theorists, and combinatorialists", "api_url": "https://www.edgepedia.org/api/v1/geo/geo.weu.t1946.physical.scientists.mathematics-statistics.logicians-set-theorists-and-combinatoria", "path": [ { "id": "geo.weu", "label": "Western Europe", "api_url": "https://www.edgepedia.org/api/v1/geo/geo.weu" }, { "id": "geo.weu.t1946", "label": "Western Europe · 1946 to 2000", "api_url": "https://www.edgepedia.org/api/v1/geo/geo.weu.t1946" }, { "id": "geo.weu.t1946.physical", "label": "Physical world and mathematics", "api_url": "https://www.edgepedia.org/api/v1/geo/geo.weu.t1946.physical" }, { "id": "geo.weu.t1946.physical.scientists", "label": "Physical and mathematical scientists", "api_url": "https://www.edgepedia.org/api/v1/geo/geo.weu.t1946.physical.scientists" }, { "id": "geo.weu.t1946.physical.scientists.mathematics-statistics", "label": "Mathematicians and statisticians", "api_url": "https://www.edgepedia.org/api/v1/geo/geo.weu.t1946.physical.scientists.mathematics-statistics" }, { "id": "geo.weu.t1946.physical.scientists.mathematics-statistics.logicians-set-theorists-and-combinatoria", "label": "Logicians, set theorists, and combinatorialists", "api_url": "https://www.edgepedia.org/api/v1/geo/geo.weu.t1946.physical.scientists.mathematics-statistics.logicians-set-theorists-and-combinatoria" } ] } ], "excerpt": "Martin Hugo Löb (1921–2006) was a German-born mathematical logician who worked in Britain and the Netherlands, best known for Löb's theorem of 1955 and the provability logic GL.", "snippet": "Martin Hugo Löb (1921–2006) was a German-born mathematical logician who worked in Britain and the Netherlands, best known for Löb's theorem of 1955 and the provability logic GL.", "node": "physical.scientists.mathematics-statistics.logicians-set-theorists-and-combinatoria.proof-theorists-and-foundational-logicians", "markdown": "# Martin Löb\n\n**Martin Hugo Löb** (31 March 1921 – August 2006) was a German-born mathematical logician who spent his career in Britain and the Netherlands, best known for [Löb's theorem](https://www.edgepedia.org/lobs-theorem) of 1955 and for developing the Leeds logic group into one of the leading centers in the UK and helping to establish logic at Amsterdam.[1](https://www.theguardian.com/science/2006/oct/03/uk.obituaries) • [2](https://web.archive.org/web/20061223222900/http:/www.ozsl.uu.nl/MartinLob.html) The Association for Symbolic Logic called him \"a central figure in the early development of Mathematical Logic in the United Kingdom.\"[3](https://aslonline.org/files/newsletters/pdfs/april2007newsletter.pdf)\n\n| Key fact | Detail |\n|---|---|\n| Born / died | 31 March 1921; died August 2006 in the Netherlands, aged 85 (21 August per the Guardian and ASL, 28 August per the Amsterdam memorial) [1](https://www.theguardian.com/science/2006/oct/03/uk.obituaries) • [3](https://aslonline.org/files/newsletters/pdfs/april2007newsletter.pdf) • [2](https://web.archive.org/web/20061223222900/http:/www.ozsl.uu.nl/MartinLob.html) |\n| Signature result | Löb's theorem (1955): for a sufficiently strong theory, proving Prov(⌜A⌝) → A entails that it already proves A [4](https://plato.stanford.edu/entries/goedel-incompleteness/) |\n| Doctorate | Ph.D., University of London, 1953, thesis *A Methodological Characterization of Constructive Mathematics*, advised by R. L. Goodstein [5](https://www.mathgenealogy.org/id.php?id=42265) |\n| Leeds | Assistant Lecturer 1951, then Reader and Professor of Mathematical Logic, twenty years [1](https://www.theguardian.com/science/2006/oct/03/uk.obituaries) |\n| Amsterdam | Chair of Mathematical Logic, 1971–1985, in the line of Evert Beth [2](https://web.archive.org/web/20061223222900/http:/www.ozsl.uu.nl/MartinLob.html) • [1](https://www.theguardian.com/science/2006/oct/03/uk.obituaries) |\n| Named after him | The Gödel–Löb provability logic GL, whose axiom is □(□A → A) → □A [6](https://plato.stanford.edu/entries/logic-provability/) |\n\n## Life and career\n\nLöb was brought up in Berlin; the Nazis came to power in 1933, when he was twelve. In 1939, just before the Second World War began, he escaped to England.[7](https://mathshistory.st-andrews.ac.uk/Biographies/Lob/) As a German national he was classed an \"enemy alien\", and in 1940 he was deported on the transport ship *Dunera* to an internment camp at Hay, on the Murrumbidgee River in the Australian outback.[7](https://mathshistory.st-andrews.ac.uk/Biographies/Lob/) • [2](https://web.archive.org/web/20061223222900/http:/www.ozsl.uu.nl/MartinLob.html) There, at age 19, he began learning advanced mathematics and logic at the \"camp university\" set up by the older academic refugees interned alongside him.[3](https://aslonline.org/files/newsletters/pdfs/april2007newsletter.pdf)\n\nThe British government acknowledged its mistake in enforcing the internments, and it was three years before Löb could return to the UK.[1](https://www.theguardian.com/science/2006/oct/03/uk.obituaries) • [7](https://mathshistory.st-andrews.ac.uk/Biographies/Lob/) In 1945 he began a part-time degree at the [University of London](https://www.edgepedia.org/university-of-london) while teaching at a boarding school.[7](https://mathshistory.st-andrews.ac.uk/Biographies/Lob/) A research studentship was advertised to work under R. L. Goodstein at [Leicester](https://www.edgepedia.org/leicester); Löb got it, and his Ph.D. followed, awarded by the University of London in 1953 for the thesis *A Methodological Characterization of Constructive Mathematics*.[1](https://www.theguardian.com/science/2006/oct/03/uk.obituaries) • [5](https://www.mathgenealogy.org/id.php?id=42265)\n\n**Leeds and Amsterdam.** By 1951, at age 30, Löb was an Assistant Lecturer at the [University of Leeds](https://www.edgepedia.org/university-of-leeds), where he stayed twenty years, becoming Reader and then Professor of Mathematical Logic.[1](https://www.theguardian.com/science/2006/oct/03/uk.obituaries) In the early 1970s he accepted the chair of Mathematical Logic at the [University of Amsterdam](https://www.edgepedia.org/university-of-amsterdam), previously held by Evert Beth, and held it from 1971 to 1985, retiring at 65.[2](https://web.archive.org/web/20061223222900/http:/www.ozsl.uu.nl/MartinLob.html) • [1](https://www.theguardian.com/science/2006/oct/03/uk.obituaries) In Amsterdam he and Anne Troelstra occupied the two central logic chairs, succeeding Beth and Heyting; Löb helped create the interdisciplinary *vakgroep* that was the predecessor of today's Institute for Logic, Language and [Computation](https://www.edgepedia.org/computation) (ILLC).[2](https://web.archive.org/web/20061223222900/http:/www.ozsl.uu.nl/MartinLob.html) He died in Annen, in the Dutch province of Drente, after a lengthy illness.[2](https://web.archive.org/web/20061223222900/http:/www.ozsl.uu.nl/MartinLob.html) • [3](https://aslonline.org/files/newsletters/pdfs/april2007newsletter.pdf)\n\n## Löb's theorem\n\nLeon Henkin had asked about sentences that \"express their own provability\": if a sentence says \"this statement is provable in T\", is it provable in T? Löb answered the question in his 1955 paper, showing that, for a sufficiently strong theory T satisfying the relevant derivability conditions (technical axioms a theory must satisfy for provability theorems to apply), such a sentence is indeed provable in T.[7](https://mathshistory.st-andrews.ac.uk/Biographies/Lob/) • [4](https://plato.stanford.edu/entries/goedel-incompleteness/) The paper's general result, now called Löb's theorem, states that for any sentence A of the language of a sufficiently strong theory F satisfying the relevant derivability conditions:\n\n\\[ F \\vdash \\mathrm{Prov}_{F}(\\ulcorner A \\urcorner) \\rightarrow A \\quad \\text{if and only if} \\quad F \\vdash A. \\]\n\nIn plain terms, a sufficiently strong theory satisfying the relevant derivability conditions can prove \"if A is provable then A\" only in the trivial case that the theory already proves A itself.[4](https://plato.stanford.edu/entries/goedel-incompleteness/) • [6](https://plato.stanford.edu/entries/logic-provability/) The theorem is associated with Löb's Paradox, illustrated by the sentence \"if this sentence is true then the moon is made of green cheese\".[2](https://web.archive.org/web/20061223222900/http:/www.ozsl.uu.nl/MartinLob.html)\n\n**Attribution and derivability conditions.** The 1955 paper brought three advances: it introduced the now-standard Löb derivability conditions, a useful simplification of the complicated conditions Hilbert and Bernays had introduced in 1939; it solved Henkin's problem; and it contained the generalization now called Löb's Theorem, which Löb himself credited to the anonymous referee of the paper, who happened to be Henkin.[4](https://plato.stanford.edu/entries/goedel-incompleteness/) Substituting the falsum symbol ⊥ for A in the theorem yields that PA ⊢ ¬Prov(⌜⊥⌝) implies PA ⊢ ⊥, which is exactly the contraposition of Gödel's second incompleteness theorem: the theorem is, in this sense, a strengthening of Gödel's result.[6](https://plato.stanford.edu/entries/logic-provability/)\n\n## Provability logic and its aftermath\n\nThe modal face of Löb's theorem is the axiom □(□A → A) → □A. Adding it to the minimal modal logic K yields the propositional provability logic called **GL**, after Gödel and Löb (alternative names in the literature are L, G, KW, K4W, and PrL).[6](https://plato.stanford.edu/entries/logic-provability/) Ironically, the first statement of the formalized Löb theorem as a modal principle appeared not in arithmetic but in a 1963 paper by T. Smiley on the logical basis of ethics; serious investigation of provability logic began only in the early 1970s.[6](https://plato.stanford.edu/entries/logic-provability/)\n\nThe main modal result about GL is the fixed point theorem, proved independently by Dick de Jongh and Giovanni Sambin in 1975: for any p-modalized formula A(p) there is a fixed point B, unique up to GL-provable equivalence, with GL ⊢ B ↔ A(B), and the fixed point can be found by an effective procedure.[6](https://plato.stanford.edu/entries/logic-provability/) • [8](https://eprints.illc.uva.nl/id/eprint/1774/7/2021.FPT.jb.pdf) The field was consolidated in George Boolos's *The Logic of Provability* ([Cambridge University Press](https://www.edgepedia.org/cambridge-university-press), 1995), a fully rewritten successor to his *The Unprovability of Consistency* (1979), which shows how modal concepts and techniques illuminate [Gödel's incompleteness theorems](https://www.edgepedia.org/godels-incompleteness-theorems) by reinterpreting necessity and possibility as provability and consistency.[9](https://www.cambridge.org/core/books/logic-of-provability/F1549530F91505462083CE2FEB6444AA)\n\n## Wider contributions, students and lineage\n\nAt Leeds, joined briefly by Robin Gandy, Löb established the BA in [Mathematics](https://www.edgepedia.org/mathematics) and [Philosophy](https://www.edgepedia.org/philosophy) and ran the early international conferences that brought distinguished senior logicians such as [Alonzo Church](https://www.edgepedia.org/alonzo-church) and Alfred Tarski to Britain; he developed the Leeds logic group into one of the leading centers in the UK, working on proof theory, modal logic, and computability theory.[1](https://www.theguardian.com/science/2006/oct/03/uk.obituaries) • [7](https://mathshistory.st-andrews.ac.uk/Biographies/Lob/) His published work beyond the 1955 theorem includes \"Extensional interpretations of modal logics\" in the *Journal of Symbolic Logic*, volume 31 (1966), pages 23–45.[10](https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/m-h-lob-extensional-interpretations-of-modal-logics-the-journal-of-symbolic-logic-vol-31-1966-pp-2345/EFAB8663DD6652C4875BFB8E09CCEF0A) His best-known Amsterdam result is the undecidability of intuitionistic second-order propositional logic, even when the language contains only implication and the universal quantifier.[2](https://web.archive.org/web/20061223222900/http:/www.ozsl.uu.nl/MartinLob.html)\n\nThe Mathematics Genealogy Project records 3 students and 431 mathematical descendants.\n\n## By the numbers\n\n- 431 mathematical descendants from 3 students.[5](https://www.mathgenealogy.org/id.php?id=42265)\n- 20 years at Leeds (1951 to the early 1970s) and a 14-year Amsterdam chair (1971–1985).[1](https://www.theguardian.com/science/2006/oct/03/uk.obituaries) • [2](https://web.archive.org/web/20061223222900/http:/www.ozsl.uu.nl/MartinLob.html)\n- The theorem is dated 1955 by most sources, though the Stanford Encyclopedia's provability logic entry dates it to 1953.[4](https://plato.stanford.edu/entries/goedel-incompleteness/) • [6](https://plato.stanford.edu/entries/logic-provability/)\n- Gödel's second incompleteness theorem has been mechanized in a proof assistant only once, by Lawrence Paulson in 2015 in Isabelle; Löb's theorem itself has since been mechanized in Rocq.[11](https://msp-strath.github.io/MSPweb/types2025/slides/TYPES2025-slides17.pdf)\n\n## Recent developments\n\nThe theorem has remained a working tool. A 2023 *Journal of Automated Reasoning* paper implemented the metatheory of GL in the HOL Light proof assistant, covering soundness and completeness for possible-world semantics with a prototype theorem prover, adapting the completeness proof from Boolos's 1995 monograph and overcoming the technical difficulty of GL's non-compactness.[12](https://link.springer.com/article/10.1007/s10817-023-09677-z) A TYPES 2025 presentation reported a mechanized proof of Löb's theorem for first-order arithmetic in the Rocq proof assistant, assuming the HBL derivability conditions and the consistency of the theory.[11](https://msp-strath.github.io/MSPweb/types2025/slides/TYPES2025-slides17.pdf)\n\n**Type theory and AI.** Via the Curry–Howard isomorphism, which identifies formal proofs with abstract syntax trees of programs, Löb's theorem implies that for total programming languages which validate it, self-interpreters are impossible; a research paper formalizes variations of the theorem in Agda.[13](https://jasongross.github.io/lob-paper/nightly/lob.pdf) In AI foundations, a 2024 arXiv paper traces the \"Löbian Obstacle\", the problem named by Yudkowsky and Hereshoff (2013) concerning agents being confident in their own conclusions, to Löb (1955) and to Smullyan's doxastic-logic presentation (1986), and defines \"Löb Safe\" logics for reflective agents.[14](https://arxiv.org/html/2408.09590v2) MIRI's research program cites the 1955 theorem because it illustrates the self-reference involved when an algorithm considers its own output, making it germane to self-modifying agents and formal verification.[15](https://intelligence.org/files/lob-notes-IAFF.pdf)\n\n## References\n\n1. [Martin Löb, obituary by Stan Wainer, The Guardian (3 October 2006)](https://www.theguardian.com/science/2006/oct/03/uk.obituaries)\n2. [Martin Löb (1921–2006), memorial notice, OZSL/ILLC Amsterdam](https://web.archive.org/web/20061223222900/http:/www.ozsl.uu.nl/MartinLob.html)\n3. [In Memoriam: Martin Löb, Association for Symbolic Logic Newsletter, April 2007](https://aslonline.org/files/newsletters/pdfs/april2007newsletter.pdf)\n4. [Gödel's Incompleteness Theorems, Stanford Encyclopedia of Philosophy](https://plato.stanford.edu/entries/goedel-incompleteness/)\n5. [Martin Löb, The Mathematics Genealogy Project](https://www.mathgenealogy.org/id.php?id=42265)\n6. [Provability Logic, Stanford Encyclopedia of Philosophy](https://plato.stanford.edu/entries/logic-provability/)\n7. [Martin Löb, MacTutor History of Mathematics](https://mathshistory.st-andrews.ac.uk/Biographies/Lob/)\n8. [An Abstract Look at the Fixed-Point Theorem for Provability Logic, ILLC preprint](https://eprints.illc.uva.nl/id/eprint/1774/7/2021.FPT.jb.pdf)\n9. [George Boolos, The Logic of Provability, Cambridge University Press](https://www.cambridge.org/core/books/logic-of-provability/F1549530F91505462083CE2FEB6444AA)\n10. [M. H. Löb, Extensional interpretations of modal logics, Journal of Symbolic Logic 31 (1966)](https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/m-h-lob-extensional-interpretations-of-modal-logics-the-journal-of-symbolic-logic-vol-31-1966-pp-2345/EFAB8663DD6652C4875BFB8E09CCEF0A)\n11. [Löb's Theorem and Provability Predicates in Rocq, TYPES 2025 slides](https://msp-strath.github.io/MSPweb/types2025/slides/TYPES2025-slides17.pdf)\n12. [Mechanising Gödel–Löb Provability Logic in HOL Light, Journal of Automated Reasoning (2023)](https://link.springer.com/article/10.1007/s10817-023-09677-z)\n13. [Löb's Theorem (formalized in Agda), Gross et al.](https://jasongross.github.io/lob-paper/nightly/lob.pdf)\n14. [Löb-Safe Logics for Reflective Agents, arXiv (2024)](https://arxiv.org/html/2408.09590v2)\n15. [An Introduction to Löb's Theorem in MIRI Research](https://intelligence.org/files/lob-notes-IAFF.pdf)\n\n---\n*Topic: Encyclopedia › Physical world and mathematics › Physical and mathematical scientists › Mathematicians and statisticians › Logicians, set theorists, and combinatorialists › Proof theorists and foundational logicians*\n\n*Initially written Oct 10, 2026 · Edited: Oct 11, 2026; Oct 15, 2026*\n\n*Copyright 2026 EdgeChat AI, a subsidiary of Biostate AI.*\n\nLicense: Edgepedia Community License 1.0, https://www.edgepedia.org/edgepedia/license\n", "same_as": [], "url": "https://www.edgepedia.org/martin-lob", "markdown_url": "https://www.edgepedia.org/martin-lob.md", "license": { "name": "Edgepedia Community License 1.0", "url": "https://www.edgepedia.org/edgepedia/license", "summary": "Free with credit, commercial use included. AI training is open to everyone. For other uses, organizations over USD 100M in revenue or 100M monthly users license separately.", "spdx": "LicenseRef-Edgepedia-Community-1.0" }, "credit": "\"Martin Löb\", Edgepedia (EdgeChat), https://www.edgepedia.org/martin-lob. Edgepedia Community License 1.0.", "credit_md": "\"[Martin Löb](https://www.edgepedia.org/martin-lob)\", Edgepedia (EdgeChat), [https://www.edgepedia.org/martin-lob](https://www.edgepedia.org/martin-lob). [Edgepedia Community License 1.0](https://www.edgepedia.org/edgepedia/license).", "credit_html": "\"Martin Löb\", Edgepedia (EdgeChat), https://www.edgepedia.org/martin-lob. Edgepedia Community License 1.0.", "speakable": "Martin Hugo Löb was a German-born mathematical logician who worked in Britain and the Netherlands, best known for Löb's theorem of 1955 and the provability logic GL." }