Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Understanding Gödel's theorems completely

Email Gateway (Aug 22 2022 at 20:34):

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: Apr 26 2024 at 16:20 UTC