ИНТУИЦИОНИСТСКИЕ ЛОГИЧЕСКИЕ ИСЧИСЛЕНИЯ

Упражнение 15. Интуиционистские пропозициональные логики

И тут-то котёнок подбежал к немубегом промчался через весь бари стал тереться о его руку и выпрашивать креветку.

Они слишком большие для тебя, котёныш,сказал Томас Хадсон. Но всё же отщипнул пальцами кусочек и подал котёнку, и тот, ухватив его, побежал обратно на витрину табачного прилавка и стал есть быстро и жадно.

Э. Хемингуэй. Острова в океане

Обязательные результаты обучения:

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

Теоретические сведения

Исследования последней четверти XX века в области теоретического программирования выявили особую роль интуиционистской логики в вопросах синтеза программ, поскольку использование этой логики в математических построениях позволяет выделить их алгоритмические, вычислительные аспекты. Поэтому интуиционистская логика является одним из актуальных разделов современной математической логики.

В частности, интенсивно изучается вопрос систематического извлечения программы из конструктивного доказательства теоремы о существовании решения задачи. Постановка этой проблемы уже делает формулы исчисления предикатов и программы однопорядковыми объектами.

Далее обнаруживается, что извлечение эффективной программы из теоремы существования требует добавления к исчислению некоторых нетривиальных посылок, составляющих специальную теорию задачи.

В основе методов решения задачи автоматического синтеза программ лежит следующий план действий:

Постановка задачи —> Теорема существования —>

—> Доказательство теоремы существования —»Программа.

Итак, необходимо уметь реализовывать:

  • 1) трансляцию постановки задачи в формулу специально подобранного логического исчисления, которая в этом исчислении является теоремой, подлежащей доказательству;
  • 2) поиск вывода в этом исчислении;
  • 3) извлечение искомой программы из построенного вывода.

Второй этап является более или менее традиционным.

Первый и третий этапы требуют разработки специальных средств

и методов. Первый этап связан со спецификой проблемной области, в которой решается задача, третий — с характером используемого логического исчисления и применяемых в нём методов доказательства теорем.

Последнее утверждение требует пояснений.

Проблема извлечения программы из доказательства теоремы и вопрос о том, какие доказательства позволяют это, а какие нет, привлекали внимание математиков задолго до появления компьютеров.

Дедуктивные средства, обеспечивающие такое извлечение, стали называться конструктивными дедуктивными средствами, а логики, использующие эти средства, — конструктивными логиками.

Общепринятое «конструктивное» ядро составляют интуиционистские формальные системы, основной характеристикой которых является согласованность с конструктивным пониманием утверждений.

Например, это означает, что:

  • 1) по формальному доказательству утверждения (Ebc е N) Л(х) можно построить натуральное число Ь, для которого верно А(Ь);
  • 2) по формальному доказательству утверждения Vx3yA(x,y) можно построить вычислимую функцию/, для которой верно VxA(x,/(x)), т. е. программу, которая по данному х строит искомое число у =/(х).

Построение программы по доказательству в интуиционистской системе может быть «поручено» компьютеру. При этом размер программы, извлекаемой из доказательства, не намного больше размера самого доказательства.

Подчеркнем тот факт, что извлечение программ из доказательств теорем связано с особенностями конструктивных систем: если использовать классические исчисления, то можно столкнуться с тем, что программа не может быть извлечена из доказательства.

 
Посмотреть оригинал
< Пред   СОДЕРЖАНИЕ   ОРИГИНАЛ     След >