Німецькі вчені підтвердили, що теорема Геделя про існування Бога вірна

Проаналізувавши теореми покійного австрійського математика Курта Геделя за допомогою Macbook, Крістоф Бенцмюллер з Вільного університету Берліна і його колега Бруно Вольценлогел Палео з технічного університету у Відні заявили, що Бог існує.
Справа: знаменитий учений Курт Гедель. Фото: Justin Sullivan / Getty Images
Теорема Геделя заснована на модальної логіки - типі формальної логіки, яка використовує вирази «необхідність» і «можливість».
Бог, або вища істота, існує в мисленні. Але реальне існування більше, ніж існування в думки. Отже, Бог повинен існувати, стверджує Гедель.
Палео і Бенцмюллер стверджують, що його теорема вірна, по крайней мере, на математичному рівні.
Вчені направили на сервер дослідження під назвою «Формалізація, механізація і автоматизація докази Геделя про існування Бога», для того щоб онтологічний доказ Геделя було вперше проаналізовано з високим ступенем деталізації і формальності за допомогою програм автоматичного доведення теорем вищого порядку.
Вчені повідомили, що були проведені наступні дослідження: докладний природне доказ віднімання, формалізації аксіом, визначень і теорем в синтаксисі TPTP ТГФ, автоматична перевірка несуперечності аксіом і визначень з Nitpick, автоматична демонстрація теорем випробувачем LEO-II і Satallax, покрокова формалізація за допомогою програм докази теорем Coq і Isabelle.
Бенцмюллер розповів щотижневому німецькому журналу Der Spiegel, що він захоплений тим, як теореми можуть бути проаналізовані за допомогою комп'ютера.
«Це зовсім дивно, що всі аргументи Геделя можуть бути доведені автоматично, протягом декількох секунд або навіть менше, на стандартному ноутбуці», - сказав він.
Математики кажуть, що їх доказ аксіоми Геделя було потрібно для того, щоб продемонструвати, що передові технології здатні привести до нових досягнень в науці.
«Я не знав, що могло б викликати великий суспільний інтерес, і не знайшов більш кращого прикладу, ніж онтологічний доказ Геделя, раніше недоступне для математики або штучного інтелекту, - сказав Бенцмюллер.- Це дуже маленький, але чіткий приклад, так як ми маємо справа з шістьма аксіомами невеликий теореми. За допомогою потрібних аксіом можна отримати будь-який доказ. Чи можемо ми розвинути комп'ютерні системи до такого рівня, щоб перевіряти кожен крок і переконуватися, що він правильний? »
Вчені вважають, що їх робота може принести користь в таких областях, як штучний інтелект, перевірка програмного забезпечення та апаратних засобів.
Версія англійською
Чи можемо ми розвинути комп'ютерні системи до такого рівня, щоб перевіряти кожен крок і переконуватися, що він правильний?