Последовательное исчисление
Основная статья: Последовательное исчисление
Последовательное исчисление является главной альтернативой естественной дедукции как основы математической логики . При естественной дедукции поток информации является двунаправленным: правила исключения направляют информацию вниз путем деконструкции, а правила введения направляют информацию вверх путем сборки. Таким образом, доказательство с помощью естественной дедукции не читается чисто снизу вверх или сверху вниз, что делает его непригодным для автоматизации поиска доказательств. Чтобы учесть этот факт, Гентцен в 1935 году предложил свое исчисление последовательностей , хотя первоначально он задумывал его как техническое устройство для выяснения непротиворечивости логики предикатов . Клин в своей основополагающей книге 1952 года "Введение в метаматематику" дал первую формулировку последовательного исчисления в современном стиле. [11]
В последовательном исчислении все правила вывода читаются исключительно снизу вверх. Правила вывода могут применяться к элементам по обе стороны турникета . (В отличие от естественной дедукции, в этой статье используется двойная стрелка ⇒ вместо правой кнопки ⊢ для обозначения последовательностей .) Вводные правила естественной дедукции рассматр иваются как правильные правила в последовательном исчислении и структурно очень похожи. Правила исключения, с другой стороны, превращаются в левые правила в последовательном исчислении. Чтобы привести пример, рассмотрим дизъюнкцию; правые правила знакомы:
| Γ ⇒ A ───────── ∨ R1 Γ ⇒ A ∨ B | Γ ⇒ B ───────── ∨ R2 Γ ⇒ A ∨ B |
Слева:
| Γ, u: A ⇒ C Γ , v: B ⇒ C ─────────────────────────── ∨ L Γ, w: (A ∨ B) ⇒ C |
Напомним ∨ E правило естественной дедукции в локализованной форме :
| Γ ⊢ A ∨ B Γ , u: A ⊢ C Γ , v: B ⊢ C ─────────────────────────────────────── ∨ E Γ ⊢ C |
Предложение A ∨ B , которое является преемником посылки в ∨ E , превращается в гипотезу вывода в левом правиле ∨ L . Таким образом , левые правила можно рассматривать как своего рода перевернутое правило исключ ения. Это наблюдение можно проиллюстрировать следующим образом:
| естественная дедукция | последовательное исчисление | |
| ────── hyp | | элим. Правила | ↓ ────────────────────── ↑↓ знакомьтесь ↑ | | вступление. Правила | заключение | ⇒ | ─────────────────────────── инициализация ↑ ↑ | | | левые правила | правые правила | | заключение |
В последовательном исчислении левое и правое правила выполняются последовательно, пока не будет достигнута начальная последовательность, которая соответствует точке пересечения правил исключения и введения в естественной дедукции. Эти исходные правила внешне похожи на правило гипотезы естественной дедукции, но в последовательном исчислении они описывают транспозицию или рукопожатие левого и правого предложений:
| ────────── инициализация Γ, u:A ⇒ A |