Специальное исчисление высказываний

Специальное исчисление высказываний (секвенций) — построение логической последовательности условных суждений (секвенций) по определённым правилам. В секвенциальном подходе используется аксиома и правила вывода, а доказательство ведётся в форме дерева вывода. Исчисления секвенций относятся к генценовскому типу.

Обозначения

A, B, C — одиночные формулы;

Γ, Г₁, Г₂ — списки формул антецедента, возможно пустые;

A₁, A₂, …, A_m — формулы списка антецедента;

B₁, B₂, …, B_n — формулы списка антецедента;

Ø — пустое множество формул;

├ — знак вывода;

W –– ослабление;

P –– перестановка;

˄ –– конъюнкция;

˅ –– дизъюнкция;

¬ –– отрицание;

→ –– импликация.

Определения

Секвенции (латинское sequentia — последовательность, следствие) — это выражения вида A₁, A₂,..., A_m |- B₁, B₂,..., B_n, где |- — знак выводимости, A₁, A₂,..., A_m и B₂,..., B_n — произвольные формулы; первые — образующие антецедент секвенции, вторые — её сукцедент. Такого рода выражения изучаются в теории доказательств. Они оказываются более удобными для анализа синтаксической структуры выводов. Их называют исчислениями генценовского типа (по имени Генцена, который начал их изучать).

Аксиома

~ аксиома

Основные правила

Дополнительные правила

Примеры секвенций

Доказательства секвенций

Пример_в

Пример_д

Пример_е

Пример_з

Пример_к

Пример_л

Пример_о

Пример_п

Другие понятия:

• Логический закон;
• Логические функции;
• Нормальные формы:
  • совершенная дизъюнктивная нормальная форма;
  • совершенная конъюнктивная нормальная форма;
  • минимальная дизъюнктивная нормальная форма;
  • минимальная конъюнктивная нормальная форма;
  • алгебраическая нормальная форма;
• Таблица истинности;
• Карта Карно;
• Трёхмерная карта Карно;
• Предикат;
• Исчисление высказываний;
• Специальное исчисление высказываний;
• Секвенции;
• Суждение;
• Умозаключения.

Ссылки

• Генцен Г. Исследования логических выводов. В кн. Математическая теория логического вывода, М, 1967, с. 9—74.
• Участник:Logic-samara