ИСЧИСЛЕНИЕ СЕКВЕНЦИЙ

- одна из основных форм представления логических систем, применяемая в логике наряду с аксиоматическими системами (гильбертовского типа) и системами натурального (естественного) вывода. Термин «секвенция» происходит от слова sequent (последовательность). Он введен в логику П. Герцем (1929) и заимствован Г. Генценом, который впервые сформулировал в форме исчисления секвенций классическую и интуиционистскую логику предикатов первого порядка.

Исчисление секвенций состоит из двух главных компонентов: основной секвенции и правил заключения (иногда их называют правилами вывода). Основная секвенция в первоначальном генценовском варианте — это секвенция вида А->А, где А — формула, но могут применяться основные секвенции и другого вида. Правила заключения делятся на два типа: логические и структурные. Логические правила заключения в свою очередь делятся на правила введения логического знака в антецедент и правила введения логического знака в сукцедент секвенции. По логическому правилу из формул, входящих в его посылки (боковых формул), в заключении с помощью введения логического знака получается более сложная формула (главная формула). Таким образом, логические правила позволяют строить сложные формулы из более простых. Число логических правил в исчислении секвенций определяется числом используемых в данном исчислении логических констант. Структурные правила (перестановка, сокращение и утончение) влияют не на структуру отдельных формул, а на структуру секвенций. В результате применения этих правил вхождения формул в антецедент или сукцедент секвенции переставляются, сокращаются или добавляются. Логические и структурные правила заключения для классической и интуиционистской логик симметричны в том смысле, что каждому антецедентному (сукцедентному) правилу соответствует в точности одно сукцеденгное (антецедентное) правило.

Это единственное правило, в результате применения которого формула сечения (в данном случае А) вычеркивается из вывода. Все остальные правила сохраняют так называемое свойство подформульности вывода: все формулы, входящие в посылки конкретного правила, являются подформулами некоторых формул, входящих в заключение этого правила.

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

С исчислением секвенций связан полученный Г. Генценом фундаментальный результат современной логики — теорема об устранении сечения, или элиминационная теорема.  В доказательстве этой теоремы Г. Генцен заменяет сечение правилом смешения: » » Г*-» где * и * не содержат формулы А, и показывает, что из любого вывода в исчислении секвенций классической и интуиционистской первопорядковой логики можно устранить все применения этого правила.

Существует множество модификаций первоначального генценовского варианта исчисления секвенций для классической и неклассических логик. Методологически эти модификации сводятся к тому, что изменяется форма или/и число основных секвенций, форма или/и число правил заключения или/и вводятся ограничения на применения конкретных правил заключения при построении дерева вывода. Иногда изменяется само понятие секвенции и используются такие объекты, как «надсеквенции», «кортежи секвенций», «структуры» и т. д. Достаточно прозрачен и эффективен подход к формулировке исчисления, при котором правилам заключения придается «глобальный» характер — их применение зависит не только от вида посылок, но и от состояния выводов этих посылок. Такие правила, в частности, расширяют возможности доказательства теоремы об устранении сечения для неклассических логик.

Исчисления секвенций тесно связаны с табличными представлениями логических систем и обеспечивают естественный переход между синтаксическим и семантическим уровнями анализа неклассических логик. Они являются удобным аппаратом исследования количественных и качественных характеристик логических выводов и процедур поиска логических доказательств. Лит.: Математическая теория логического вывода. М., 1969.

П. И. Быстрое

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




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

  • Аналогии правила
  • Декарт: основные правила научного метода
  • Дидактические правила
  • Культурные правила –
  • Культурные правила выражения эмоций
  • Обращения суждения правила
  • Основные правила
  • Отбора правила
  • ПЕКИНСКИЕ ПРАВИЛА
  • Правила
  • Правила
  • Правила беседы
  • ПРАВИЛА ВОСПИТАНИЯ
  • Правила воспитания
  • Правила воспитания
  • Правила выражения эмоций
  • Правила декодирования
  • ПРАВИЛА И СЛЕДОВАНИЕ ПРАВИЛАМ
  • ПРАВИЛА ИГРЫ
  • Правила игры
  • Правила обучения
  • Правила прохождения обучения
  • Правила проявления эмоций
  • ПРАВИЛА СОЦИАЛИСТИЧЕСКОГО ОБЩЕЖИТИЯ
  • ПРАВИЛА, УСВОЕНИЕ
  • Профессиональное общение: принципы и правила
  • Санитарные правила и нормы
  • САНИТАРНЫЕ ПРАВИЛА И НОРМЫ (СанПиН)
  • Семейные нормы и правила
  • СОЦИАЛЬНЫЕ ПРАВИЛА



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

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






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

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







    Locations of visitors to this page



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