Теорема за Бога

  • Курт Гьодел е австрийски, а след това американски логик, математик и философ. Заедно с Аристотел и Фреге той е смятан за един от най-значителните логици в историята на човечеството. Гьодел има огромен принос в развитието на научно-философското мислене през ХХ век.

    През 1931-ва, когато бил на 25 г., Гьодел публикувал две теореми за непълнотата. Година по-рано получил докторска степен във Виенския университет. За доказателство на първата теорема на Гьодел е разработена методика, преобразуваща формалните изрази в числа.

    Гьодел доказал също така, че нито аксиомата на избора, нито хипотезата за континуума могат да бъдат опровергани чрез приетите теории на множествата, тъй като тези аксиоми се съгласуват. Благодарение на това математиците получили възможност да изследват аксиомата на избора в своите доказателства. Той също внесъл важен принос в теорията на доказателствата с уточняване на връзките между класическата логика, интуиционистката логика и модалната логика.

    Теоремата на Гьодел се основава на модалната логика, вид формална логика, която накратко дефинирана, включва изразите „задължително" и „възможно", според Станфордския университет.

    Според теоремата Бог, или Върховно същество, е това, от което няма по-висше. Бог съществува в това, което определяме като "разбираемо". Ако Бог съществува в "разбираемото", можем да си го представим по-велик, съществуващ в реалността. Ето защо Бог трябва да съществува.

    През октомври 2013 година двама учени – Кристоф Бенцмюлер от Берлинския свободен университет и колегата му Бруно Волценлогел Палео от Техническия университет на Виена – доказали теоремата за съществуването на Бога, създадена от австрийския математик Курт Гьодел, за която вече споменахме.

    Палео и Бенцмюлер твърдят, че са доказали теоремата, поне на математическо ниво.

    При първоначалното представяне на „Сформиране, механизация и автоматизация на доказателството на Гьодел за съществуването на Бог" двамата учени казват, че „онтологичното доказателство на Гьодел се анализира за първи път с безпрецедентна степен на детайлност и строгост с помощта на по-висок разред програми, доказващи теореми.

    Учените добавят: „Извършено бе следното (и в следния ред): Подробно доказателство чрез естествена дедукция. Формализация на аксиоми, дефиниции и теореми в TPTP THF синтаксис. Автоматична проверка на последователността на аксиомите и дефинициите с „Nitpick". Автоматична демонстрация на теоремите с доказващите програми „LEO-II" и „Satallax". Формализация стъпка по стъпка чрез асистент за доказателства „Coq". Формализация чрез асистент за доказателства „Isabelle", където теоремите (и някои допълнителни леми) са били автоматизирани със „Sledgehammer and Metis."

    Бенцмюлер изрази пред „Der Spiegel" възхищението си от това как една теорема може да бъде анализирана посредством математиката.

    „Напълно невероятно е как от този аргумент, поведен от Гьодел, всичко това може да бъде доказано автоматично само за няколко секунди или на обикновен преносим компютър," добави той.

    Според двамата математици тяхното доказателство на аксиомите на Гьодел по-скоро демонстрира как по-добрите технологии могат да допринесат за нови постижения в науката.

    „Не знаех, че това ще предизвика толкова огромен обществен интерес, но (онтологичното доказателство на Гьодел) определено беше по-добър пример от нещо недостъпно в математиката или изкуствения интелект – коментира Бенцмюлер. – Това е нещо малко и свежо, защото се занимаваме само с шест аксиоми в малка теорема. ...Може да има други неща, които използват подобна логика. Можем ли да разработим компютърни системи, които да проверяват всяка една стъпка и да се уверяват, че е правилна?"

    Учените смятат, че тяхната работа може да облагодетелства области като изкуствения интелект и верификацията на софтуера и хардуера.