секвентальный

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

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

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

Введение [ править ]

Форма и семантика секвенций [ править ]

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

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

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

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

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

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

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

Подробности синтаксиса [ править ]

В общей секвенции вида

\Gamma \vdash \Sigma

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

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

Свойства [ править ]

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

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

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

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

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

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

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

Примеры [ править ]

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

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

Правила [ править ]

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

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

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

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

Интерпретация [ править ]

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

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

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

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

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

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

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

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

Интуитивное значение [ править ]

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

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

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

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

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

Вариации [ править ]

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

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

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

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

Этимология [ править ]

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

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

См. также [ править ]

Примечания [ править ]

^ Дизъюнктивная семантика правой части секвенции сформулирована и объяснена Карри 1977 , стр. 189–190, Клини 2002 , стр. 290, 297, Клини 2009 , стр. 441, Гильберт и Бернейс 1970 , с. 385, Смуллян 1995 , стр. 104–105, Такеути 2013 , стр. 9, и Генцен 1934 , с. 180.
^ Перейти обратно: ^а ^б Леммон 1965 , с. 12 писал: «Таким образом, секвенция — это фрейм аргумента, содержащий набор предположений и вывод, который, как утверждается, следует из них. [...] Предложения слева от «⊢» становятся предположениями аргумента, и предложение справа становится выводом, обоснованно сделанным из этих предположений».
^ Смуллян 1995 , с. 105.
^ Генцен 1934 , с. 180.
2.4. Последовательность A ₁ , ..., A _µ → B ₁ , ..., B _ν означает точно то же, что и формула
(А ₁ & ... & А _µ ) ⊃ (B ₁ ∨ ... ∨ B _ν ).
^ Гильберт и Бернейс 1970 , с. 385.
Последовательность используется для интерпретации содержания.
А ₁ , ..., А _р → В ₁ , ..., Б _s ,

где числа r и s отличны от 0, что эквивалентно импликации
(А ₁ & ... & А _р ) → (B ₁ ∨ ... ∨ B _s )
^ Церковь 1996 , с. 165.
^ Карри 1977 , с. 184
^ Хут и Райан (2004 , стр. 5)
^ Бен-Ари 2012 , с. 69 определяет секвенции в виде U ⇒ V для (возможно, непустых) множеств формул U и V . Затем он пишет:
«Интуитивно, секвенция представляет собой «доказуемую из» в том смысле, что формулы в U являются предположениями для множества формул V , которые должны быть доказаны. Символ ⇒ подобен символу ⊢ в гильбертовых системах, за исключением того, что ⇒ является частью объектного языка формализуемой дедуктивной системы, а ⊢ — это метаязыковая нотация, используемая для рассуждений о дедуктивных системах».
^ Правиц 2006 , с. 90.
^ См. Prawitz 2006 , с. 91, где описаны эти и другие подробности интерпретации.
^ Генцен 1934 , Генцен 1935 .
^ Клини 2002 , с. 441

Ссылки [ править ]

Бен-Ари, Мордехай (2012) [1993]. Математическая логика для информатики . Лондон: Спрингер. ISBN 978-1-4471-4128-0 .
Черч, Алонзо (1996) [1944]. Введение в математическую логику . Принстон, Нью-Джерси: Издательство Принстонского университета. ISBN 978-0-691-02906-1 .
Карри, Хаскелл Брукс (1977) [1963]. Основы математической логики . Dover Publications Inc. Нью-Йорк: ISBN 978-0-486-63462-3 .
Генцен, Герхард (1934). «Исследования по логическим рассуждениям. I» . Математический журнал . 39 (2): 176–210. дои : 10.1007/bf01201353 . S2CID 121546341 .
Генцен, Герхард (1935). «Исследования по логическим рассуждениям. II» . Математический журнал . 39 (3): 405–431. дои : 10.1007/bf01201363 . S2CID 186239837 .
Гильберт, Дэвид ; Бернейс, Пол (1970) [1939]. Основы математики II (Второе изд.). Берлин, Нью-Йорк: Springer Verlag. ISBN 978-3-642-86897-9 .
Хут, Майкл; Райан, Марк (2004). Логика в информатике (второе изд.). Кембридж, Соединенное Королевство: Издательство Кембриджского университета. ISBN 978-0-521-54310-1 .
Клини, Стивен Коул (2009) [1952]. Введение в метаматематику . Иши Пресс Интернешнл. 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]

[1] Дизъюнктивная семантика правой части секвенции сформулирована и объяснена Карри 1977 , стр. 189–190, Клини 2002 , стр. 290, 297, Клини 2009 , стр. 441, Гильберт и Бернейс 1970 , с. 385, Смуллян 1995 , стр. 104–105, Такеути 2013 , стр. 9, и Генцен 1934 , с. 180.

[Lemmon1965p12-2] Перейти обратно: ^а ^б Леммон 1965 , с. 12 писал: «Таким образом, секвенция — это фрейм аргумента, содержащий набор предположений и вывод, который, как утверждается, следует из них. [...] Предложения слева от «⊢» становятся предположениями аргумента, и предложение справа становится выводом, обоснованно сделанным из этих предположений».

[3] Смуллян 1995 , с. 105.

[4] Генцен 1934 , с. 180.
2.4. Последовательность A ₁ , ..., A _µ → B ₁ , ..., B _ν означает точно то же, что и формула
(А ₁ & ... & А _µ ) ⊃ (B ₁ ∨ ... ∨ B _ν ).

[5] Гильберт и Бернейс 1970 , с. 385.
Последовательность используется для интерпретации содержания.
А ₁ , ..., А _р → В ₁ , ..., Б _s ,

где числа r и s отличны от 0, что эквивалентно импликации
(А ₁ & ... & А _р ) → (B ₁ ∨ ... ∨ B _s )

[6] Церковь 1996 , с. 165.

[7] Карри 1977 , с. 184

[8] Хут и Райан (2004 , стр. 5)

[9] Бен-Ари 2012 , с. 69 определяет секвенции в виде U ⇒ V для (возможно, непустых) множеств формул U и V . Затем он пишет:
«Интуитивно, секвенция представляет собой «доказуемую из» в том смысле, что формулы в U являются предположениями для множества формул V , которые должны быть доказаны. Символ ⇒ подобен символу ⊢ в гильбертовых системах, за исключением того, что ⇒ является частью объектного языка формализуемой дедуктивной системы, а ⊢ — это метаязыковая нотация, используемая для рассуждений о дедуктивных системах».

[10] Правиц 2006 , с. 90.

[11] См. Prawitz 2006 , с. 91, где описаны эти и другие подробности интерпретации.

[12] Генцен 1934 , Генцен 1935 .

[13] Клини 2002 , с. 441

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]