Email Gateway (Aug 22 2022 at 10:50): Email Gateway (Aug 22 2022 at 10:50):From: Ken Kubota <mail@kenkubota.de>
Dear members of the research community,
Please take note of the now extended version of Gödel’s First Incompleteness Theorem, originally by Lawrence C. Paulson.
The following theorem is proved:
{} ⊢ δ <–> {} ⊢ Neg δ
{} \<turnstile> \<delta> \<longleftrightarrow> {} \<turnstile> Neg \<delta>
(Neg delta can be obtained from delta and vice versa.)
The file with the proof (Goedel_I_Extended.thy) is available at: http://dx.doi.org/10.4444/100.102
This extension allows a straightforward comparison of the proofs of Gödel’s First Incompleteness Theorem proposed by Peter B. Andrews and Lawrence C. Paulson respectively.
For this purpose, I also extended the proof by Peter B. Andrews in his system Q0 (resp. Q0^inf).
Kind regards,
Ken Kubota
Last updated: Apr 19 2024 at 04:17 UTC