[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.