Последовательность - Sequent

В математической логике , секвенции очень общий вид условного утверждения.

${\ displaystyle A_ {1}, \, \ dots, A_ {m} \, \ vdash \, B_ {1}, \, \ dots, B_ {n}.}$

Последовательность может иметь любое количество m формул условий A _i (называемых « антецедентами ») и любое количество n утвержденных формул B _j (называемых «последователями» или « консеквентами »). Под секвенцией понимается то, что если все предшествующие условия верны, то по крайней мере одна из последующих формул верна. Этот стиль условного утверждения почти всегда связан с концептуальной структурой секвенциального исчисления .

Вступление

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

Секвенты лучше всего понимать в контексте следующих трех видов логических суждений :

1. Безусловное утверждение . Никаких предшествующих формул.
   • Пример: ⊢ B
   • Значение: B верно.
2. Условное утверждение . Любое количество предшествующих формул.
   1. Простое условное утверждение . Единая консеквентная формула.
      • Пример: A ₁ , A ₂ , A ₃ ⊢ B
      • Значение: ЕСЛИ ₁ И ₂ И ₃ верны, то В истинно.
   2. Sequent . Любое количество последовательных формул.
      • Пример: A ₁ , A ₂ , A ₃ ⊢ B ₁ , B ₂ , B ₃ , B _4.
      • Значение: ЕСЛИ ₁ И ₂ И ₃ верны, то B ₁ ИЛИ В ₂ ИЛИ В ₃ ИЛИ В ₄ верно.

Таким образом, секвенции являются обобщением простых условных утверждений, которые являются обобщением безусловных утверждений.

Слово «ИЛИ» здесь является включающим ИЛИ . Мотивация дизъюнктивной семантики в правой части секвенции проистекает из трех основных преимуществ.

1. Симметрия классических правил вывода для секвенций с такой семантикой.
2. Легкость и простота преобразования таких классических правил в интуиционистские.
3. Способность доказать полноту исчисления предикатов, когда оно выражается таким образом.

Все три преимущества были определены в основополагающей статье Гентцена (1934 , стр. 194).

Не все авторы придерживаются первоначального значения слова «секвенция», которое использовал Генцен. Например, Леммон (1965) использовал слово «секвенция» строго для простых условных утверждений с одной и только одной последовательной формулой. Такое же определение секвенции с единственной консеквенцией дано Huth & Ryan 2004 , p. 5.

Детали синтаксиса

В общем виде

${\ Displaystyle \ Gamma \ vdash \ Sigma}$

и Γ, и Σ представляют собой последовательности логических формул, а не множества . Таким образом, значение имеют как количество, так и порядок появления формул. В частности, одна и та же формула может встречаться дважды в одной и той же последовательности. Полный набор правил вывода последовательного исчисления содержит правила для замены соседних формул слева и справа от символа утверждения (и, таким образом, произвольного перестановки левой и правой последовательностей), а также для вставки произвольных формул и удаления повторяющихся копий в левой части. и правильные последовательности. (Однако Smullyan (1995 , стр. 107–108) использует наборы формул в секвенциях вместо последовательностей формул. Следовательно, три пары структурных правил, называемые «прореживание», «сжатие» и «взаимозаменяемость», не требуются.)

Символ ' ' часто называют " турникет ", "правая галс", "тройник", "знак утверждения" или "символ утверждения". Его часто читают как «дает», «доказывает» или «влечет за собой». ${\ displaystyle \ vdash}$

Характеристики

Эффекты вставки и удаления предложений

Поскольку каждая формула в антецеденте (левая сторона) должна быть истинной, чтобы сделать вывод об истинности хотя бы одной формулы в последующем (правая сторона), добавление формул к любой из сторон приводит к более слабой секвенции, а удаление их с любой стороны дает более сильный. Это одно из преимуществ симметрии, которое следует из использования дизъюнктивной семантики в правой части символа утверждения, в то время как конъюнктивная семантика соблюдается в левой части.

Последствия пустых списков формул

В крайнем случае, когда список предшествующих формул секвенции пуст, консеквент является безусловным. Это отличается от простого безусловного утверждения, потому что количество консеквентов произвольно, не обязательно один консеквент. Так, например, «⊢ B ₁ , B ₂ » означает, что либо B ₁ , либо B ₂ , либо оба должны быть истинными. Пустой список предшествующих формул эквивалентен утверждению «всегда истинное», называемому « verum » и обозначается «⊤». (См. Тройник (символ) .)

