Войти
В математической логике секвенция - это очень общий вид условного утверждения.
Секвенция может иметь любое количество m условие формулы Ai(называемые «антецеденты ») и любое количество n утвержденных формул B j (называемых «последователями» или «консеквентами »). Под секвенцией понимается то, что если все предшествующие условия верны, то по крайней мере одна из последующих формул верна. Этот стиль условного утверждения почти всегда связан с концептуальной структурой исчисления последовательностей.
Секвенты лучше всего понимаются в контексте следующих трех видов логических суждений :
Таким образом, секвенты являются обобщением простых условных утверждений, которые являются обобщением безусловных утверждений.
Слово «ИЛИ» здесь означает включительное ИЛИ. Мотивация дизъюнктивной семантики в правой части секвенции проистекает из трех основных преимуществ.
Все три из этих преимуществ были определены в основополагающей статье Генценом (1934, стр. 194).
Не все авторы придерживаются первоначального значения слова «секвенция», которое использовал Генцен. Например, Леммон (1965) использовал слово «секвенция» строго для простых условных утверждений с одной и только одной последовательной формулой. Такое же определение секвенции с единственной консеквенцией дано в Huth Ryan 2004, p. 5.
В общей последовательности вида
и Γ, и Σ равны последовательности логических формул, а не наборы. Таким образом, значение имеют как количество, так и порядок появления формул. В частности, одна и та же формула может встречаться дважды в одной и той же последовательности. Полный набор правил вывода последовательного исчисления содержит правила для замены соседних формул слева и справа от символа утверждения (и тем самым произвольно переставить левую и правую последовательности), и также для вставки произвольных формул и удаления дубликатов в левой и правой последовательностях. (Однако Смоллян (1995, стр. 107–108) использует наборы формул в секвенциях вместо последовательностей формул. Следовательно, три пары структурных правил, называемые «прореживание», «сжатие» и «взаимообмен» "не требуются.)
Символ '
Поскольку каждая формула в антецеденте (левая сторона) должна быть истинной, чтобы сделать вывод об истинности хотя бы одной формулы в прецедент (правая сторона), добавление формул к любой из сторон приводит к более слабой секвенции, а удаление их с любой стороны дает более сильную. Это одно из преимуществ симметрии, которое следует из использования дизъюнктивной семантики в правой части символа утверждения, тогда как конъюнктивная семантика соблюдается в левой части.
В крайнем случае, когда список предшествующих формул секвенции пуст, консеквент является безусловным. Это отличается от простого безусловного утверждения, поскольку количество консеквентов произвольно, не обязательно один консеквент. Так, например, «⊢ B 1, B 2 » означает, что либо B 1, либо B 2, либо оба должны быть правда. Пустой список предшествующих формул эквивалентен утверждению «всегда истинное», называемому «verum », обозначаемым «⊤». (См. тройник (символ).)
В крайнем случае, когда список последовательных формул секвенции пуст, правило по-прежнему таково, что хотя бы один член справа должен быть истинным., что явно невозможно. Это обозначено предложением «всегда ложно», называемым «ложным », обозначенным «⊥». Поскольку следствие ложное, по крайней мере, одно из предшествующих должно быть ложным. Так, например, «A 1, A 2 ⊢» означает, что по крайней мере один из предшественников A 1 и A 2 должен быть ложным.
Здесь снова наблюдается симметрия из-за дизъюнктивной семантики с правой стороны. Если левая часть пуста, то одно или несколько предложений правой стороны должны быть истинными. Если правая часть пуста, то одно или несколько левых предложений должны быть ложными.
Двойной крайний случай «», где и предшествующий, и последовательный списки формул пусты, - это «невыполнимо ». В этом случае значение секвенции фактически «⊤ ⊢ ⊥». Это эквивалентно секвенции «⊢ ⊥», которая явно не может быть верной.
Секвенция формы «⊢ α, β» для логических формул α и β означает, что либо α истинно, либо β истинно (или оба). Но это не означает, что либо α - тавтология, либо β - тавтология. Чтобы прояснить это, рассмотрим пример «⊢ B ∨ A, C ∨ ¬A». Это верная секвенция, потому что либо B ∨ A истинно, либо C ∨ ¬A истинно. Но ни одно из этих выражений не является изолированной тавтологией. Разъединение этих двух выражений является тавтологией.
Аналогично, секвенция формы «α, β ⊢» для логических формул α и β означает, что либо α ложно, либо β ложно. Но это не означает, что либо α противоречие, либо β противоречие. Чтобы прояснить это, рассмотрим пример «B ∧ A, C ∧ ¬A ⊢». Это правильная секвенция, потому что либо B ∧ A ложно, либо C ∧ ¬A ложно. Но ни одно из этих выражений не является изолированным противоречием. Противоречие между этими двумя выражениями.
Большинство систем доказательства предоставляют способы вывести одну последовательность из другой. Эти правила вывода записываются со списком секвенций выше и ниже строки. Это правило указывает, что если все, что находится выше линии, верно, то все, что находится под линией, верно.
Типичное правило:
Это означает, что если мы можем вывести, что 
Символ утверждения в секвентах изначально означал то же самое, что и оператор импликации. Но со временем его значение изменилось, чтобы обозначать доказуемость в рамках теории, а не семантическую истину во всех моделях.
В 1934 году Генцен не определял символ утверждения «⊢» в секвенции для обозначения доказуемости. Он определил это как то же самое, что и оператор импликации «⇒». Используя «→» вместо «⊢» и «⊃» вместо «⇒», он написал: «Секвенция A 1,..., A μ → B 1,..., B ν означает, что касается содержания, то же самое, что и формула (A 1... A μ) ⊃ (B 1 ∨... ∨ B ν) ". (Генцен использовал символ стрелки вправо между антецедентами и консеквентами секвенций. Он использовал символ «⊃» для оператора логической импликации.)
В 1939 году Гильберт и Бернейс также утверждал, что секвенция имеет то же значение, что и соответствующая формула импликации.
В 1944 году Алонзо Черч подчеркнул, что секвенции Гентцена не означают доказуемости.
В многочисленных публикациях после этого времени утверждалось, что символ утверждения в секвенциях действительно означает доказуемость в рамках теории, где сформулированы последовательности. Карри в 1963 году, Леммон в 1965 году и Хут и Райан в 2004 году все заявляют, что символ последовательного утверждения означает доказуемость. Однако Бен-Ари (2012, стр. 69) утверждает, что символ утверждения в секвентах системы Генцен, который он обозначает как «⇒», является частью объектного языка, а не метаязыка.
Согласно Prawitz (1965): «Исчисления секвенций можно понимать как метаисчисления для отношения выводимости в соответствующих системах естественного вывода». И более того: «Доказательство в исчислении секвенций можно рассматривать как инструкцию о том, как построить соответствующий естественный вывод». Другими словами, символ утверждения является частью объектного языка для секвенциального исчисления, который является своего рода метаисчислением, но одновременно означает выводимость в лежащей в основе естественной системе вывода.
Секвенция - это формализованное утверждение доказуемости, которое часто используется при указании Calculi для удержание. В исчислении секвенций для построения конструкции используется секвенция, которую можно рассматривать как особый вид суждения, характерный для этой системы дедукции.
Интуитивное значение секвенции 
Конечно, возможны и другие интуитивные объяснения, которые классически эквивалентны. Например,
В любом случае, эти интуитивные прочтения носят исключительно педагогический характер. Поскольку формальные доказательства в теории доказательств являются чисто синтаксическими, значение (получения) секвенции задается только свойствами исчисления, которое обеспечивает действительные правила вывод.
Не допуская каких-либо противоречий в технически точном определении выше, мы можем описывать секвенции в их вводной логической форме.
Общее понятие секвенции, введенное здесь, может быть определено различными способами. Секвенция называется интуиционистской секвенцией, если в последующем есть не более одной формулы (хотя для интуиционистской логики также возможны множественные исчисления). Точнее, ограничение общего исчисления секвенций последовательностями с единственными последовательными формулами с теми же правилами вывода, что и для общих секвенций, составляет интуиционистское исчисление секвенций. (Это ограниченное исчисление секвенций обозначается LJ.)
Точно так же можно получить исчисления для дуальной интуиционистской логики (тип паранепротиворечивой логики ), требуя, чтобы секвенции быть единичным в антецеденте.
Во многих случаях предполагается, что последовательности состоят из мультимножеств или наборов вместо последовательностей. Таким образом, игнорируется порядок или даже количество вхождений формул. Для классической логики высказываний это не составляет проблемы, поскольку выводы, которые можно сделать из совокупности предпосылок, не зависят от этих данных. Однако в субструктурной логике это может стать весьма важным.
Системы естественного вывода используют условные утверждения с одним следствием, но они обычно не используют те же наборы правил вывода, что и Гентцен, введенный в 1934 году. В частности, системы естественного вывода, которые являются очень удобные для практического доказательства теорем в исчислении высказываний и исчислении предикатов, были применены Suppes (1957) harvtxt error: no target: CITEREFSuppes1957 (help ) и Lemmon (1965)) для обучения вводной логике в учебниках.
Исторически секвенты были введены Герхардом Гентценом для уточнения его знаменитого секвенциального исчисления. В своей немецкой публикации он использовал слово «Sequenz». Однако в английском языке слово «последовательность » уже используется как перевод на немецкий «Folge» и довольно часто встречается в математике. Термин «секвенция» был создан в поисках альтернативного перевода немецкого выражения.
Клини делает следующий комментарий к переводу на английский язык: «Гентцен говорит« Sequenz », что мы переводим как« последовательность », потому что мы уже использовали« последовательность »для любой последовательности объектов, где немецкий - «Фольге».
