It’s “Gödel’s proof of God’s existence”, which was computerised by Christoph Benzmüller at the Free University of Berlin and Bruno Woltzenlogel Paleo at the Vienna University of Technology. A big question is proposed: Can mathematic-logic and computers prove metaphysical problems?

Đó là “Chứng minh của Gödel về sự hiện hữu của Chúa”, đã được thực hiện trên computer bởi Christoph Benzmüller ở Đại học Tự do Berlin và Bruno Woltzenlogel Paleo ở Đại học Công nghệ Vienna. Vấn đề lớn đặt ra: Toán học và computer có thể chứng minh các bài toán của siêu hình học?

Lịch sử ngày nay biết rằng Kurt Gödel, tác giả của Định lý Bất toàn nổi tiếng, có một công trình toán học nổi tiếng không kém về bản thể luận (Ontology) – đó là chứng minh của ông về sự hiện hữu của Chúa, mà sách báo tiếng Anh ngày nay gọi là “Gödel’s Ontological Proof” hoặc “Gödel’s Proof of God’s Existence”.

Mãi cho đến năm 1970, tức là 8 năm trước khi mất, Gödel mới tiết lộ cho bạn bè biết rằng ông có một chứng minh như thế, mặc dù phiên bản đầu tiên của chứng minh này của ông có niên đại khoảng 1941. Điều này cho thấy Gödel rất thận trọng trong việc công bố công trình này. Điều này rất dễ hiểu – thời đại của Gödel là thời đại thắng thế của chủ nghĩa vô thần. Là một nhà toán học logic sâu sắc hơn ai hết, Gödel hiểu rõ rằng ông chỉ có thể công bố những gì mà người đời khó có thể tranh cãi với ông. Hơn nữa, năm 1970 cũng là lúc Gödel cảm thấy mình không còn dư dật thời gian để nói với người đời một vấn đề hệ trọng như vấn đề chứng minh Chúa hiện hữu, và do đó ông quyết định tiết lộ công trình này.

Tháng 02/1970, ông cho phép Dana Scott sao chép một phiên bản của chứng minh và được lưu hành riêng tư.

Tháng 08/1970, Gödel nói với Oskar Morgenstern rằng ông “hài lòng” với chứng minh, nhưng Morgenstern ghi trong nhật ký ngày 29/08/1970 rằng Gödel sẽ không xuất bản vì ông sợ người khác có thể nghĩ “rằng ông thực sự tin vào Chúa”, trong khi ông chỉ thử sử dụng logic toán học để chứng minh những sự kiện của siêu hình học mà thôi. Tuy nhiên, nhiều tài liệu khác cho thấy Gödel thực sự tin vào Chúa, và nhận xét của Morgenstern là không đúng.

Thật vậy, trong những bức thư gửi cho mẹ, Gödel đã thảo luận rất nhiều về niềm tin vào thế giới sau sự sống (afterlife / life after death). Ông nói:

“Thế giới là hợp lý”, và “nếu thế giới được cấu trúc một cách hợp lý thì ắt phải có một cái gì đó như là sự sống đời sau”. Gödel mô tả tôn giáo của mình là “một người theo đạo Tin Lành (Lutheran) đã được rửa tội”, “Niềm tin của tôi là hữu thần như Leibniz, chứ không phải phiếm thần như Spinoza”

Gödel mất ngày 14/01/ 1978. Sau khi ông mất, người ta tìm thấy một phiên bản khác của chứng minh, hơi khác so với phiên bản ông đã tiết lộ cho Scott. Cuối cùng, năm 1987, phiên bản này đã được xuất bản cùng với phiên bản của Scott.

Năm 2013, chứng minh của Gödel đã được hai nhà khoa học computer là Christoph Benzmüller ở Đại học Tự do Berlin và Bruno Woltzenlogel Paleo ở Đại học Công nghệ Vienna biến thành một bài toán trên computer và cho chạy thử, KẾT QUẢ HOÀN TOÀN MỸ MÃN. Hai ông đã công bố công trình của mình trên những tạp chí chuyên ngành khoa học computer, dưới tiêu đề sau đây:

“Formalization, Mechanization and Automation of Gödel’s Proof of God’s Existence” (Hình thức hóa, Cơ giới háo và Tự động hóa Chứng minh của Gödel về sự hiện hữu của Chúa).

Công trình này đã gây chấn động dự luận thế giới vì hai lý do:

●        Một, nó chỉ ra rằng computer có thể tự động hóa các chứng minh toán học.

●        Hai, logic toán học có thể biến những bài toán của triết học siêu hình thành một khoa học chính xác. Đây chính là việc Gödel đã làm, và hy vọng chứng minh của ông chính là một hình mẫu cho một thứ triết học và thần học mới mà ông gọi là “triết học và thần học khoa học” (scientific philosophy and theology).