В крайнем случае, когда список последовательных формул секвенции пуст, по-прежнему действует правило, согласно которому хотя бы один член справа должен быть истинным, что явно невозможно . Это обозначено предложением «всегда ложно», называемым « ложью », обозначенным «⊥». Поскольку следствие ложно, по крайней мере, одно из предшествующих должно быть ложным. Так, например, « A ₁ , A ₂ ⊢» означает, что по крайней мере один из антецедентов A ₁ и A ₂ должен быть ложным.

Здесь снова наблюдается симметрия из-за дизъюнктивной семантики с правой стороны. Если левая часть пуста, то одно или несколько утверждений правой части должны быть истинными. Если правая часть пуста, то одно или несколько левых предложений должны быть ложными.

Двойной крайний случай «», когда и антецедентный, и последовательный списки формул пусты, « невыполнимы ». В этом случае секвенция имеет смысл «⊤ ⊢ ⊥». Это эквивалентно секвенции «⊢ ⊥», которая явно не может быть верной.

Примеры

Секвенция вида «⊢ α, β» для логических формул α и β означает, что либо α истинно, либо β истинно (или и то, и другое). Но это не означает, что либо α - тавтология, либо β - тавтология. Чтобы прояснить это, рассмотрим пример «⊢ B ∨ A, C ∨ ¬A». Это правильная секвенция, потому что либо B ∨ A истинно, либо C ∨ ¬A истинно. Но ни одно из этих выражений не является изолированной тавтологией. Это разъединение этих двух выражений, является тавтологией.

Точно так же секвенция вида «α, β ⊢» для логических формул α и β означает, что либо α ложно, либо β ложно. Но это не означает, что либо α - противоречие, либо β - противоречие. Чтобы прояснить это, рассмотрим пример «B ∧ A, C ∧ ¬A ⊢». Это правильная секвенция, потому что либо B ∧ A ложно, либо C ∧ ¬A ложно. Но ни одно из этих выражений не является изолированным противоречием. Это сочетание этих двух выражений, противоречие.

Правила

Большинство систем доказательства предоставляют способы вывести одну последовательность из другой. Эти правила вывода записываются со списком секвенций над и под строкой . Это правило указывает, что если все, что находится над линией, верно, то все, что находится под линией, верно.

Типичное правило:

${\ displaystyle {\ frac {\ Gamma, \ alpha \ vdash \ Sigma \ qquad \ Gamma \ vdash \ alpha} {\ Gamma \ vdash \ Sigma}}}$

Это указывает на то, что если мы можем вывести, что дает , и что дает , то мы также можем вывести, что дает . (См. Также полный набор правил вывода последовательного исчисления .) ${\ displaystyle \ Gamma, \ alpha}$${\ displaystyle \ Sigma}$${\ displaystyle \ Gamma}$${\ displaystyle \ alpha}$${\ displaystyle \ Gamma}$${\ displaystyle \ Sigma}$

Интерпретация

История значения последовательных утверждений

Символ утверждения в секвентах изначально означал то же самое, что и оператор импликации. Но со временем его значение изменилось, чтобы обозначать доказуемость в рамках теории, а не семантическую истину во всех моделях.

В 1934 году Генцен не определял символ утверждения «⊢» в секвенции для обозначения доказуемости. Он определил это как то же самое, что и оператор импликации «⇒». Используя «→» вместо «⊢» и «⊃» вместо «⇒», он писал: «Секвенция A ₁ , ..., A _μ → B ₁ , ..., B _ν означает, что касается содержания, точно так же, как формула (A ₁ & ... & A _μ ) ⊃ (B ₁ ∨ ... ∨ B _ν ) ". (Генцен использовал символ стрелки вправо между антецедентами и консеквентами секвенций. Он использовал символ «⊃» для оператора логической импликации.)

В 1939 году Гильберт и Бернейс также заявили, что секвенция имеет то же значение, что и соответствующая формула импликации.

В 1944 году Алонзо Черч подчеркнул, что последующие утверждения Гентцена не означают доказуемости.

