Ташнер: що комп’ютер перевірив у «доказі Бога»

У пролозі книжки «У що вірити. 10 пропозицій для освічених людей» Рудольф Ташнер розповідає про логічний доказ існування Бога й пише: «Доказ є цілком коректним і бездоганним». Поруч — згадка про його комп’ютерну перевірку Крістофом Бенцмюллером і Бруно Вольценлогелем Палео. Здається, питання закрите. Але саме тут варто запитати: що перевіряла машина?

Відповідь цікавіша за сенсацію. Перевірити, чи випливає висновок із заданих припущень, — не те саме, що встановити істинність цих припущень. А для такого аргументу важливо ще й уточнити, яку саме версію перевірено.

Маленька правка з великими наслідками

У повідомленні дослідників розібрано версію Геделевого аргументу, запропоновану Даною Скоттом. Автори прямо залишають критичне обговорення понять, визначень та аксіом людям: комп’ютер допомагає будувати й перевіряти логічні виведення.[2]

Різниця між версіями не косметична. У статті 2016 року ті самі дослідники пояснюють суперечність в оригінальній версії Геделя, яку автоматичний доводжувач виявив ще 2013-го. У варіанті Скотта змінено визначення сутності; ця зміна дозволяє уникнути розібраної суперечності. Отже, успішна перевірка одного варіанта не є сертифікатом бездоганності всього, що називають «доказом Геделя».[1]

Це також не спростування існування Бога. Виявлена суперечність стосується певної формальної конструкції. Щоб не підмінити одне питання іншим, треба розрізняти сам предмет віри, спосіб його визначення та правила, за якими з припущень отримують висновок.

Тому формулювання Ташнера потребує уточнення про версію й межі перевірки. Надійніше сказати: дослідники перевірили логічний аргумент за певних визначень та аксіом. Це суттєвий результат, але він не знімає питання, чому приймати саме ці вихідні положення.

Автор теж не ставить знак рівності між доказом і вірою

Було б нечесно звести Ташнера до ефектної фрази про комп’ютер. Уже в тому самому пролозі він пише, що доказ буття Бога не повертає віри в Нього. Його цікавить різниця між формально встановленим існуванням і тим, до кого людина звертається з молитвою.

В епілозі ця відмінність дістає іншу форму. Ташнер звертається до Карла Ясперса: доведене твердження може бути доступним іншим незалежно від особи, яка його обстоює; віра, якою людина живе, пов’язана з її власною позицією. Це філософське розрізнення, а не дозвіл оголосити будь-яку переконаність знанням.

Наприклад, можна особисто триматися певного сенсу життя, не маючи способу нав’язати його всім як теорему. Але якщо поруч з’являється перевірне твердження про світ, особиста важливість не робить його правильним. Потреба у вірі й потреба в доказі не скасовують одна одну — вони відповідають на різні запити.

Як читати ці «пропозиції»

У передмові Ташнер обирає форму есе й попереджає: десять пропозицій не виключають одна одну та не претендують на завершеність. Це запрошення розглянути способи віри, не перелік десяти доведених положень. Водночас жанрова свобода не робить неточність у розповіді про дослідження менш важливою.

З цих обрамлювальних частин варто взяти звичку не перескакувати між трьома твердженнями: «з припущень випливає висновок», «припущення обґрунтовані» та «ця думка має для людини життєвий сенс». Жодне автоматично не замінює решти.

Для українського читача це придатна перевірка повідомлень, у яких авторитет комп’ютера має закрити суперечку. Попросіть назвати точне твердження, вихідні припущення й результат перевірки. Слово «доведено» без цих уточнень залишає забагато роботи уяві.

Книжкове джерело

Рудольф Ташнер. «У що вірити»: передмова; пролог «Математичний доказ існування Бога»; епілог «Віра, яку не можна довести». Прочитано ці частини українського видання; історичні відступи з них не використано як незалежно перевірені факти. Зовнішні праці нижче уточнюють саме комп’ютерну перевірку аргументу.

Зовнішні джерела

[1] https://www.ijcai.org/Proceedings/16/Papers/137.pdf — Benzmüller and Woltzenlogel Paleo — The Inconsistency in Gödel’s Ontological Argument (IJCAI 2016) [2] https://ar5iv.labs.arxiv.org/html/1308.4526 — Benzmüller and Woltzenlogel Paleo — Formalization, Mechanization and Automation of Gödel’s Proof (2013; updated 2017)