„ღმერთი ცოცხალია", „გიოდელი მართალი იყო", „მათემატიკოსებმა ღვთის არსებობა დაამტკიცეს" – ბოლო სამ თვეში მსგავსი სათაურის მქონე სტატიები სამოცდაათზე მეტმა ბეჭდურმა თუ ინტერნეტგამოცემამ გამოაქვეყნა, დაწყებული Frankfurter Allgemeine Zeitung-ით და დამთავრებული ინტერნეტჟურნალით Неужели?
ასეთი ინტერესის აღძვრის მიზეზი ორგვერდიანი სტატიაა, რომელიც აგვისტოს ბოლოს arxiv.org-ზე გამოქვეყნდა და რომლის ავტორები მათემატიკოსები, კომპიუტერული ლოგიკის სპეციალისტები არიან: ქრისტოფ ბენცმიულერი ბერლინის თავისუფალი უნივერსიტეტიდან და ბრუნო ვოლცენლოგელ პალეო ვენის ტექნიკური უნივერსიტეტიდან. სტატია მოკლედ აღწერს ღვთის არსებობის გიოდელისეული ონტოლოგიური მტკიცებულების ფორმალიზაციას ლოგიკურ განსაზღვრებებში, აქსიომებსა და თეორემებში. თეორემები სპეციალური კომპიუტერული პროგრამების (თეორემათა ავტომატური დამამტკიცებლების, ანუ პრუვერების) მეშვეობითაა დამტკიცებული. მთავარ თეორემას ძალიან მარტივი სახე აქვს: □xG(x), რაც ადამიანურ ენაზე იკითხება, როგორც „ღმერთი აუცილებლად არსებობს".
ონტოლოგიური მტკიცებულების მიზანი სწორედ ასეთი დასკვნის მიღებაა. ესაა ღვთის არსებობის დამამტკიცებელი მსჯელობა, რომელიც დაკვირვებისგან და ცდისგან დამოუკიდებელი, აპრიორული წანამძღვრებიდან ამოდის. ასეთი მსჯელობის პირველ მაგალითად ითვლება მეთერთმეტე საუკუნის ბენედიქტელი ბერის, წმიდა ანსელმ კენტერბერიელის ონტოლოგიური არგუმენტი. ცნობილია დეკარტის, ლაიბნიცის და სხვათა ონტოლოგიური არგუმენტები. თავად ტერმინი „ონტოლოგიური მტკიცებულება" ანუ „ონტოლოგიური არგუმენტი" ეკუთვნის კანტს, ვინც საკმაოდ სკეპტიკურად ეკიდებოდა ამგვარ მცდელობებს.
ბენცმიულერის და პალეოს ნაშრომში ფორმალიზებული ონტოლოგიური არგუმენტი კურტ გიოდელისაა, მე-20 საუკუნის ერთ-ერთი უდიდესი ლოგიკოსის. ამ მტკიცების პირველი ვერსია 40-იანი წლებით თარიღდება, მაგრამ გიოდელს იგი დიდხანს არავისთვის გაუმხელია. მხოლოდ 1970 წელს, როცა ეგონა, რომ კვდებოდა, გაუგზავნა ხელნაწერი პრინსტონის უნივერსიტეტის ფილოსოფიის და მათემატიკის პროფესორს დენა სკოტს. გიოდელი 1978 წელს გარდაიცვალა, ხელნაწერი კი ცხრა წლის შემდეგ გამოქვეყნდა სკოტის მიერ შეტანილი რამდენიმე ცვლილებით.
გიოდელის ონტოლოგიური არგუმენტი მოდალურ ლოგიკაშია ჩამოყალიბებული. ასეთი ლოგიკები აუცილებელ ჭეშმარიტებას შესაძლო ჭეშმარიტებისგან განასხვავებენ. აუცილებლად ჭეშმარიტია წინადადება, თუ ის ყოველთვის, ნებისმიერ გარემოებაში (ანუ, სხვაგვარად, ყველა შესაძლო სამყაროში) ჭეშმარიტია. შესაძლო ჭეშმარიტი წინადადება ჭეშმარიტია ერთ სამყაროში, მაგრამ შეიძლება მცდარი იყოს სხვაში. გიოდელის მტკიცებულება უშვებს ღვთის შესაძლო არსებობას (ანუ ღვთის არსებობის ჭეშმარიტებას რომელიმე სამყაროში) და ლოგიკური გამოყვანის გზით ასკვნის ღვთის აუცილებელ არსებობას (ღვთის არსებობის ჭეშმარიტებას ნებისმიერ სამყაროში).
გიოდელის ამ მსჯელობის სკოტის ვერსია სამ განსაზღვრებას და ხუთ აქსიომას ეყრდნობა. განსაზღვრებები განმარტავენ „ღვთის მსგავსს", როგორც ყველა „დადებითი თვისების" მატარებელს, „ინდივიდის არსს", როგორც ინდივიდის თვისებას, რომლისგანაც ამ ინდივიდის ყველა თვისება გამომდინარეობს, და „ინდივიდის აუცილებელ არსებობას", როგორც ამ ინდივიდის თითოეული არსის მქონე კონკრეტული ობიექტის აუცილებელ არსებობას. დადებითი თვისება განსაზღვრული არაა. იგი მხოლოდ დახასიათებულია აქსიომებით, რომლებიც, კერძოდ, ამბობენ, რომ „ღვთის მსგავსობა" და „აუცილებელი არსებობა" დადებითი თვისებებია, დადებითი თვისებიდან აუცილებლად გამომდინარე თვისებაც დადებითია, დადებითი თვისება აუცილებლად დადებითია, და მისი უარყოფა დადებითი არაა.
ამ წანამძღვრებიდან ღვთის აუცილებელი არსებობის თეორემის დამტკიცება მხოლოდ ტექნიკის საქმეა, მაგრამ გიოდელის ონტოლოგიურ არგუმენტს, ისევე, როგორც სხვა მსგავს არგუმენტებს, კრიტიკა არ მოკლებია. კრიტიკოსები არა თავად დამტკიცების პროცესს, არამედ წანამძღვრებს, ანუ დადებით თვისებათა დამახასიათებელ აქსიომებს არ ეთანხმებოდნენ: რატომ უნდა ჩაითვალოს „ღვთის მსგავსობა" და „აუცილებელი არსებობა" დადებით თვისებებად, როგორც ამას გიოდელი განმარტავს? საიდან ვიცით, რომ არსებობს თეოლოგიურად საინტერესო დადებით თვისებათა სიმრავლე? და თუ არსებობს, საიდან ვიცით, რომ ასეთი სიმრავლე ერთადერთია? ისიც უნდა აღინიშნოს, რომ გიოდელის თავდაპირველ ვერსიაში აქსიომათა სიმრავლე წინააღმდეგობრივი იყო და ეს ხარვეზი მერე სკოტმა აღმოფხვრა.
ასეა თუ ისე, ამ თეორემისადმი მედიის ბოლოდროინდელი ყურადღება ვინმეს შეიძლება ცოტა უცნაურად მოეჩვენოს: მისი პირველი დამტკიცება ხომ ჯერ კიდევ მეოთხედი საუკუნის წინ გამოქვეყნდა. მაგრამ ცხადია, რომ ამ ყურადღების მიზეზი მხოლოდ ის კი არაა, თუ რა დამტკიცდა, არამედ ის, თუ როგორ დამტკიცდა იგი. ეტყობა, ჩაითვალა, რომ მკითხველისთვის ონტოლოგიური არგუმენტი უფრო დამაჯერებელი გახდება, თუ მის დამტკიცებაში თანამედროვე ტექნოლოგიები იქნა გამოყენებული. ალბათ, ამიტომაც გვხვდება ზოგ სტატიაში ისეთი ფრაზები, როგორიცაა „ღვთის არსებობა მაკბუქის მეშვეობით დამტკიცდა", რაც ისევე ღიმილისმომგვრელია, „ვეფხისტყაოსანზე" რომ თქვან, მშვენიერი პოემაა, რადგან თეთრშუბლა ბატის ფრთით დაიწერაო.
წესით, როგორც თეისტებს, ისე ათეისტებს ონტოლოგიურ არგუმენტზე კამათში მოწინავე ტექნოლოგიების მოშველიება ნაკლებად უნდა სჭირდებოდეთ: პირველთ ისედაც სწამთ, მეორენი კი ეჭვს მტკიცების წანამძღვრებში შეიტანენ. ამიტომ ბენცმიულერისთვის და პალეოსთვის, როგორც თავად აღიარეს, მედიის ასეთი ყურადღება საკმაოდ მოულოდნელი აღმოჩნდა. მათთვის გიოდელის არგუმენტის ფორმალიზაცია პირველ რიგში იმით იყო საინტერესო, რომ მოდალური ლოგიკის თეორემების ავტომატური მტკიცებისადმი ახალი მიდგომის პრაქტიკულობაში სურდათ დარწმუნებულიყვნენ. ეს მიდგომა, რომელიც ბენცმიულერის და კემბრიჯის უნივერსიტეტის პროფესორის ლერი პაულსონის იდეას ეყრდნობა, გულისხმობს კვანტორებიანი მოდალური ლოგიკის პრობლემების მაღალი რიგის ლოგიკაში გამოსახვას და შემდეგ მათზე სამსჯელოდ მაღალი რიგის პრუვერების გამოყენებას. გიოდელის არგუმენტის ფორმალიზაციამ და ავტომატურმა დამტკიცებამ ამ მიდგომის ელეგანტურობას გაუსვა ხაზი.
ბენცმიულერის და პალეოს შრომა ასევე აჩვენებს, რომ ავტომატური მსჯელობის სისტემები შეიძლება თეორიული ფილოსოფიის პრობლემებისთვის იქნეს გამოყენებული. ცნებების, განსაზღვრებების და აქსიომების ჩამოყალიბება ადამიანის პრეროგატივაა, ლოგიკური არგუმენტების აგებისთვის, დამტკიცების ჩატარებისთვის, მსჯელობის სისწორის შემოწმებისთვის კი სისტემა შეიძლება დაიხმარონ.
გარდა ამისა, ისიც უნდა ითქვას, რომ დამტკიცების ტექნიკის საილუსტრაციოდ ონტოლოგიური არგუმენტის შერჩევა სწორი ნაბიჯი გამოდგა როგორც თავად ამ ტექნიკის, ისე მთლიანად ავტომატური მსჯელობის დარგის პოპულარიზაციისთვის. ეს უკანასკნელი მათემატიკის და კომპიუტერული მეცნიერებების ქვედარგია, რომლის მიზანია ლოგიკური გამოყვანის ალგორითმების, პროცედურების, მეთოდების შემუშავება და კომპიუტერზე მათი იმპლემენტაცია.
ავტომატურ მსჯელობას გაცილებით პრაქტიკული გამოყენებები აქვს, ვიდრე ეს თეორიულ ფილოსოფიაში არგუმენტების სისწორის შემოწმებაა. მისი როლი უსაფრთხო პროგრამული უზრუნველყოფის და, საზოგადოდ, უსაფრთხო კომპიუტერული სისტემების შექმნაში უფრო და უფრო იზრდება. პროგრამებში დაშვებულ მცირე უზუსტობებსაც კი შეიძლება მძიმე შედეგები მოჰყვეს. ეს თავის თავზე იწვნია ევროპის კოსმოსურმა სააგენტომ 1996 წელს, როცა რიცხვების კონვერტაციისას დაშვებულმა შეცდომამ Ariane-5 რაკეტის თვითგანადგურება გამოიწვია. პროგრამის ერთი არასწორი სტრიქონი სააგენტოს 370 მილიონ დოლარზე მეტი დაუჯდა. როდესაც საქმე სიცოცხლისთვის კრიტიკულ აპლიკაციებს (მაგალითად, სამედიცინო აპარატურას) ეხება, შეცდომებს შეიძლება კიდევ უფრო სავალალო შედეგები მოჰყვეს. ამიტომ კომპიუტერული სისტემების მუშაობის სისწორის მათემატიკურ დამტკიცებას დიდი მნიშვნელობა ენიჭება. ტექნიკურად ეს ურთულესი ამოცანაა. მისი სრულად გადაჭრა, საზოგადოდ, შეუძლებელია. ამ საქმისთვის მსჯელობის კომპიუტერული სისტემების გამოყენება ბევრი პრობლემის ამოხსნას აადვილებს. ის, რის ხელით დამტკიცებასაც ადამიანი დღეებს მოანდომებდა (და დამტკიცების სისწორეში მაინც ვერ იქნებოდა დარწმუნებული), მსჯელობის სისტემამ შეიძლება წამებში გადაწყვიტოს. არაერთ შემთხვევაში ასეთ პროგრამებს ისეთ ჰიპოთეზებზე გაუციათ პასუხი, ადამიანისთვის გადაუჭრელი რომ რჩებოდა. მაგალითად, ჰიპოთეზა, რომ რობინსის ყველა ალგებრა ამავე დროს ბულის ალგებრაცაა, ორმოცდაათი წლის განმავლობაში ვერ გადაწყვიტეს, მიუხედავად ისეთი მათემატიკოსების მცდელობებისა, როგორიც იყვნენ ჰერბერტ რობინსი, ედვარდ ჰანტინგტონი, ალფრედ ტარსკი. ეს ჰიპოთეზა საბოლოოდ ბილ მაკკიუნის პრუვერმა დაამტკიცა ერთკვირიანი გამოთვლების შემდეგ.
ბუნებრივად ისმის კითხვა: რა ვიცით, რომ მსჯელობის სისტემა, რომელსაც სხვა სისტემის სისწორის შესამოწმებლად, ან ღია პრობლემის ამოსახსნელად ვიყენებთ, თავად სწორად მუშაობს? ამ კითხვაზე ერთ-ერთ პასუხს იძლევა დე ბროინის კრიტერიუმი: მსჯელობის სისტემის მიერ მიღებული დამტკიცების ვერიფიკაცია უნდა შეიძლებოდეს სპეციალური შემმოწმებელი პროგრამით, რომელიც, თავის მხრივ, იმდენად მარტივი უნდა იყოს, რომ მის სანდოობაში დარწმუნება განსაკუთრებულ ძალისხმევას არ მოითხოვდეს.
დღეს მსჯელობის ბევრი კომპიუტერული სისტემა ითვლება სანდოდ, მათ შორის ისინი, ბენცმიულერმა და პალეომ რომ გამოიყენეს. ონტოლოგიური არგუმენტების მოწინააღმდეგეებს ამან საეჭვოა, რომ აზრი შეაცვლევინოს, მაგრამ იმაში მაინც დაარწმუნებს, რომ გიოდელი თავის მსჯელობაში არ ცდებოდა.
