Formalization, Mechanization and Automation of Gödel's Proof of God's Existence
Особенно понравилось - In case of logico-philosophical disputes, the computer can check the disputing arguments and partially fulfill Leibniz’ dictum: Calculemus — Let us calculate!
Особенно понравилось - In case of logico-philosophical disputes, the computer can check the disputing arguments and partially fulfill Leibniz’ dictum: Calculemus — Let us calculate!
no subject
Date: 2013-09-09 01:43 pm (UTC)no subject
Date: 2013-09-09 02:51 pm (UTC)Скажи пожалуйста, вот твои дети в школу идут с бумажными учебниками или с электронной Book? Как принято? Что ждет укр школьников через 10 лет?
no subject
Date: 2013-09-09 02:59 pm (UTC)no subject
Date: 2013-09-09 03:09 pm (UTC)no subject
Date: 2013-09-10 12:20 pm (UTC)no subject
Date: 2013-09-10 03:55 pm (UTC)Але це не та Теорема Гьоделя, що відома (є дві знамениті математичні теореми Гьоделя, одна більш відома за іншу). Це взагалі не теорема, а спроба формалізації деякого філософського міркування.
no subject
Date: 2013-09-09 07:30 pm (UTC)Я, от офигения (ну никак не думал, что таким образом на такие вещи у нас в стране можно денег насобирать), даже их страничку на Вике этой инфой дополнил.
no subject
Date: 2013-09-10 12:19 pm (UTC)no subject
Date: 2013-09-10 06:01 am (UTC)no subject
Date: 2013-09-10 06:54 am (UTC)Согласен. Какой смысл выкладывать полуторастраничнную аннотацию на архив?!
Товарищи сделали интересную работу, могли бы и нормальную статью написать.
Вот тут, кстати, исходники доказательств лежат https://github.com/FormalTheology/GoedelGod
Там же есть пара интервью на тему:
- https://github.com/FormalTheology/GoedelGod/blob/master/Press%20Releases/SpiegelOnline.pdf?raw=true
- https://github.com/FormalTheology/GoedelGod/blob/master/Press%20Releases/InterviewTelepolis.pdf?raw=true
no subject
Date: 2013-09-10 11:34 am (UTC)После теоремы о неполноте соорудить формализованное доказательство бытия бога - это сильно :)
Кстати, будучи хорошим логиком, Гёдель прекрасно понимал несостоятельность доказательства Лейбница, которое он формализует. Смотри:
D1 A God-like being possesses all positive properties
A5 Necessary existence is a positive property
То есть мы заявили, что Бог имеет все Positive properties. Потом объявили, что существование - это позитивное свойство. Тем самым, по определению D1, бог обладает существованием, то есть существует.
Еще то ли Смаллиан, то ли Гарднер пародировал это доказательство:
Докажем, что граф Дракула (g-D) существует. Для этого, в качестве леммы докажем даже более сильное утверждение, что существующий g-D существует. (ведь если даже существующий g-D существует, то уж какой.нибудь g-D тем более существует, поскольку существующие g-D - это подмножество всех g-D). Итак, есть две и только две альтернативы: (A) существующий g-D существует, и (-A) существующий g-D не существует. Очевидно, -A внутренне противоречиво. Тем самым, А. Таким образом, существование графа Дракулы доказано. Quod erat demonstrandum.
Но развлекаться, а заодно отрабатывать алгоритмы можно, это да.
У Christoph Benzmüller and Bruno Woltzenlogel Paleo с чувством юмора, видимо, тоже все в порядке.
no subject
Date: 2013-09-10 12:18 pm (UTC)no subject
Date: 2013-09-13 01:45 am (UTC)