Логические последовательности: антецеденты и консеквенты.

Введение

Логическое доказательство, включающее антецеденты и консеквенты.

В математической логике последовательность — это очень общий вид условного утверждения. Последовательность может иметь любое число m формул-антецедентов Ai (называемых "антецедентами") и любое число n формул-консеквентов Bj (называемых "сукцедентами" или "консеквентами"). Последовательность понимается как то, что если все антецеденты истинны, то хотя бы одна из консеквент является истинной. Этот стиль условного утверждения почти всегда связан с концептуальной основой исчисления секвенций.

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

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

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

В крайнем случае, когда список предшествующих формул последовательности пуст, последовательность является безусловной. Это отличается от простого безусловного утверждения, поскольку число заключающих формул произвольно, и не обязательно равно единице. Например, ‘⊢ B1, B2’ означает, что истинным должно быть либо B1, либо B2, либо оба. Пустой список предшествующих формул эквивалентен высказыванию "всегда истинному", называемому "верум", обозначаемому "⊤". (См. статью о символе "⊤".) В крайнем случае, когда список заключающих формул последовательности пуст, правило остается в силе: по крайней мере одно выражение справа должно быть истинным, что очевидно невозможно. Это обозначается высказыванием "всегда ложным", называемым "falsum", обозначаемым "⊥". Поскольку следствие ложно, по крайней мере одно из предшествующих выражений должно быть ложным. Например, ‘A1, A2 ⊢’ означает, что по крайней мере одно из предшествующих выражений A1 и A2 должно быть ложным. Здесь вновь проявляется симметрия, обусловленная дизъюнктивной семантикой правой части. Если левая часть пуста, то одно или несколько выражений правой части должны быть истинными. Если правая часть пуста, то одно или несколько выражений левой части должны быть ложными. Совершенно крайний случай ‘⊢’, когда списки как предшествующих, так и заключающих формул пусты, является "неудовлетворимым". В этом случае смысл последовательности фактически сводится к ‘⊤ ⊢ ⊥’. Это эквивалентно последовательности ‘⊢ ⊥’, которая, очевидно, не может быть истинной.

Примеры

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

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

Символ утверждения в последовательности первоначально означал то же самое, что и оператор импликации. Но со временем его значение изменилось, чтобы обозначать доказуемость в рамках теории, а не семантическую истину во всех моделях. В 1934 году Гентцен не определял символ утверждения '⊢' в последовательности для обозначения доказуемости. Он определил его как означающий то же самое, что и оператор импликации '⇒'. Используя '→' вместо '⊢' и '⊃' вместо '⇒', он писал: "Последовательность A1, …, Aμ → B1, …, Bν означает, в отношении содержания, точно то же самое, что и формула (A1 & … & Aμ) ⊃ (B1 ∨ … ∨ Bν)". (Гентцен использовал символ правой стрелки между антецедентами и консеквентами последовательностей. Он использовал символ '⊃' для оператора логической импликации.) В 1939 году Гильберт и Бернайс также заявили, что последовательность имеет то же значение, что и соответствующая формула импликации. В 1944 году Алонзо Черч подчеркнул, что последовательные утверждения Гентцена не означают доказуемости. "Применение теоремы дедукции в качестве примитивного или производного правила, однако, не следует путать с использованием Sequenzen у Гентцена. Ибо стрелка Гентцена → не сопоставима с нашим синтаксическим обозначением ⊢, но принадлежит его объектному языку (что ясно из того факта, что выражения, содержащие ее, появляются в качестве посылок и заключений в применении его правил вывода)." Многочисленные публикации после этого времени утверждали, что символ утверждения в последовательностях действительно означает доказуемость в рамках теории, в которой эти последовательности сформулированы. Карри в 1963 году, Леммон в 1965 году, все утверждают, что символ утверждения в последовательности означает доказуемость. Однако, [имя автора] утверждает, что символ утверждения в последовательностях системы Гентцена, который он обозначает как '⇒', является частью объектного языка, а не метаязыка. Согласно Правицу (1965): "Исчисления последовательностей можно понимать как метаисчисления для отношения выводимости в соответствующих системах натуральной дедукции". И далее: "Доказательство в исчислении последовательностей можно рассматривать как инструкцию о том, как построить соответствующую натуральную дедукцию". Другими словами, символ утверждения является частью объектного языка для исчисления последовательностей, которое является своего рода метаисчислением, но одновременно обозначает выводимость в базовой системе натуральной дедукции.

The assertion symbol in sequents originally meant exactly the same as the implication operator. But over time, its meaning has changed to signify provability within a theory rather than semantic truth in all models. In 1934, Gentzen did not define the assertion symbol ' ⊢ ' in a sequent to signify provability. He defined it to mean exactly the same as the implication operator ' ⇒ '. Using ' → ' instead of ' ⊢ ' and ' ⊃ ' instead of ' ⇒ ', he wrote: "The sequent A1, , Aμ → B1, , Bν signifies, as regards content, exactly the same as the formula (A1 & & Aμ) ⊃ (B1 ∨ ∨ Bν)". (Gentzen employed the right arrow symbol between the antecedents and consequents of sequents. He employed the symbol ' ⊃ ' for the logical implication operator.) In 1939, Hilbert and Bernays stated likewise that a sequent has the same meaning as the corresponding implication formula. In 1944, Alonzo Church emphasized that Gentzen's sequent assertions did not signify provability. "Employment of the deduction theorem as primitive or derived rule must not, however, be confused with the use of Sequenzen by Gentzen. For Gentzen's arrow, →, is not comparable to our syntactical notation, ⊢, but belongs to his object language (as is clear from the fact that expressions containing it appear as premisses and conclusions in applications of his rules of inference)." Numerous publications after this time have stated that the assertion symbol in sequents does signify provability within the theory where the sequents are formulated. Curry in 1963, Lemmon in 1965, all state that the sequent assertion symbol signifies provability. However, states that the assertion symbol in Gentzen system sequents, which he denotes as ' ⇒ ', is part of the object language, not the metalanguage. According to Prawitz (1965): "The calculi of sequents can be understood as meta calculi for the deducibility relation in the corresponding systems of natural deduction." And furthermore: "A proof in a calculus of sequents can be looked upon as an instruction on how to construct a corresponding natural deduction." In other words, the assertion symbol is part of the object language for the sequent calculus, which is a kind of meta calculus, but simultaneously signifies deducibility in an underlying natural deduction system.

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