Sau đây là toàn văn công trình khoa học computer của C. Benzmüller và B. W. Paleo:

 

Formalization, Mechanization and Automation

of

Gödel’s Proof of God’s Existence[1]

Christoph Benzmüller (1) and Bruno Woltzenlogel Paleo (2)

(1) Dahlem Center for Intelligent Systems, Freie Universitat Berlin, Germany c.benzmueller@gmail.com

(2) Theory and Logic Group, Vienna University of Technology, Austria bruno@logic.at

 

Update (31/08/2017): The abstract below, uploaded to arXiv on 21/08/2013, was the first communication of the computer-assisted formalization of Gödel’s ontological proof. Since then, the following longer papers have been published:

[11,10,19,13,12,8,7,16,15,14,17,9,18,20,3,38,29,21,28].

Attempts to prove the existence (or non-existence) of God by means of abstract ontological arguments are an old tradition in philosophy and theology. Gödel’s proof [30,31] is a modern culmination of this tradition, following particularly the footsteps of Leibniz. G¨odel defines God as a being who possesses all positive properties. He does not extensively discuss what positive properties are, but instead he states a few reasonable (but debatable) axioms that they should satisfy. Various slightly different versions of axioms and definitions have been considered by Gödel and by several philosophers who commented on his proof (cf. [36,2,27,1,26]).

Dana Scott’s version of Gödel’s proof [35] employs the following axioms (A), definitions (D), corollaries (C) and theorems (T), and it proceeds in the following order[2]:

Scott’s version of Gödel’s proof has now been analysed for the first-time with an unprecedent degree of detail and formality with the help of theorem provers; cf. [40,39]. The following has been done (and in this order):

– A detailed natural deduction proof.

– A formalization of the axioms, definitions and theorems in the TPTP THF syntax [37].

– Automatic verification of the consistency of the axioms and definitions with Nitpick [24]. – Automatic demonstration of the theorems with the provers LEO-II [6] and Satallax [25]. – A step-by-step formalization using the Coq proof assistant [22]. – A formalization using the Isabelle proof assistant [34], where the theorems (and some additional lemmata) have been automated with Sledgehammer [23] and Metis [33].

Gödel’s proof is challenging to formalize and verify because it requires an expressive logical language with modal operators (possibly and necessarily) and with quantifiers for individuals and properties. Our computer-assisted formalizations rely on an embedding of the modal logic into classical higher-order logic with Henkin semantics [5,4]. The formalization is thus essentially done in classical higher-order logic where quantified modal logic is emulated.

In our ongoing computer-assisted study of Gödel’s proof we have obtained the following results:

– The basic modal logic K is sufficient for proving T1, C and T2.

– Modal logic S5 is not needed for proving T3; the logic KB is sufficient.

– Without the first conjunct φ(x) in D2 the set of axioms and definitions would be inconsistent.

– For proving theorem T1, only the left to right direction of axiom A1 is needed. However, the backward direction of A1 is required for proving T2.

This work attests the maturity of contemporary interactive and automated deduction tools for classical higher-order logic and demonstrates the elegance and practical relevance of the embeddings-based approach. Most importantly, our work opens new perspectives for a computer assisted theoretical philosophy. The critical discussion of the underlying concepts, definitions and axioms remains a human responsibility, but the computer can assist in building and checking rigorously correct logical arguments. In case of logico-philosophical disputes, the computer can check the disputing arguments and partially fulfill Leibniz’ dictum: Calculemus — Let us calculate!

References

1. R.M. Adams. Introductory note to *1970. In Kurt Gödel: Collected Works Vol. 3: Unpublished Essays and Letters. Oxford University Press, 1995.

2. A.C. Anderson and M. Gettings. Gödel ontological proof revisited. In Gödel’96: Logical Foundations of Mathematics, Computer Science, and Physics: Lecture Notes in Logic 6, pages 167–172. Springer, 1996.

3. Matthias Bentert, Christoph Benzmüller, David Streit, and Bruno Woltzenlogel Paleo. Analysis of an ontological proof proposed by Leibniz. In Charles Tandy, editor, Death and Anti-Death, Volume 14: Four Decades after Michael Polanyi, Three Centuries after G.W. Leibniz. Ria University Press, 2016.

4. C. Benzmüller and L.C. Paulson. Exploring properties of normal multimodal logics in simple type theory with LEO-II. In Festschrift in Honor of Peter B. Andrews on His 70th Birthday, pages 386–406. College Publications, 2008.

5. C. Benzmüller and L.C. Paulson. Quantified multimodal logics in simple type theory. Logica Universalis (Special Issue on Multimodal Logics), 7(1):7–20, 2013.

