Теоретико-доказательная семантика

редактировать

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

Содержание

  • 1 Обзор
  • 2 См. также
  • 3 Ссылки
  • 4 Внешние ссылки

Обзор

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

Даг Правиц расширил понятие Гентцена аналитического доказательства до естественного вывода, и предположил, что ценность доказательства в естественной дедукции может пониматься как его нормальная форма. Эта идея лежит в основе изоморфизма Карри – Ховарда и теории интуиционистского типа. Его ложь лежит в основе большинства современных объяснений теоретико-доказательной семантики.

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

См. Также

Ссылки

Внешние ссылки

Последняя правка сделана 2021-06-02 08:11:27
Содержание доступно по лицензии CC BY-SA 3.0 (если не указано иное).
Обратная связь: support@alphapedia.ru
Соглашение
О проекте