ДОКАЗАТЕЛЬСТВ ТЕОРИЯ


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

Новая философская энциклопедия: В 4 тт. М.: Мысль. . 2001.


Просмотров: 1427
Категория: Словари и энциклопедии » Философия » Философская энциклопедия





Другие новости по теме:

  • "ЧТО ДЕЛАТЬ?"
  • “О НЕОБХОДИМОСТИ И ВОЗМОЖНОСТИ НОВЫХ НАЧАЛ ДЛЯ ФИЛОСОФИИ”
  • “ФИЛОСОФИЯ ДЛЯ ДЕТЕЙ”
  • «ИСКУССТВО ДЛЯ ИСКУССТВА»
  • «ЧТО ДЕЛАТЬ»
  • «ЧТО ТАКОЕ ДРУЗЬЯ НАРОДА И КАК ОНИ ВОЮЮТ ПРОТИВ СОЦИАЛДЕМОКРАТОВ»
  • ВЫВОД ()
  • Город для колесниц
  • Двенадцать Шагов
  • ДЛЯ-МЕНЯ-БЫТИЕ
  • ДЛЯ-СЕБЯ-БЫТИЕ
  • Дорога для Рамы
  • жертвенник для курений
  • Загон для овец, овечий хлев
  • знание-как и знание-что
  • Квота для женщин
  • КЛАСС «В СЕБЕ» И КЛАСС «ДЛЯ СЕБЯ»
  • Кондаков И.М. Методика Для Изучения
  • Конференция Для Священнослужителей Разных Вероисповеданий
  • Кувшин Для Умывания
  • Опросник Для Диагностики Устойчивых Форм
  • Оценка труда работника (для установления заработной платы) (job evaluation)
  • Программы когнитивного вмешательства для пожилых людей (cognitive interventions with older persons)
  • СМИРЕНИЕ, покорность-добродетель, которая может возникнуть от сознания, что совершенство
  • СООБЩЕСТВО АНОНИМНЫХ АЛКОГОЛИКОВ (АА) И ЕГО ПРОГРАММА «12 ШАГОВ»
  • Такие подростки, как правило, зависимы от своих родителей и для них характерны социальная и психологическая незрелость и социальная изоляция.
  • Тесты для отбора кандидатов (selection tests)
  • ФИЛОСОФИЯ ДЛЯ ДЕТЕЙ
  • ЧЕЛОВЕК ДЛЯ СЕБЯ. ИССЛЕДОВАНИЕ ПСИХОЛОГИЧЕСКИХ ПРОБЛЕМ ЭТИКИ
  • Что значит быть летучей мышью?



  • ---
    Разместите, пожалуйста, ссылку на эту страницу на своём веб-сайте:

    Код для вставки на сайт или в блог:       
    Код для вставки в форум (BBCode):       
    Прямая ссылка на эту публикацию:       






    Данный материал НЕ НАРУШАЕТ авторские права никаких физических или юридических лиц.
    Если это не так - свяжитесь с администрацией сайта.
    Материал будет немедленно удален.
    Электронная версия этой публикации предоставляется только в ознакомительных целях.
    Для дальнейшего её использования Вам необходимо будет
    приобрести бумажный (электронный, аудио) вариант у правообладателей.

    На сайте «Глубинная психология: учения и методики» представлены статьи, направления, методики по психологии, психоанализу, психотерапии, психодиагностике, судьбоанализу, психологическому консультированию; игры и упражнения для тренингов; биографии великих людей; притчи и сказки; пословицы и поговорки; а также словари и энциклопедии по психологии, медицине, философии, социологии, религии, педагогике. Все книги (аудиокниги), находящиеся на нашем сайте, Вы можете скачать бесплатно без всяких платных смс и даже без регистрации. Все словарные статьи и труды великих авторов можно читать онлайн.







    Locations of visitors to this page



          <НА ГЛАВНУЮ>      Обратная связь