6. C. Benzmüller, F. Theiss, L. Paulson, and A. Fietzke. LEO-II – a cooperative automatic theorem prover for higher-order logic. In Proc. of IJCAR 2008, volume 5195 of LNAI, pages 162–170. Springer, 2008.

7. Christoph Benzmüller. Gödel’s ontological argument revisited – findings from a computer-supported analysis (invited). In Ricardo Souza Silvestre and Jean-Yves B´eziau, editors, Handbook of the 1st World Congress on Logic and Religion, Jo˜ao Pessoa, Brazil, page 13, 2015. (Invited abstract).

8. Christoph Benzmüller, Leon Weber, and Bruno Woltzenlogel Paleo. Computer-assisted analysis of the Anderson-H´ajek ontological controversy. In Ricardo Souza Silvestre and Jean-Yves B´eziau, editors, Handbook of the 1st World Congress on Logic and Religion, Joao Pessoa, Brasil, pages 53–54, 2015. (superseded by 2016 article in Logica Universalis).

9. Christoph Benzmüller, Leon Weber, and Bruno Woltzenlogel Paleo. Computer-assisted analysis of the Anderson-H´ajek controversy. Logica Universalis, 11(1):139–151, 2017.

10. Christoph Benzmüller and Bruno Woltzenlogel Paleo. Gödel’s God in Isabelle/HOL. Archive of Formal Proofs, 2013. (Formally verified).

11. Christoph Benzmüller and Bruno Woltzenlogel Paleo. Gödel’s God on the computer. In S. Schulz, G. Sutcliffe, and B. Konev, editors, Proceedings of the 10th International Workshop on the Implementation of Logics, 2013. (Invited paper).

12. Christoph Benzmüller and Bruno Woltzenlogel Paleo. Automating Gödel’s ontological proof of God’s existence with higher-order automated theorem provers. In Torsten Schaub, Gerhard Friedrich, and Barry O’Sullivan, editors, ECAI 2014, volume 263 of Frontiers in Artificial Intelligence and Applications, pages 93 – 98. IOS Press, 2014.

13. Christoph Benzmüller and Bruno Woltzenlogel Paleo. Gödel’s proof of God’s existence. In Jean-Yves Beziau and Katarzyna Gan-Krzywoszynska, editors, Handbook of the World Congress on the Square of Opposition IV, pages 22–23, 2014. (superseded by ECAI-2014 paper).

14. Christoph Benzmüller and Bruno Woltzenlogel Paleo. Experiments in computational metaphysics: Gödel’s proof of god’s existence. In Subhash C. Mishram, Ramgopal Uppaluri, and Varun Agarwal, editors, Science & Spiritual Quest, Proceedings of the 9th All India Students’ Conference, 30th October – 1 November, 2015, IIT Kharagpur, India, pages 23–40. Bhaktivedanta Institute, Kolkata, http://www.binstitute.org, 2015. (Invited paper, superseded by article in Savijnanam).

15. Christoph Benzmüller and Bruno Woltzenlogel Paleo. Higher-order modal logics: Automation and applications. In Adrian Paschke and Wolfgang Faber, editors, Reasoning Web. Web Logic Rules – 11th International Summer School 2015, Berlin, Germany, July 31 – August 4, 2015, Tutorial Lectures, number 9203 in LNCS, pages 32–74, Berlin, Germany, 2015. Springer.

16. Christoph Benzmüller and Bruno Woltzenlogel Paleo. Interacting with modal logics in the Coq proof assistant. In Lev D. Beklemishev and Daniil V. Musatov, editors, Computer Science – Theory and Applications – 10th International Computer Science Symposium in Russia, CSR 2015, Listvyanka, Russia, July 13-17, 2015, Proceedings, volume 9139 of LNCS, pages 398–411. Springer, 2015.

17. Christoph Benzmüller and Bruno Woltzenlogel Paleo. On logic embeddings and Gödel’s God. In Mihai Codescu, Razvan Diaconescu, and Ionut Tutu, editors, Recent Trends in Algebraic Development Techniques: 22nd International Workshop, WADT 2014, Sinaia, Romania, September 4-7, 2014, Revised Selected Papers, number 9563 in LNCS, pages 3–6, Sinaia, Romania, 2015. Springer. (Invited paper).

18. Christoph Benzmüller and Bruno Woltzenlogel Paleo. The inconsistency in Gödel’s ontological argument: A success story for AI in metaphysics. In Subbarao Kambhampati, editor, IJCAI 2016, volume 1-3, pages 936–942. AAAI Press, 2016.

