В математической логике секвенция — это очень общий вид условного утверждения.
Секвенция может иметь любое количество m формул условий A i (называемых « антецедентами ») и любое количество n утвержденных формул B j (называемых «последующими» или « консеквенциями »). Под секвенцией понимается, что если все предшествующие условия верны, то истинна хотя бы одна из последующих формул. Этот стиль условного утверждения почти всегда связан с концептуальной структурой секвенциального исчисления .
Секвенции лучше всего понимать в контексте следующих трех видов логических суждений :
Таким образом, секвенции являются обобщением простых условных утверждений, которые являются обобщением безусловных утверждений.
Слово «ИЛИ» здесь является включающим ИЛИ . [1] Мотивация использования дизъюнктивной семантики в правой части секвенции обусловлена тремя основными преимуществами.
Все три преимущества были определены в основополагающем документе Генцена (1934, стр. 194).
Не все авторы придерживались первоначального значения слова «последовательный», данного Генценом. Например, Леммон (1965) использовал слово «секвенциальный» строго для простых условных утверждений с одной и только одной последовательной формулой. [2] Такое же однозначное определение секвенции дано Huth & Ryan 2004, p. 5.
В общей секвенции вида
и Γ, и Σ являются последовательностями логических формул, а не множествами . Поэтому существенное значение имеют как количество, так и порядок появления формул. В частности, одна и та же формула может встречаться дважды в одной и той же последовательности. Полный набор правил вывода секвенционного исчисления содержит правила замены соседних формул слева и справа от символа утверждения (и тем самым произвольно переставлять местами левую и правую последовательности), а также вставки произвольных формул и удаления повторяющихся копий внутри левой части. и правильная последовательность. (Однако Смаллиан (1995, стр. 107–108) использует наборы формул в секвенциях вместо последовательностей формул. Следовательно, три пары структурных правил , называемых «утончение», «сокращение» и «обмен», не требуются.)
Символ ' ' часто называют « турникетом », «правым поворотом», «тройником», «знаком утверждения» или «символом утверждения». Его часто читают, что наводит на размышления, как «дает», «доказывает» или «влечет за собой».
Поскольку каждая формула в антецеденте (левая часть) должна быть истинной, чтобы сделать вывод об истинности хотя бы одной формулы в последующем (правая часть), добавление формул в любую сторону приводит к более слабой секвенции, а удаление их из любой стороны дает более сильный. Это одно из преимуществ симметрии, которое следует из использования дизъюнктивной семантики в правой части символа утверждения, тогда как конъюнктивная семантика сохраняется в левой части.
В крайнем случае, когда список предшествующих формул секвенции пуст, консеквент безусловен. Это отличается от простого безусловного утверждения, поскольку количество консеквентов произвольно и не обязательно является одним консеквентом. Так , например, '⊢ B1 , B2 ' означает, что либо B1 , либо B2 , либо оба должны быть истинными. Пустой список антецедентных формул эквивалентен утверждению «всегда истинно», называемому « verum », обозначаемому «⊤». (См. Тройник (символ) .)
В крайнем случае, когда список последовательных формул секвенции пуст, правило по-прежнему состоит в том, что хотя бы один член справа должен быть истинным, что явно невозможно . На это указывает «всегда ложное» суждение, называемое « ложным », обозначаемое «⊥». Поскольку следствие ложно, по крайней мере один из антецедентов должен быть ложным. Так, например, ' 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] Другими словами, символ утверждения является частью объектного языка секвенциального исчисления, которое является разновидностью метаисчисления, но одновременно означает выводимость в лежащей в его основе естественной системе вывода.
Секвенция — это формализованное утверждение доказуемости , которое часто используется при определении исчислений для вывода . В секвенциальном исчислении название секвенция используется для конструкции, которую можно рассматривать как особый вид суждения , характерный для этой системы дедукции.
Интуитивный смысл секвенции состоит в том, что в предположении Γ заключение Σ доказуемо. Классически формулы слева от турникета можно интерпретировать конъюнктивно , а формулы справа можно рассматривать как дизъюнкцию . Это означает, что если все формулы из Γ выполняются, то хотя бы одна формула из Σ также должна быть истинной. Если сукцедент пуст, это интерпретируется как ложность, т. е. означает, что Γ доказывает ложность и, следовательно, является противоречивым. С другой стороны, пустой антецедент считается истинным, т. е. означает, что Σ следует без каких-либо предположений, т. е. он всегда истинен (как дизъюнкция). Секвенция такого вида с пустым Γ известна как логическое утверждение .
Конечно, возможны и другие интуитивные объяснения, классически эквивалентные. Например, это можно прочитать как утверждение, что не может быть так, чтобы каждая формула в Γ была истинной, а каждая формула в Σ была ложной (это связано с интерпретациями двойного отрицания классической интуиционистской логики , такими как теорема Гливенко ).
В любом случае, эти интуитивные прочтения имеют лишь педагогический характер. Поскольку формальные доказательства в теории доказательств являются чисто синтаксическими , смысл (вывод) секвенции задается только свойствами исчисления, которое обеспечивает действительные правила вывода .
Исключив какие-либо противоречия в приведенном выше технически точном определении, мы можем описать секвенции в их вводной логической форме. представляет собой набор предположений, с которых мы начинаем наш логический процесс, например «Сократ — человек» и «Все люди смертны». Это представляет собой логический вывод, который следует из этих предпосылок. Например, «Сократ смертен» следует из разумной формализации приведенных выше положений, и мы могли ожидать увидеть его на боковой стороне турникета . В этом смысле означает процесс рассуждения, или «следовательно» по-английски.
Введенное здесь общее понятие секвенции можно специализировать по-разному. Секвенция называется интуиционистской секвенцией , если в ней содержится не более одной формулы (хотя для интуиционистской логики также возможны многопоследовательные исчисления). Точнее, ограничение общего секвенциального исчисления секвенциями с одной последовательной формулой с теми же правилами вывода , что и для общих секвенций, представляет собой интуиционистское секвенциальное исчисление. (Это ограниченное секвенциальное исчисление обозначается LJ.)
Точно так же можно получить исчисления для дуальной интуиционистской логики (разновидность паранепротиворечивой логики ), потребовав, чтобы секвенции были сингулярны в антецеденте.
Во многих случаях предполагается, что секвенции состоят из мультимножеств или наборов , а не последовательностей. При этом игнорируется порядок или даже количество вхождений формул. Для классической логики высказываний это не представляет проблемы, поскольку выводы, которые можно сделать из совокупности посылок, не зависят от этих данных. Однако в субструктурной логике это может стать весьма важным.
Системы естественной дедукции используют условные утверждения с одним следствием, но они обычно не используют те же наборы правил вывода, которые Генцен представил в 1934 году. В частности, табличные системы естественной дедукции , которые очень удобны для практического доказательства теорем в исчислении высказываний и исчислении предикатов. исчисления, применялись Суппесом (1999) и Леммоном (1965) для преподавания вводной логики в учебниках.
Исторически секвенции были введены Герхардом Генценом для уточнения его знаменитого исчисления секвенций . [12] В своей немецкой публикации он использовал слово «Sequenz». Однако в английском языке слово « последовательность » уже используется как перевод на немецкий «Folge» и довольно часто встречается в математике. Термин «последовательность» был создан в поисках альтернативного перевода немецкого выражения.
Клини [13] делает следующий комментарий по поводу перевода на английский язык: «Гентцен говорит «Sequenz», что мы переводим как «последовательность», потому что мы уже использовали слово «последовательность» для любой последовательности объектов, тогда как по-немецки это «Folge». ."
