В Степин - Новая философская энциклопедия. Том первый

• Название: Новая философская энциклопедия. Том первый
• Автор: В Степин
• Издательство: МЫСЛЬ
• Жанр: Философия
• Год: 2010
• ISBN: 978-2-244-01115-9

Введите сюда краткую аннотацию

---

ДОКАЗАТЕЛЬСТВ ТЕОРИЯ— раздел современной математической логики, изучающий свойства и преобразования формальных доказательств, т.е. формальных объектов, синтаксическая правильность которых гарантирует семантическую. Это определение унифицирует множество разнородных понятий формального доказательства, существующих в математической логике: последовательности формул, графы, диаграммы и т. д. В некоторых областях современного общества понятие доказательства стало практически тоже формальным. В частности, понятие документа в юриспруденции включает в себя прежде всего правильность его формы, которая делает его содержание истинным по определению. Однако формальное определение доказательства может в некоторых случаях быть содержательно неадекватным. Часто составленный по всей форме документ прикрывает результат абсолютно незаконных действий либо обмана. Доказательств теория первоначально появилась в связи с программой Гильберта (см. Формализм), с задачей обоснования того, что каждый формальный вывод содержательно интерпретируемого (реального) утверждения дает содержательно правильный результат, включающий в случае необходимости и соответствующее построение. Одним из шагов по направлению к данной цели казалось доказательство непротиворечивости формальных теорий. Это средство незаметно подменило собой цель, и поэтому первым громко прозвучавшим результатом теории доказательств была теорема Геделя о неполноте и ее следствие — о недоказуемости непротиворечивости. Важным позитивным результатом является теорема Я. С. Новикова: утверждение о существовании результата алгоритмического построения, доказанное в классической арифметике, дает верное следствие, и в том числе (грубую) оценку числа необходимых шагов построения. Эта теорема стала основой целого класса результатов современной теории доказательств, обосновывающих совпадение классической истинности и конструктивной обоснованности для многих видов утверждений (в последнее время такие результаты все чаще доказываются методами моделей теории). Следующим шагом в развитии теории доказательств, надолго предопределившим ее магистральное направление, стала формулировка Г. Генценом исчисления секвенций и естественного вывода и доказательство им теоремы нормализации для классического и интуиционистского исчисления секвенций. Содержательно теорема нормализации означает возможность перестроить любой формальный вывод в нормализованный вывод без лемм. Было ясно, что понятие нормализованного вывода применимо и к естественному выводу, но точную формулировку дал только Д. Правиц (1965). Хотя формально определение Правица является сложным, содержательный смысл его вполне прозрачен. Логических правил для каждой связки обычно два: правило ее введения, показывающее, как доказывать утверждения данного вида, и правило удаления, показывающее, как их применять. Напр., для импликации в классической и во многих других логиках правила имеют вид: Допустим А В, исходя из А А,А=>В А^В В Во втором из данных правил формула А => В используется именно как импликация, формула же А не анализируется и может быть любой. Для того чтобы подчеркнуть данный факт, А => В называется главной посылкой правила удаления импликации. В выводе есть окольный путь, если результат правила введения используется как главная посылка в соответствующем правиле удаления, а такая пара правил называется вершиной окольного пути. Если в выводе нет вершин окольных путей, то он называется прямым либо нормализованные. Теорема нормализации гласит, что любой вывод можно перестроить в нормализованный. Длительное время разные формы нормализации являлись ведущей темой исследований в теории доказательств. Расширялся класс исчислений и теорий, для которых устанавливалась норма- лизуемость выводов. Сейчас она обоснована для теории типов и для множества неклассических логик. Устанавливались и оценки соотношения длины нормализованного и исходного выводов. Здесь была подтверждена правота Гильберта о необходимости идеальных объектов для реальных результатов. В частности, В. А. Оревков построил пример последовательности формул, таких, что доказательство я-й формулы с окольными путями происходит приблизительно за 13« шагов, а нормализованный вывод либо вывод методом резолюций должен делать не менее 22" (п раз) шагов. В косвенном доказательстве (п + 1)-й формулы используется промежуточный результат, содержащий в два раза больше связок, чем в доказательстве л-й. В исчислении высказываний оценка увеличения длины вывода чуть «оптимистичней» — она экспоненциальна. В свою очередь изучение свойств самих преобразований, используемых при нормализации выводов, в частности показало, что предложенная Правицем система операций

682

ДОКАЗАТЕЛЬСТВ ТЕОРИЯ устранения вершин окольных путей обладает свойством полной недетерминированности: независимо от порядка применения операций за конечное число шагов получается нормшшзованный вывод. Но сам результирующий вывод существенно зависит от порядка применения шагов. В последнее время на стыках между теорией доказательств и информатикой появились новые классы результатов. Во-первых, выяснилось, что структуры доказательств и структуры извлекаемых из них построений, записанных на алгоритмическом языке достаточно высокого уровня (допускающем работу с значениями высших типов; так что Pascal и С этим требованиям не удовлетворяют), тесно связаны. Построение мономорфно вкладывается в доказательство, а часть доказательства, получающаяся отбрасыванием шагов и формул, нужных лишь для обоснования результата, изоморфна программе. Далее, были рассмотрены соотношения между преобразованиями доказательств и скрытых в них программ. Оказалось, что нормализация соответствует вычислению программы в символьной форме (т. е. когда.проделываются все вычисления и преобразования выражений, которые не зависят от входных данных). Оптимизирующие преобразования программ в свою очередь подсказали новые классы преобразований доказательств, ориентированные на устранение избыточностей. Лит.: Клини С. К. Введение в метаматематику. М., 1957; Та- кеути Г. Теория доказательств. М., 1978. Я. Н. Непейвода, В, А. Смирнов

