# [isabelle] Extended version of GÃdelâs First Incompleteness Theorem

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

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*