info
Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss
[isabelle] Extended version of Gödel’s First Incompleteness Theorem
30 views
Skip to first unread message
Ken Kubota
Jul 8, 2015, 3:57:17 AM7/8/15
to cl-isabe...@lists.cam.ac.uk, Prof. Lawrence C. Paulson, Prof. Peter B. Andrews
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
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
0 new messages