У математичній логіці секвенція — це дуже загальний вид умовних тверджень.

Секвенція може мати довільну кількість формул («антецеденти») та будь-яку кількість («сукцеденти» або «консеквенти»). Секвенція інтерпретується так: якщо всі антецеденти істинні, то принаймні один консеквент також істинний. Така форма умовних тверджень майже завжди використовується в межах концептуального апарату числення секвенцій.

Вступ

Форма та семантика секвенцій

Секвенції можна найкраще зрозуміти в контексті таких трьох видів логічних суджень:

Безумовне твердження. Формула без антецедентів. Приклад: Значення: істинне. Умовне твердження. Формула з будь-якою кількістю антецедентів. а) Просте умовне твердження. Формула з одним консеквентом. Приклад: Значення: Якщо формули , , істинні, тоді теж істинна. б) Секвенція. Формула з будь-якою кількістю консеквентів. Приклад: Значення: Якщо формули , , істинні, тоді АБО АБО АБО теж істинна.

Таким чином, секвенції — це узагальнення простих умовних тверджень, які, у свою чергу, є узагальненням безумовних тверджень.

Слово «АБО» у цьому контексті вживається як диз'юнкція. Мотивація для використання диз'юнктивної семантики в правій частині секвенції випливає з трьох основних переваг: Симетрія класичних правил виведення для секвенцій з такою семантикою. Легкість та простота у зведенні таких класичних правил до інтуїціоністських правил. Можливість довести повноту для числення предикатів, коли «АБО» подане в такому вигляді.

Усі три переваги були знайдені у фундаментальній роботі Ґенцена (1934, с. 194).

Не всі автори дотримувались початкового значення слова «секвенція», яке увів Ґенцен. Наприклад, Леммон (1965) використав слово «секвенція» виключно для простих умовних тверджень з рівно однією формулою. Таке ж означення для секвенції дали Гут та Раян (2004, с. 5).

Синтаксичні подробиці

У загальній формі секвенції:

Символи та — це послідовності логічних формул, не множини. Більше того, кількість та порядок появи формул також мають значення. Зокрема, одна й та сама формула може з'явитись двічі в одній і тій самій послідовності. Повний набір правил перетворень числення секвенцій має правила для перестановки прилеглих формул зліва та справа від символу твердження (що дозволяє довільно переставляти ліві та праві послідовності), а також для вставки довільних формул та вилучення копій з лівої та правої послідовностей. (Проте, Смалліан (1995, с. 107–108) використовує множини формул замість послідовностей формул. Отже, три пари структурних правил: «потоншення», «скорочення» та «перестановка» не обов'язкові.)

Символ '' часто називають «знаком твердження» або «символом твердження». Він часто читається як «доводить» або «спричиняє».

Див. також Ґергард Ґенцен Інтуїціоністська логіка Природне виведення Числення секвенцій

Література