«Использование теоремы дедукции в качестве примитивного или производного правила, однако, не следует путать с использованием Sequenzen Гентценом. Для стрелки Гентцена, → не сопоставимо с нашей синтаксической нотацией,, но принадлежит его объектному языку (как ясно из того факта, что содержащие его выражения выступают в качестве посылок и выводов в применении его правил вывода) ".

В многочисленных публикациях после этого времени утверждалось, что символ утверждения в секвенциях действительно означает доказуемость в рамках теории, в которой сформулированы секвенции. Карри в 1963 году, Леммон в 1965 году и Хут и Райан в 2004 году - все заявляют, что последовательный символ утверждения означает доказуемость. Однако Бен-Ари (2012 , стр. 69) утверждает, что символ утверждения в секвентах системы Генцен, который он обозначает как «⇒», является частью объектного языка, а не метаязыка.

Согласно Правитцу (1965): «Исчисления секвенций можно понимать как метаисчисления для отношения выводимости в соответствующих системах естественного вывода». И более того: «Доказательство в исчислении секвенций можно рассматривать как инструкцию о том, как построить соответствующий естественный вывод». Другими словами, символ утверждения является частью объектного языка для исчисления секвенций, которое является своего рода метаисчислением, но одновременно означает выводимость в лежащей в основе естественной системе вывода.

Интуитивное значение

Секвенция - это формализованное заявление о доказуемости , которое часто используется при указании исчислений для дедукции . В исчислении секвенций для построения конструкции используется название секвенция , которую можно рассматривать как особый вид суждения , характерный для этой системы дедукции.

Интуитивный смысл секвенции состоит в том, что в предположении Γ заключение Σ доказуемо. Классически формулы слева от турникета можно интерпретировать совместно, а формулы справа можно рассматривать как дизъюнкцию . Это означает, что если все формулы в Γ верны, то хотя бы одна формула из Σ также должна быть истинной. Если преемник пуст, это интерпретируется как ложность, т. Е. Означает, что Γ доказывает ложность и, таким образом, несовместима. С другой стороны, пустой антецедент считается истинным, т. Е. Означает, что Σ следует без каких-либо предположений, т. Е. Всегда верно (как дизъюнкция). Секвенция такой формы с пустым Γ называется логическим утверждением . ${\ Displaystyle \ Gamma \ vdash \ Sigma}$${\ displaystyle \ Gamma \ vdash}$${\ Displaystyle \ vdash \ Sigma}$

Конечно, возможны и другие интуитивные объяснения, которые классически эквивалентны. Например, его можно рассматривать как утверждение, что не может быть случая, чтобы каждая формула в Γ была истинной, а каждая формула в Σ ложна (это связано с интерпретациями двойного отрицания классической интуиционистской логики , такими как теорема Гливенко ). ${\ Displaystyle \ Gamma \ vdash \ Sigma}$

В любом случае эти интуитивные прочтения носят исключительно педагогический характер. Поскольку формальные доказательства в теории доказательств являются чисто синтаксическими , значение (вывода) секвенции определяется только свойствами исчисления, которое обеспечивает действительные правила вывода .

Не допуская каких-либо противоречий в технически точном определении выше, мы можем описывать секвенции в их вводной логической форме. представляет собой набор предположений, с которых мы начинаем наш логический процесс, например «Сократ - человек» и «Все люди смертны». Символ представляет собой логический вывод, который следует из этих посылок. Например, «Сократ смертен» следует из разумной формализации вышеупомянутых пунктов, и мы могли бы ожидать увидеть это сбоку турникета . В этом смысле означает процесс рассуждения или «следовательно» по-английски. ${\ displaystyle \ Gamma}$${\ displaystyle \ Sigma}$${\ displaystyle \ Sigma}$${\ displaystyle \ vdash}$

Вариации

Введенное здесь общее понятие секвенции может быть различным образом специализировано. Секвенция называется интуиционистской секвенцией, если в последующем есть не более одной формулы (хотя также возможны множественные исчисления для интуиционистской логики). Точнее, ограничение общего исчисления секвенций последовательностями с единственными последовательностями формул с теми же правилами вывода, что и для общих секвенций, составляет интуиционистское исчисление секвенций. (Это ограниченное исчисление секвенций обозначается LJ.)

Точно так же можно получить исчисления для дуальной интуиционистской логики (типа паранепротиворечивой логики ), требуя, чтобы секвенции были единичными в антецеденте.