19. Christoph Benzmüller and Bruno Woltzenlogel Paleo. The modal collapse as a collapse of the modal square of opposition. In Jean-Yves B´eziau and Gianfranco Basti, editors, The Square of Opposition: A Cornerstone of Thought (Collection of papers related to the World Congress on the Square of Opposition IV, Vatican, 2014), http://www.springer.com/us/book/    9783319450612, Studies in Universal Logic. Springer International Publishing Switzerland, 2016.

20. Christoph Benzmüller and Bruno Woltzenlogel Paleo. An object-logic explanation for the inconsistency in Gödel’s ontological theory (extended abstract, sister conferences). In Malte Helmert and Franz Wotawa, editors, KI 2016: Advances in Artificial Intelligence, Proceedings, LNCS, pages 244–250, Berlin, Germany, 2016. Springer.

21. Christoph Benzmüller and Bruno Woltzenlogel Paleo. Experiments in Computational Metaphysics: Gödel’s proof of God’s existence. Savijnanam: scientific exploration for a spiritual paradigm. Journal of the Bhaktivedanta Institute, 9:43–57, 2017.

22. Y. Bertot and P. Casteran. Interactive Theorem Proving and Program Development. Springer, 2004.

23. J.C. Blanchette, S. B¨ohme, and L.C. Paulson. Extending Sledgehammer with SMT solvers. Journal of Automated Reasoning, 51(1):109–128, 2013.

24. J.C. Blanchette and T. Nipkow. Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In Proc. of ITP 2010, number 6172 in LNCS, pages 131–146. Springer, 2010.

25. C.E. Brown. Satallax: An automated higher-order prover. In Proc. of IJCAR 2012, number 7364 in LNAI, pages 111 – 117. Springer, 2012.

26. R. Corazzon. Contemporary bibligraphy on the ontological proof (http://www.ontology.co/biblio/ontological-proof-contemporary-biblio.htm).

27. M. Fitting. Types, Tableaux and Gödel’s God. Kluver Academic Press, 2002.

28. David Fuenmayor and Christoph Benzmüller. Automating emendations of the ontological argument in intensional higher-order modal logic. In KI 2017: Advances in Artificial Intelligence 40th Annual German Conference on AI, LNAI. Springer, 2017.

29. David Fuenmayor and Christoph Benzmüller. Types, Tableaus and Gödel’s God in Isabelle/HOL. Archive of Formal Proofs, 2017. Formally verified with Isabelle/HOL.

30. K. Gödel. Ontological proof. In Kurt Gödel: Collected Works Vol. 3: Unpublished Essays and Letters. Oxford University Press, 1970.

31. K. Gödel. Appendix A. Notes in Kurt G¨odel’s Hand, pages 144–145. In [36], 2004.

32. A.P. Hazen. On Gödel’s ontological proof. Australasian Journal of Philosophy, 76:361–377, 1998.

33. J. Hurd. First-order proof tactics in higher-order logic theorem provers. In Design and Application of Strategies/Tactics in Higher Order Logics, NASA Tech. Rep. NASA/CP-2003-212448, pages 56–68, 2003.

34. T. Nipkow, L.C. Paulson, and M. Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Number 2283 in LNCS. Springer, 2002.

35. D. Scott. Appendix B. Notes in Dana Scott’s Hand, pages 145–146. In [36], 2004.

36. J.H. Sobel. Logic and Theism: Arguments for and Against Beliefs in God. Cambridge U. Press, 2004.

37. G. Sutcliffe and C. Benzmüller. Automated reasoning in higher-order logic using the TPTP THF infrastructure. Journal of Formalized Reasoning, 3(1):1–27, 2010.

38. B. Woltzenlogel Paleo. Leibniz’s characteristica universalis and calculus ratiocinator today. In Charles Tandy, editor, Death and Anti-Death, Volume 14: Four Decades after Michael Polanyi, Three Centuries after G. W. Leibniz. Ria University Press, 2016.

39. B. Woltzenlogel Paleo and C. Benzmüller. Computational philosophy repository(https://gitlab.com/aossie/ComputationalPhilosophy/).

40. B. Woltzenlogel Paleo and C. Benzmüller. Formal theology repository(https://github.com/FormalTheology/GoedelGod)

---

[1] This work has been supported by the German Research Foundation under grant BE2501/9-1.

[2] A1, A2, A5, D1, D3 are logically equivalent to, respectively, axioms 2, 5 and 4 and definitions 1 and

3 in Gödel’s notes [30,31]. A3 was introduced by Scott [35] and could be derived from Gödel’s axiom 1

and D1 in a logic with infinitary conjunction. A4 is a weaker form of Gödel’s axiom 3. D2 has an extra

conjunct φ(x) lacking in Gödel’s definition 2; this is believed to have been an oversight by Gödel [32].