ДОКАЗАТЕЛЬСТВО ВАРАБО-МУСУЛЬМАНСКОЙ ФИЛОСОФИИ, а также в религиозно-правовой мысли (фикх) понимается на основе соотнесения получаемого или оцениваемого знания с троичной градацией степеней его достоверности: «уверенность» (йакйн), «мнение» (занн), «сомнение» (шакк; см. Знание). В качестве доказательства в философии рассматриваются способы получения «уверенного» знания, в фикхе — то, что дает «уверенное» знание и «мнение». Несмотря на общность терминологии, сами «уверенность» и «мнение» понимаются по-разному в философии и фикхе: «мнение» во втором случае ближе к тому, что философия называет «уверенностью», нежели «мнением». Доказательность знания, наличного или получаемого, связывается в самом широком плане с его ясностью. Среди терминов, которыми в философии, фикхе и филологии обозначается доказательство в общем смысле, многие происходят от корня б-й-н, передающего эту идею (байан, табййн, баййина). Ясность достигается разными путями, в соответствии с чем можно в целом разделить способы доказательства на недискурсивные и дискурсивные. Первые не предполагают процедур перехода от наличного знания к искомому и соответственно необходимости орудий такого перехода, вторые в них нуждаются. С этим связана в целом устойчиво признаваемая и в философии, и в фикхе предпочтительность недискурсивных способов доказательства в сравнении с дискурсивными. Не нуждающимися в доказательстве признавались ясные для ума априорные истины ('ава'ил ал-'акл) типа «целое больше части», а также «врожденное знание» (фитриййат), которым любая душа обладает независимо от своего желания. Близким к последнему можно считать понятие «неизбежное знание» ('илм идтирар, 'илм дарурийй), в которое некоторые мута- каллимы включали, в частности, знание о наличии Творца. Помимо отмеченных наиболее общими терминами для доказательства служат «далала» (указание), однокоренное «истидлал» (руководство указанием), а также «худджа» (аргумент). Термином «бурхан» обозначается аподейк- тическое доказательство в логике. Хотя были найдены стоические аналоги для понимания «далала» (напр., дым является «признаком» — 'амара — огня, доказывающим его наличие), этот термин в арабо-мусульманской мысли значительно шире своего возможного прототипа. Понимание далала тесно связано и с классической теорией указания на смысл, в которой связь между «выговоренностью» (лафз) и «смыслом» (ма'нан), а также между «состоянием вещей» (насба) и смыслом считается, во-первых, сущностной, а не случайной (а потому разводится с указанием «знака» — «'алам» на «означаемое» — «мадлул», которое- случайно и может быть установлено произвольным образом) и, во-вторых, улавливаемой ясно и безошибочно и по сути дела непосредственно (см. Смысл). В фикхе в качестве источников «уверенного» знания рассматриваются Коран и сунна, точнее, только те их положения, которые в результате длительной работы по различению «отменяющих» (насих) и «отмененных» (мансух), «ясных» (мухкамат) и «неясных» (муташабихат) аятов Корана и их взаимного отношения, классификации хадисов по степеням достоверности и установления их отношения к кораническим аятам были признаны в качестве незыблемых норм (насс, букв, —текст). Соответственно «доказательство от текста» (далалат ан-насс) считается прямым свидетельством истины, перевешивающим все прочие. Хотя вычленение незыблемых норм-насс из текста Корана и сунны включает дискурсивные элементы, сами по себе такие нормы являются недискурсивным доказательством. Разновидностью недискурсивного доказательства в фикхе можно считать «единогласие» (иджма'), хотя этот метод оценивается ниже далалат ан-насс и даже дискурсивного кийас (соизмерение), в основном в связи с сомнением в возможности его безошибочного установления. В философии также исследуются пути недискурсивного достижения абсолютной несомненности. Она связывается с возможностью «соединения» (иттисал) субъекта и объекта познания в силу их тождественности. Ибн Cum разрабатывает в этом направлении понятие «хадс» (интуиция), вслед за ним ас-Сухравардй говорит о непосредственной и полной «явленности» (зухур) «яйности» ('ана'иййа) человека самому себе. Близким можно считать понятие «завк» (вкушение) в суфизме, хотя в него, в отличие от авиценновского и ишракистского понимания «явленности», может включаться и постижение сенси- бельного. Хотя такая явленность не является доказательством в привычном смысле слова, она прямо связывается с пониманием очевидности и ясности как обладающими высшей доказательной силой. Кроме того, недискурсив- ность гарантирует от ошибок, связанных с неправильным применением дискурсивных методов доказательства или ошибочностью их исходных посылок. В исмаилизме недискурсивность доказательства связывается скорее с его авторитетным характером, нежели с ясностью: «цело- купное» (куллиййа) метафизическое знание, полученное избранными единицами благодаря горней «поддержке» (та'йид), само не нуждается в доказательстве и служит основой всякого доказательства, которое сводится к детализации и конкретизации этого знания.