Во многих случаях предполагается, что последовательности состоят из мультимножеств или наборов вместо последовательностей. Таким образом, игнорируется порядок или даже количество вхождений формул. Для классической логики высказываний это не представляет проблемы, поскольку выводы, которые можно сделать из совокупности предпосылок, не зависят от этих данных. Однако в субструктурной логике это может стать весьма важным.

Системы естественного вывода используют условные утверждения с одним следствием, но они обычно не используют те же наборы правил вывода, которые Гентцен ввел в 1934 году. В частности, табличные системы естественного вывода , которые очень удобны для практического доказательства теорем в исчислении высказываний и предикатах. исчисление, применялись Суппесом (1957) и Леммоном (1965) для обучения вводной логике в учебниках. Ошибка harvtxt: цель отсутствует: CITEREFSuppes1957 ( справка )

Этимология

Исторически секвенции были введены Герхардом Гентценом для уточнения его знаменитого исчисления секвенций . В своей немецкой публикации он использовал слово «Sequenz». Однако в английском языке слово « последовательность » уже используется как перевод на немецкий «Folge» и довольно часто встречается в математике. Термин «секвенция» был создан в поисках альтернативного перевода немецкого выражения.

Клини делает следующий комментарий к переводу на английский язык: «Гентцен говорит« Sequenz », что мы переводим как« последовательность », потому что мы уже использовали« последовательность »для любой последовательности объектов, где по-немецки« Folge »».

Смотрите также

• Герхард Гентцен
• Интуиционистская логика
• Естественный вычет
• Последовательное исчисление

Заметки

Рекомендации

• Бен-Ари, Мордехай (2012) [1993]. Математическая логика для информатики . Лондон: Спрингер. ISBN   978-1-4471-4128-0 .
• Чёрч, Алонзо (1996) [1944]. Введение в математическую логику . Принстон, Нью-Джерси: Издательство Принстонского университета. ISBN   978-0-691-02906-1 .
• Карри, Хаскелл Брукс (1977) [1963]. Основы математической логики . Нью-Йорк: ISBN Dover Publications Inc.   978-0-486-63462-3 .
• Генцен, Герхард (1934). "Untersuchungen über das logische Schließen. I" . Mathematische Zeitschrift . 39 (2): 176–210. DOI : 10.1007 / bf01201353 .
• Генцен, Герхард (1935). "Untersuchungen über das logische Schließen. II" . Mathematische Zeitschrift . 39 (3): 405–431. DOI : 10.1007 / bf01201363 .
• Гильберт, Дэвид ; Бернейс, Пол (1970) [1939]. Grundlagen der Mathematik II (Второе изд.). Берлин, Нью-Йорк: Springer-Verlag. ISBN   978-3-642-86897-9 .
• Хут, Майкл; Райан, Марк (2004). Логика в информатике (второе изд.). Кембридж, Соединенное Королевство: Издательство Кембриджского университета. ISBN   978-0-521-54310-1 .
• Клини, Стивен Коул (2009) [1952]. Введение в метаматематику . Ishi Press International. ISBN   978-0-923891-57-2 .
• Клини, Стивен Коул (2002) [1967]. Математическая логика . Минеола, Нью-Йорк: Dover Publications. ISBN   978-0-486-42533-7 .
• Леммон, Эдвард Джон (1965). Начало логики . Томас Нельсон. ISBN   0-17-712040-1 .
• Prawitz, Dag (2006) [1965]. Естественная дедукция: теоретико-доказательное исследование . Минеола, Нью-Йорк: Dover Publications. ISBN   978-0-486-44655-4 .
• Смуллян, Раймонд Меррилл (1995) [1968]. Логика первого порядка . Нью-Йорк: Dover Publications. ISBN   978-0-486-68370-6 .
• Суппес, Патрик Полковник (1999) [1957]. Введение в логику . Минеола, Нью-Йорк: Dover Publications. ISBN   978-0-486-40687-9 .
• Такеути, Гайси (2013) [1975]. Теория доказательств (Второе изд.). Минеола, Нью-Йорк: Dover Publications. ISBN   978-0-486-49073-1 .

Внешние ссылки

• «Последовательность (в логике)» , Энциклопедия математики , EMS Press , 2001 [1994]