From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Dear Juho,
In addition to the papers mentioned, there is our recent paper (http://www.andreipopescu.uk/pdf/Goedel_CADE_2019.pdf). It provides a pedagogical, top-down formalization of Gödel's theorems in Isabelle/HOL, focusing on the ingredients necessary for a logic to satisfy these theorems.
Outside the formalized work, a classic pedagogical presentation is Smorynski's (https://www.karlin.mff.cuni.cz/~krajicek/smorynski.pdf).
Best wishes,
Andrei
Last updated: Nov 21 2024 at 12:39 UTC