Последовательность — это формализованное утверждение о доказуемости, которое часто используется при определении исчислений для дедукции. В исчислении секвенций название «последовательность» используется для обозначения конструкции, которую можно рассматривать как специфический вид суждения, характерный для этой системы дедукции. Интуитивное значение последовательности Γ ⊢ Σ заключается в том, что при допущении Γ заключение Σ доказуемо. Классически формулы слева от разделителя (turnstile) можно интерпретировать как конъюнкцию, а формулы справа — как дизъюнкцию. Это означает, что если все формулы в Γ истинны, то хотя бы одна формула в Σ также должна быть истинной. Если сукцедент (правая часть) пуст, это интерпретируется как ложь, то есть Γ ⊢ ⊥ означает, что Γ доказывает ложь и, следовательно, является противоречивым. С другой стороны, пустой антецедент (левая часть) считается истинным, то есть ⊢ Σ означает, что Σ следует без каких-либо предположений, то есть всегда истинно (как дизъюнкция). Последовательность такого вида, с пустым Γ, известна как логическое утверждение. Конечно, возможны и другие интуитивные интерпретации, которые классически эквивалентны. Например, Γ ⊢ Σ можно понимать как утверждение о том, что не может быть так, чтобы все формулы в Γ были истинными, а все формулы в Σ — ложными (это связано с интерпретациями двойного отрицания в классической интуиционистской логике, например, с теоремой Гливенко). В любом случае, эти интуитивные интерпретации носят лишь педагогический характер. Поскольку формальные доказательства в теории доказательств являются чисто синтаксическими, значение (вывода) последовательности определяется только свойствами исчисления, которое предоставляет фактические правила вывода. Если не допустить противоречий в технически точном определении выше, мы можем описать последовательности в их исходной логической форме. Γ представляет собой набор предпосылок, с которых мы начинаем логическое рассуждение, например, «Сократ — человек» и «Все люди смертны». Σ представляет собой логическое заключение, которое следует из этих предпосылок. Например, «Сократ смертен» следует из разумной формализации вышеуказанных утверждений, и мы можем ожидать увидеть его на стороне разделителя. В этом смысле, Γ ⊢ Σ означает процесс рассуждения, или «следовательно» на английском языке.

A sequent is a formalized statement of provability that is frequently used when specifying calculi for deduction. In the sequent calculus, the name sequent is used for the construct, which can be regarded as a specific kind of judgment, characteristic to this deduction system. The intuitive meaning of the sequent is that under the assumption of Γ the conclusion of Σ is provable. Classically, the formulae on the left of the turnstile can be interpreted conjunctively while the formulae on the right can be considered as a disjunction. This means that, when all formulae in Γ hold, then at least one formula in Σ also has to be true. If the succedent is empty, this is interpreted as falsity, i. e. means that Γ proves falsity and is thus inconsistent. On the other hand an empty antecedent is assumed to be true, i. e., means that Σ follows without any assumptions, i. e., it is always true (as a disjunction). A sequent of this form, with Γ empty, is known as a logical assertion. Of course, other intuitive explanations are possible, which are classically equivalent. For example, can be read as asserting that it cannot be the case that every formula in Γ is true and every formula in Σ is false (this is related to the double negation interpretations of classical intuitionistic logic, such as Glivenko's theorem). In any case, these intuitive readings are only pedagogical. Since formal proofs in proof theory are purely syntactic, the meaning of (the derivation of) a sequent is only given by the properties of the calculus that provides the actual rules of inference. Barring any contradictions in the technically precise definition above we can describe sequents in their introductory logical form. represents a set of assumptions that we begin our logical process with, for example "Socrates is a man" and "All men are mortal". The represents a logical conclusion that follows under these premises. For example "Socrates is mortal" follows from a reasonable formalization of the above points and we could expect to see it on the side of the turnstile. In this sense, means the process of reasoning, or "therefore" in English.

Вариации

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

Этимология

Исторически секвенты были введены Герхардом Гентценом для уточнения его знаменитого секвенциального исчисления. В своей немецкой публикации он использовал слово "Sequenz". Однако в английском языке слово "sequence" уже используется как перевод немецкого "Folge" и довольно часто встречается в математике. Термин "sequent" был создан в поисках альтернативного перевода немецкого выражения. Клин делает следующий комментарий относительно перевода на английский язык: "Гентцен использует 'Sequenz', который мы переводим как 'sequent', поскольку мы уже используем 'sequence' для любой последовательности объектов, где немецкий эквивалент – 'Folge'."