Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Löb's theorem

view this post on Zulip Email Gateway (Jul 18 2025 at 14:40):

From: Lawrence Paulson <lp15@cam.ac.uk>
Janis Bailitis has contributed a formalisation of Löb's theorem, building on the existing Incompleteness development. Löb's theorem essentially states that if Provable(“φ”) → φ is formally provable then so is φ itself. It is a generalisation of the second incompleteness theorem, and now has its own chapter (the last).

https://www.isa-afp.org/entries/Incompleteness.html

Last updated: Jul 26 2025 at 12:43 UTC