В математической логике , секвенции очень общий вид условного утверждения.
Последовательность может иметь любое количество m формул условий A i (называемых « антецедентами ») и любое количество n утвержденных формул B j (называемых «последователями» или « консеквентами »). Под секвенцией понимается то, что если все предшествующие условия верны, то по крайней мере одна из последующих формул верна. Этот стиль условного утверждения почти всегда связан с концептуальной структурой секвенциального исчисления .
Вступление
Форма и семантика секвенций
Секвенты лучше всего понимать в контексте следующих трех видов логических суждений :
- Безусловное утверждение . Никаких предшествующих формул.
- Пример: ⊢ B
- Значение: B верно.
- Условное утверждение . Любое количество предшествующих формул.
- Простое условное утверждение . Единая консеквентная формула.
- Пример: A 1 , A 2 , A 3 ⊢ B
- Значение: ЕСЛИ 1 И 2 И 3 верны, то В истинно.
- Секвент . Любое количество последовательных формул.
- Пример: A 1 , A 2 , A 3 ⊢ B 1 , B 2 , B 3 , B 4.
- Значение: ЕСЛИ 1 И 2 И 3 верны, то B 1 ИЛИ В 2 ИЛИ В 3 ИЛИ В 4 верно.
- Простое условное утверждение . Единая консеквентная формула.
Таким образом, секвенции являются обобщением простых условных утверждений, которые являются обобщением безусловных утверждений.
Слово «ИЛИ» здесь является включающим ИЛИ . [1] Мотивация дизъюнктивной семантики в правой части секвенции проистекает из трех основных преимуществ.
- Симметрия классических правил вывода для секвенций с такой семантикой.
- Легкость и простота преобразования таких классических правил в интуиционистские.
- Способность доказать полноту исчисления предикатов, когда оно выражается таким образом.
Все три преимущества были определены в основополагающем документе Генцен (1934 , стр. 194).
Не все авторы придерживаются первоначального значения слова «секвенция», которое использовал Генцен. Например, Леммон (1965) использовал слово «секвенция» строго для простых условных утверждений с одной и только одной последовательной формулой. [2] Такое же определение секвенции с единственной консеквенцией дано Huth & Ryan 2004 , p. 5.
Детали синтаксиса
В общем виде
и Γ, и Σ представляют собой последовательности логических формул, а не множества . Таким образом, значение имеют как количество, так и порядок появления формул. В частности, одна и та же формула может встречаться дважды в одной и той же последовательности. Полный набор правил вывода последовательного исчисления содержит правила для замены соседних формул слева и справа от символа утверждения (и, таким образом, произвольного перестановки левой и правой последовательностей), а также для вставки произвольных формул и удаления повторяющихся копий в левой части. и правильные последовательности. (Однако Smullyan (1995 , стр. 107–108) использует наборы формул в секвенциях вместо последовательностей формул. Следовательно, три пары структурных правил, называемые «прореживание», «сжатие» и «взаимозаменяемость», не требуются.)
Символ ' 'часто называют « турникет », «правая галс», «тройник», «знак утверждения» или «символ утверждения». Его часто читают как «дает», «доказывает» или «влечет за собой».
Характеристики
Эффекты вставки и удаления предложений
Поскольку каждая формула в антецеденте (левая сторона) должна быть истинной, чтобы сделать вывод об истинности хотя бы одной формулы в последующем (правая сторона), добавление формул к любой из сторон приводит к более слабой секвенции, а удаление их с любой стороны дает более сильный. Это одно из преимуществ симметрии, которое следует из использования дизъюнктивной семантики в правой части символа утверждения, в то время как конъюнктивная семантика соблюдается в левой части.
Последствия пустых списков формул
В крайнем случае, когда список предшествующих формул секвенции пуст, консеквент является безусловным. Это отличается от простого безусловного утверждения, потому что количество консеквентов произвольно, не обязательно один консеквент. Так, например, «⊢ B 1 , B 2 » означает, что либо B 1 , либо B 2 , либо оба должны быть истинными. Пустой список предшествующих формул эквивалентен предложению «всегда истинное», называемому « 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 году Алонсо Черч подчеркнул, что последующие утверждения Гентцена не означают доказуемости.
- «Использование теоремы дедукции в качестве примитивного или производного правила, однако, не следует путать с использованием Гентцена Sequenzen. Для стрелки Гентцена, → не сопоставимо с нашей синтаксической нотацией, но принадлежит его объектному языку (как ясно из того факта, что содержащие его выражения выступают в качестве посылок и выводов в применении его правил вывода) ". [6]
В многочисленных публикациях после этого времени утверждалось, что символ утверждения в секвенциях действительно означает доказуемость в рамках теории, в которой сформулированы секвенции. Карри в 1963 г. [7] Леммон в 1965 г. [2] и Хут и Райан в 2004 г. [8] утверждают, что символ последовательного утверждения означает доказуемость. Однако Бен-Ари (2012 , стр. 69) утверждает, что символ утверждения в секвентах системы Генцен, который он обозначает как «⇒», является частью объектного языка, а не метаязыка. [9]
Согласно Правитцу (1965): «Исчисления секвенций можно понимать как метаисчисления для отношения выводимости в соответствующих системах естественного вывода». [10] И более того: «Доказательство в исчислении секвенций можно рассматривать как инструкцию о том, как построить соответствующий естественный вывод». [11] Другими словами, символ утверждения является частью объектного языка для секвенциального исчисления, которое является своего рода метаисчислением, но одновременно означает выводимость в лежащей в основе естественной системе вывода.
Интуитивное значение
Секвенция - это формализованное заявление о доказуемости , которое часто используется при указании исчислений для дедукции . В исчислении секвенций для построения конструкции используется название секвенция , которую можно рассматривать как особый вид суждения , характерный для этой системы дедукции.
Интуитивное значение секвенции состоит в том, что в предположении Γ заключение Σ доказуемо. Классически формулы слева от турникета можно интерпретировать совместно, а формулы справа можно рассматривать как дизъюнкцию . Это означает, что если все формулы в Γ верны, то хотя бы одна формула из Σ также должна быть истинной. Если преемник пуст, это интерпретируется как ложь, т. Е.означает, что Γ доказывает ложность и, таким образом, несовместима. С другой стороны, пустой антецедент считается истинным, т. Е.означает, что Σ следует без каких-либо предположений, т. е. всегда верно (как дизъюнкция). Секвенция такой формы с пустым Γ называется логическим утверждением .
Конечно, возможны и другие интуитивные объяснения, которые классически эквивалентны. Например,можно прочитать как утверждение, что не может быть случая, чтобы каждая формула в Γ была истинной, а каждая формула в Σ ложна (это связано с интерпретациями двойного отрицания классической интуиционистской логики , такими как теорема Гливенко ).
В любом случае эти интуитивные прочтения носят исключительно педагогический характер. Поскольку формальные доказательства в теории доказательств являются чисто синтаксическими , значение (вывода) секвенции определяется только свойствами исчисления, которое обеспечивает действительные правила вывода .
Не допуская противоречий в технически точном определении выше, мы можем описывать секвенции в их вводной логической форме. представляет собой набор предположений, с которых мы начинаем наш логический процесс, например «Сократ - человек» и «Все люди смертны». Впредставляет собой логический вывод, который следует из этих посылок. Например, «Сократ смертен» следует из разумной формализации вышеупомянутых пунктов, и мы могли бы ожидать увидеть это насторона турникета . В этом смысле, означает процесс рассуждения или «поэтому» на английском языке.
Вариации
Введенное здесь общее понятие секвенции может быть различным образом специализировано. Секвенция называется интуиционистской секвенцией, если в последующем есть не более одной формулы (хотя также возможны множественные исчисления для интуиционистской логики). Точнее, ограничение общего исчисления секвенций последовательностями с единственными последовательностями формул с теми же правилами вывода, что и для общих секвенций, составляет интуиционистское исчисление секвенций. (Это ограниченное исчисление секвенций обозначается LJ.)
Точно так же можно получить исчисления для дуальной интуиционистской логики (типа паранепротиворечивой логики ), требуя, чтобы секвенции были единичными в антецеденте.
Во многих случаях предполагается, что последовательности состоят из мультимножеств или наборов вместо последовательностей. Таким образом, игнорируется порядок или даже количество вхождений формул. Для классической логики высказываний это не представляет проблемы, поскольку выводы, которые можно сделать из совокупности предпосылок, не зависят от этих данных. Однако в субструктурной логике это может стать весьма важным.
Системы естественного вывода используют условные утверждения с одним следствием, но они обычно не используют те же наборы правил вывода, которые Гентцен ввел в 1934 году. В частности, табличные системы естественного вывода , которые очень удобны для практического доказательства теорем в исчислении высказываний и предикатах. исчисление, были применены Suppes (1957)
и Lemmon (1965) за преподавание вводной логики в учебниках.Этимология
Исторически секвенции были введены Герхардом Гентценом для уточнения его знаменитого исчисления секвенций . [12] В своей немецкой публикации он использовал слово «Sequenz». Однако в английском языке слово « последовательность » уже используется как перевод на немецкий «Folge» и довольно часто встречается в математике. Термин «секвенция» был создан в поисках альтернативного перевода немецкого выражения.
Клини [13] делает следующий комментарий к переводу на английский язык: «Гентцен говорит« Sequenz », что мы переводим как« последовательность », потому что мы уже использовали« последовательность »для любой последовательности объектов, где по-немецки« Folge ». . "
Смотрите также
- Герхард Гентцен
- Интуиционистская логика
- Естественный вычет
- Последовательное исчисление
Заметки
- ^ Дизъюнктивная семантика для правой части секвенции сформулирована и объяснена в Curry 1977 , pp. 189–190, Kleene 2002 , pp. 290, 297, Kleene 2009 , p. 441, Hilbert & Bernays 1970 , стр. 385, Смуллян, 1995 , с. 104–105, Такеути, 2013 , с. 9, и Gentzen 1934 , стр. 180.
- ^ а б Леммон 1965 , стр. 12, писал: «Таким образом, секвенция - это рамка аргумента, содержащая набор предположений и вывод, который, как утверждается, следует из них. [...] Предложения слева от '' становятся предположениями аргумента, и предложение справа становится выводом, обоснованно сделанным из этих предположений ".
- ^ Smullyan 1995 , стр. 105.
- ^ Генценовского 1934 , стр. 180.
- 2.4. Die Sequenz A 1 , ..., A μ → B 1 , ..., B ν bedeutet inhaltlich genau dasselbe wie die Formel
- (A 1 & ... & A μ ) ⊃ (B 1 ∨ ... ∨ B ν ).
- 2.4. Die Sequenz A 1 , ..., A μ → B 1 , ..., B ν bedeutet inhaltlich genau dasselbe wie die Formel
- Перейти ↑ Hilbert & Bernays 1970 , p. 385.
- Für die inhaltliche Deutung ist eine Sequenz
- A 1 , ..., A r → B 1 , ..., B s ,
- worin die Anzahlen r und s von 0 verschieden sind, gleichbedeutend mit der Implikation
- (A 1 & ... & A r ) → (B 1 ∨ ... ∨ B s )
- Für die inhaltliche Deutung ist eine Sequenz
- ^ Церковь 1996 , стр. 165.
- Перейти ↑ Curry 1977 , p. 184
- ^ Хут & Ryan (2004 , стр. 5)
- Перейти ↑ Ben-Ari 2012 , p. 69, определяет секвенциичтобы иметь форму U ⇒ V для (возможно непустых) множеств формул U и V . Затем он пишет:
- «Интуитивно секвенция представляет« доказуемую из »в том смысле, что формулы в U являются предположениями для множества формул V , которые должны быть доказаны. Символ ⇒ аналогичен символу ⊢ в гильбертовых системах, за исключением того, что ⇒ является частью объектного языка формализуемой дедуктивной системы, а ⊢ - обозначение метаязыка, используемое для рассуждений о дедуктивных системах ».
- ^ Prawitz 2006 , стр. 90.
- ^ См. Prawitz 2006 , стр. 91, для этого и других деталей интерпретации.
- ^ Генценовский 1934 , генценовский 1935 .
- Перейти ↑ Kleene 2002 , p. 441
Рекомендации
- Бен-Ари, Мордехай (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.
- Правиц, Даг (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]