В математической логике секвенция — это весьма общий вид условного утверждения.
Секвента может иметь любое количество m условных формул A i (называемых « антецедентами ») и любое количество n утверждаемых формул B j (называемых «сукцедентами» или « консеквентами »). Под секвентой понимается то, что если все предшествующие условия истинны, то по крайней мере одна из консеквентных формул истинна. Этот стиль условного утверждения почти всегда связан с концептуальной структурой исчисления секвенций .
Секвенты лучше всего понимать в контексте следующих трех видов логических суждений :
Таким образом, секвенции являются обобщением простых условных утверждений, которые, в свою очередь, являются обобщением безусловных утверждений.
Слово «ИЛИ» здесь является инклюзивным ИЛИ . [1] Мотивация дизъюнктивной семантики в правой части секвенции исходит из трех основных преимуществ.
Все три этих преимущества были определены в основополагающей статье Генцена (1934, стр. 194).
Не все авторы придерживались первоначального значения слова «секвент», данного Генценом. Например, Леммон (1965) использовал слово «секвент» строго для простых условных утверждений с одной и только одной консеквентной формулой. [2] Такое же определение секвента с одним консеквентом дано в работе Huth & Ryan 2004, стр. 5.
В общей последовательности вида
и Γ, и Σ являются последовательностями логических формул, а не множествами . Поэтому как число, так и порядок появления формул имеют значение. В частности, одна и та же формула может появляться дважды в одной и той же последовательности. Полный набор правил вывода секвенциального исчисления содержит правила для обмена соседними формулами слева и справа от символа утверждения (и, таким образом, произвольной перестановки левой и правой последовательностей), а также для вставки произвольных формул и удаления дубликатов копий внутри левой и правой последовательностей. (Однако, Smullyan (1995, стр. 107–108), использует наборы формул в секвенциях вместо последовательностей формул. Следовательно, три пары структурных правил , называемые «прореживание», «сокращение» и «взаимообмен», не требуются.)
Символ ' ' часто называют « турникетом », «правым галсом», «тройником», «знаком утверждения» или «символом утверждения». Его часто читают, намекая, как «уступает», «доказывает» или «влечет за собой».
Поскольку каждая формула в антецеденте (левая сторона) должна быть истинной, чтобы заключить об истинности хотя бы одной формулы в сукцеденте (правая сторона), добавление формул к любой стороне приводит к более слабой секвенции, в то время как их удаление с любой стороны дает более сильную. Это одно из преимуществ симметрии, которое следует из использования дизъюнктивной семантики с правой стороны символа утверждения, тогда как конъюнктивная семантика соблюдается с левой стороны.
В крайнем случае, когда список антецедентных формул секвенции пуст, консеквент является безусловным. Это отличается от простого безусловного утверждения, поскольку количество консеквентов произвольно, не обязательно один консеквент. Так, например, ' ⊢ B 1 , B 2 ' означает, что либо B 1 , либо B 2 , либо оба должны быть истинными. Пустой список антецедентных формул эквивалентен "всегда истинному" утверждению, называемому " verum ", обозначаемому "⊤". (См. Tee (символ) .)
В крайнем случае, когда список консеквентных формул секвенции пуст, правило все еще заключается в том, что по крайней мере один термин справа должен быть истинным, что явно невозможно . Это обозначается предложением «всегда ложно», называемым « falsum », обозначаемым «⊥». Поскольку следствие ложно, по крайней мере один из антецедентов должен быть ложным. Так, например, « A 1 , A 2 ⊢ » означает, что по крайней мере один из антецедентов A 1 и A 2 должен быть ложным.
Здесь снова можно увидеть симметрию из-за дизъюнктивной семантики с правой стороны. Если левая сторона пуста, то одно или несколько предложений с правой стороны должны быть истинными. Если правая сторона пуста, то одно или несколько предложений с левой стороны должны быть ложными.
Дважды крайний случай ' ⊢ ', когда и предшествующий, и последующий списки формул пусты, является « невыполнимым ». [3] В этом случае значение секвенции фактически равно ' ⊤ ⊢ ⊥ '. Это эквивалентно секвенции ' ⊢ ⊥ ', которая явно не может быть допустимой.
Секвента вида ' ⊢ α, β ' для логических формул α и β означает, что либо α истинно, либо β истинно (или оба). Но это не означает, что либо α является тавтологией, либо β является тавтологией. Чтобы прояснить это, рассмотрим пример ' ⊢ 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 ν )». [4] (Гентцен использовал символ правой стрелки между антецедентами и консеквентами секвенций. Он использовал символ ' ⊃ ' для логического оператора импликации.)
В 1939 году Гильберт и Бернайс также заявили, что секвенция имеет то же значение, что и соответствующая формула импликации. [5]
В 1944 году Алонзо Чёрч подчеркнул, что последовательные утверждения Генцена не означают доказуемости.
Многочисленные публикации после этого времени утверждали, что символ утверждения в секвенциях действительно означает доказуемость в рамках теории, в которой сформулированы секвенции. Карри в 1963 году, [7] Леммон в 1965 году, [2] и Хут и Райан в 2004 году [8] все утверждают, что символ утверждения секвенции означает доказуемость. Однако Бен-Ари (2012, стр. 69) утверждает, что символ утверждения в секвенциях системы Генцена, который он обозначает как ' ⇒ ', является частью объектного языка, а не метаязыка. [9]
Согласно Правитцу (1965): «Исчисления секвенций можно понимать как метаисчисления для отношения выводимости в соответствующих системах естественного вывода». [10] И более того: «Доказательство в исчислении секвенций можно рассматривать как инструкцию о том, как построить соответствующую естественную дедукцию». [11] Другими словами, символ утверждения является частью объектного языка для исчисления секвенций, которое является разновидностью метаисчисления, но одновременно обозначает выводимость в базовой системе естественного вывода.
Секвента — это формализованное утверждение доказуемости , которое часто используется при указании исчислений для дедукции . В исчислении секвенты название секвента используется для конструкции, которую можно рассматривать как особый вид суждения , характерный для данной системы дедукции.
Интуитивный смысл секвенции заключается в том, что при предположении Γ заключение Σ доказуемо. Классически формулы слева от турникета можно интерпретировать конъюнктивно, в то время как формулы справа можно рассматривать как дизъюнкцию . Это означает, что когда все формулы в Γ верны, то по крайней мере одна формула в Σ также должна быть истинной. Если сукцедент пуст, это интерпретируется как ложность, т. е. означает, что Γ доказывает ложность и, таким образом, является непоследовательным. С другой стороны, пустой антецедент предполагается истинным, т. е. означает, что Σ следует без каких-либо предположений, т. е. он всегда истинен (как дизъюнкция). Секвенция этой формы, при пустом Γ, известна как логическое утверждение .
Конечно, возможны и другие интуитивные объяснения, которые классически эквивалентны. Например, можно прочитать как утверждение, что не может быть так, что каждая формула в Γ истинна, а каждая формула в Σ ложна (это связано с интерпретациями двойного отрицания классической интуиционистской логики , такими как теорема Гливенко ).
В любом случае, эти интуитивные чтения являются только педагогическими. Поскольку формальные доказательства в теории доказательств являются чисто синтаксическими , значение (вывод) секвенции дается только свойствами исчисления, которое обеспечивает фактические правила вывода .
Исключая любые противоречия в технически точном определении выше, мы можем описать секвенции в их вводной логической форме. представляет собой набор предположений, с которых мы начинаем наш логический процесс, например, «Сократ — человек» и «Все люди смертны». Представляет собой логическое заключение, которое следует из этих предпосылок. Например , «Сократ смертен» следует из разумной формализации вышеуказанных пунктов, и мы могли бы ожидать увидеть его на стороне турникета . В этом смысле означает процесс рассуждения или «thereper» на английском языке.
Общее понятие секвенции, введенное здесь, может быть специализировано различными способами. Секвенция называется интуиционистской секвенцией, если в сукцеденте содержится не более одной формулы (хотя исчисления с несколькими сукцедентами для интуиционистской логики также возможны). Точнее, ограничение общего исчисления секвенций секвенциями с одной формулой-сукцедентом, с теми же правилами вывода, что и для общих секвенций, составляет интуиционистское исчисление секвенций. (Это ограниченное исчисление секвенций обозначается LJ.)
Аналогичным образом можно получить исчисления для дуально-интуиционистской логики (тип паранепротиворечивой логики ), потребовав, чтобы секвенции были сингулярными в антецеденте.
Во многих случаях предполагается, что секвенции состоят из мультимножеств или множеств вместо последовательностей. Таким образом, игнорируется порядок или даже количество вхождений формул. Для классической пропозициональной логики это не создает проблемы, поскольку выводы, которые можно сделать из набора посылок, не зависят от этих данных. Однако в субструктурной логике это может стать весьма важным.
Системы естественного вывода используют условные утверждения с одним следствием, но они, как правило, не используют те же наборы правил вывода, которые Генцен ввел в 1934 году. В частности, табличные системы естественного вывода , которые очень удобны для практического доказательства теорем в исчислении высказываний и исчислении предикатов, применялись Суппесом (1999) и Леммоном (1965) для преподавания вводной логики в учебниках.
Исторически секвенции были введены Герхардом Генценом для того, чтобы определить его знаменитое секвенциальное исчисление . [12] В своей немецкой публикации он использовал слово «Sequenz». Однако в английском языке слово « sequence » уже используется как перевод немецкого «Folge» и довольно часто встречается в математике. Термин «sequent» затем был создан в поисках альтернативного перевода немецкого выражения.
Клини [13] делает следующий комментарий по поводу перевода на английский язык: «Гентцен говорит «Sequenz», что мы переводим как «последовательность», потому что мы уже использовали «последовательность» для любой последовательности объектов, тогда как в немецком языке это «Folge»».
